Program specification and verification methods

Course: Informatics

Structural unit: Faculty of Computer Science and Cybernetics

Title
Program specification and verification methods
Code
ВК.2.02
Module type
Вибіркова дисципліна для ОП
Educational cycle
Second
Year of study when the component is delivered
2022/2023
Semester/trimester when the component is delivered
6 Semester
Number of ECTS credits allocated
3
Learning outcomes
PLO18.2 Know approaches to software quality evaluation and assurance, be able to apply them. PLO19.2 Analyse, evaluate and select instrumental and computing tools, paradigms, technologies, algorithmic and software solutions in the design and development of software systems.
Form of study
Distance form
Prerequisites and co-requisites
Know: relational databases basics and SQL query language, technologies for developing informational software systems, data access technologies principles using ADO.Net as an example, basics of HTML, CSS, and JavaScript, software engineering fundamentals, principles of technologies for web application developmentпринципи using ASP.Net as an example. To be able to: work with ADO.Net technology autonomously, work with ADO.Net Entity Framework technology, and work with ASP.Net technology. Have basic skills: programming in C#.
Course content
The aim of the discipline is to acquire basic knowledge of the testing fundamentals, formal specification, and software verification. Mastering the basic skills of designing tests for software systems, and working with the most commonly used testing tools, and tools for formal specification and verification. The educational discipline "Methods of specification and verification of programs" is a component of the program for training specialists at the first (bachelor's) level of higher education in the field of knowledge 12 "Information technologies" from the specialty 122 "Computer science", elective block "Theory and Technology of Programming", within the educational and professional program "Informatics". This discipline is an optional course in the "Informatics" program under the block of disciplines "Theory and technology of programming". Taught in the 6th semester of the 3rd course with a total of 90 hours. (3 ECTS credits) including lectures – 42 hours, consultations – 2 hours, independent work – 46 hours. The course includes 3 parts and 2 tests. The discipline ends with a credit in the 6th semester.
Recommended or required reading and other learning resources/tools
1. Buy D.B., Nikitchenko M.S., Omelchuk L.L., Redko V.N., Shyshatska O.V. Klasyfikatsiya mov ta metodiv formalnyh specifikatsiy programnyh system // Theoretical and applied aspects of program systems development (TAAPSD’2008). – Abstracts. – Berdyansk, Ukraine, 2007. P. 27-33. 2. The RAISE specification language. Prentice Hall Int.– 1992.– 397 p. 3. Babenko L.P. , Lavryshcheva K.M. Osnovy programnoi injenerii: Kyiv, "Znannya", 2001.– 269 p. 4. Hanne Riis Nielson, Flemming Nielson Semantics with Applications. An Appetizer, SpringerVerlag.– 2007.– 274p. 5. Mike Spivey. The Z Notation: A Reference Manual, 2nd edition. Prentice Hall International Series in Computer Science, 1992. 6. https://junit.org/junit4/ 7. https://testng.org/doc/documentation-main.html 8. http://static.javadoc.io/org.mockito/mockito-core/2.23.0/org/mockito/Mockito.html.
Planned learning activities and teaching methods
Lectures, laboratory works, individual work.
Assessment methods and criteria
Semester Assessment: 1. Midterm Exam (Test) 1: LO 1.2., LO 2.2 — 32 points/19 points. 2. Midterm Exam (Test) 2: LO 1.3. — 20 points/12 points. 3. Individual laboratory work 1 (project): LO1.1, LO 2.1, LO3.1 – 10 points/6 points. 4. Individual laboratory work 2 (project): LO1.1, LO 2.1, LO3.1 – 10 points/6 points. 5. Individual laboratory work 3 (project): LO2.1, LO 4.1, LO4.2 – 10 points/6 points; 6. Current assessment: LO3.1, LO 4.1, LO4.2 – 8 points/5 points; Final assessment in the form of a credit. Credit points are defined as the sum of grades/points for all successfully assessed learning outcomes provided by this program.
Language of instruction
Ukrainian

Lecturers

This discipline is taught by the following teachers

Andrii V. Kryvolap
Theory and Technology of Programming
Faculty of Computer Science and Cybernetics

Departments

The following departments are involved in teaching the above discipline

Theory and Technology of Programming
Faculty of Computer Science and Cybernetics