Infopaket

Software Specification Methods

ДВС.2.09

Вибіркова дисципліна для ОП

First

2022/2023

8 Semester

4

LO17.2. Know approaches to software quality evaluation and assurance, be able to apply them. LO19.2. Choose source data for software systems design, guided by formal methods of modelling and requirements description.

Distance form

Know: basic concepts of programming theory, methods of formalization of programming languages, in particular formalization and analysis of semantics and syntax of programs; theory of least fixed points. Be able to: formalize the syntax of programming languages ​​using BNF and grammars, perform syntactic analysis of programs, construct a semantic term of a program in the algebra of programs, prove the correctness of programs. Formalize and investigate recursive programs. Possess elementary skills: programming in modern languages.

The goal of the discipline is to get acquainted with formal methods of specifications and master formal methods of program specifications, their practical application using the example of formal specification languages ​​Z, Dafny, B and UML/OCL. The learning course "Software Specification Methods" is a component of the educational-professional program of 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", the educational-professional program "Informatics". This discipline is an optional educational discipline in the "Informatics" program, specializing in "Theory and Technology of Programming". Taught in the 8th semester of the 4nd year with a total of 120 hours (4 ECTS credits), including: lectures - 40 hours, consultations - 2 hours, self-study - 78 hours. The course consists of 2 parts, 2 tests and 1 design work. The discipline is concluded with an exam in the 8th semester.

1. SMT-LIB Theory of Nominative Data / Omelchuk L. and Shyshatska O. // Springer Nature Switzerland AG, Communications in Computer and Information Science, 1175 CCIS, pp. 89-110, 2020. 2. І. Rodhe, M. Karresand. Overview of formal methods in software engineering. – FOI Swedish Defence Research Agency, 2015. – 50 р. 3. S. Kumar, R.S. Suryavanshi, G. Chandra. Formal Methods:Techniques and Languages For Software Development // International Journal of Engineering Science and Advanced Research 1 (1), 2015. – Р. 35-42. 4. Omelchuk L.L. Formalni metody spetsyfikatsii prohram // K.: UkrINTEI, 2009. – 78 s. 5. Bui D.B., Nikitchenko M.S., Omelchuk L.L., Redko V.N., Shyshatska O.V. Klasyfikatsiia mov ta metodiv formalnykh spetsyfikatsii prohramnykh system // Theoretical and applied aspects of program systems development (TAAPSD’2008). – Abstracts. – Berdyansk, Ukraine, 2007. P. 27-33.

Lectures, independent work.

Semester assessment: 1. Test paper 1: РН 1.1., РН 1.2 — 20 points/12 points. 2. Test paper 2: РН1.2, РН 2.1, РН 2.2, РН2.3 - 20 points/12 points. 3. Project work: РН2.1, РН 2.2, РН2.3, РН3.1, РН4.1, РН4.2 – 20 points/12 points. The final assessment (in the form of an exam) indicates: - the maximum number of points that can be obtained by a student: 40 points; - learning outcomes that will be assessed: PH1.1, PH1.2, PH2.1, PH2.2, PH2.3; - form of conduct and types of tasks: written. Types of tasks: 6 written tasks.

Ukrainian