Infopaket

Formal methods of software engineering

ВК.1.01

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

Second

2023/2024

3 Semester

3

LO03. Build and research models of information processes in the applied field. LO10. Modify existing and develop new algorithmic solutions for detailed software design.

1. To know certain sections of discrete mathematics, first of all, mathematical logic, theory of algorithms, theory of abstract automata, theory of Boolean functions, theory of graphs, theory of algebraic systems and others. 2. Know the basic concepts of programming and the principles of program development.

The goal of the discipline is to learn and analyze the basic mathematical methods of writing specifications, developing and verifying software and computer equipment (at all stages of their life cycle). As a result of studying the academic discipline, the master's student should know: the role of formal methods in the life cycle of programs; tabular means of specification of programs; equalities, substitutions and the problem of defining semantics; denotational, operational and axiomatic semantics, their connection with substitutions; logical means and axiomatic descriptions; graphic means of specification: graphs, networks, diagrams; operations, expressions, procedural means and their combination; means of modularization, typification, structuring and their implementation; means of naming (in particular, variable names and concepts, contexts and scopes of names); methodological principles and pragmatic recommendations for the application of formal methods of software engineering. As a result of studying the academic discipline, the master's student should be able to: apply the acquired knowledge in the development of software systems (for which reliability or security are important) in order to protect them from errors both at the early stages of writing requirements and specifications, and for fully formal development of program implementation.

1. Hoare, C.A.R. Communicating Sequential Processes. London: Prentice-Hall International. – 1985. 2. Milner R.G. A Theory of Type Polymorphism in Programming. Journal of Computer and System Science, 1978, 17, p. 348-357. 3. Joseph Goguen and Grant Malcolm, Algebraic Semantics of Imperative Programs. – MIT Press, 1996. 4. Björner, Dines; Henson, Martin C. (Eds.) Logics of Specification Languages, Series: Monographs in Theoretical Computer Science. An EATCS Series 2008, XXII, 624 p. 69 illus., Hardcover. 5. RAISE Method Group. The RAISE Development Method. BCS Practitioner Series. Prentice Hall. 1995. – 493 p. 6. Rod M. Burstall , Joseph A. Goguen, The Semantics of CLEAR, A Specification Language, Proceedings of the Abstract Software Specifications, 1979, Copenhagen Winter School, p. 292-332, January 22-February 02. 7. Guttag J.V., Horning J.J. Larch: Languages and Tools for Formal Specification. – Springer-Verlag, Texts and monographs in Computer Science, 1993. – 259 p.

Lectures, independent work, tests, homework, test.

Intermediate assessment: 1. Control work 1: SC01, SC04, SC05 - 50 points / 9 points. 2. Control work 2: SC01, SC04, SC05 - 50 points / 10 points. Final evaluation (in the form of differentiated credit): 1. The maximum number of points that can be received by a student for credit on a 100-point scale: 100 points; 2. The minimum threshold level of a positive assessment, at which a student is admitted to credit (on a 100-point scale): 20 points. 3. Learning outcomes that are assessed on credit: SC01, SC04, SC05.

ukrainian