Infopaket

Formal methods in software development

ННД.07

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

Second

2023/2024

2 Semester

4

LO1. To have specialized conceptual knowledge that includes modern scientific achievements in the field of computer science and is the basis for original thinking and conducting research, critical understanding of problems in the field of computer science and at the border of the fields of knowledge LO2. To have specialized computer science problem-solving skills necessary for conducting research and/or conducting innovative activities to develop new knowledge and procedures. LO4. To manage work processes in the field of information technologies, which are complex, unpredictable and require new strategic approaches. LO6. To develop a conceptual model of an information or computer system LO7. Develop and apply mathematical methods for the analysis of information models. LO13. To assess and ensure the quality of information and computer systems for various purposes. LO16. To do research in the field of computer science.

Distance form

To know basic concepts, means and methods of mathematical logic, their application in informatics and programming; know the languages of propositional logic and logic of the 1st order, their possibilities for describing subject areas; basic methods of finding proofs and means of logical deduction. To be able to describe statements for various subject areas in formal languages of the 1st order; establish the truth of propositional formulas, quantifier-free formulas, formulas of the 1st order; establish the existence of a logical consequence; establish expressiveness and vagueness of predicates in language models. To possess elementary skills - programming in modern languages, checking the feasibility of formulas.

Course's aim: mastering the main concepts, principles, methods and tools of developing software systems using formal approaches to create modern software of high quality. The learning course "Formal methods of software development" is a component of the educational-scientific program of training specialists at the educational-qualification level "master" in the field 12 "Information technologies" from the specialty 122 "Computer science", the educational-scientific program "Informatics". This subject is a compulsory subject under the "Informatics" program. It is taught in the 2nd semester of the 1st course of the master's degree in the amount of 120 hours (4 ECTS credits), in particular: lectures - 30 hours, seminars - 8 hours, consultations - 2 hours, independent work - 80 hours. The course includes 2 parts and 2 tests. The course ends with an exam in the 2nd semester.

1. Roggenbach M., Cerone A., Schlingloff B.-H., Schneider G, Shaikh S.A. Formal Methods for Software Engineering Languages, Methods, Application Domains. Springer, 2022, 524 p. 2. Nielson F., Nielson H.R. Formal methods. An appetizer. Springer, 2019, 160 p. 3. Leslie Lamport. Specifying Systems: The TLA+ Language and Tools for Hardware and Software Engineers, 2002 Pearson Education Publ. 4. Steve Schneider. The B-Method: An Introduction, Cornerstones of Computing series, 2001. ISBN 0-333-79284-X. 5. Schneider K.: Verification of Reactive Systems. Formal Methods and Algorithms. Springer-Verlag Berlin Heidelberg (2004). 6. Jim Davies and Jim Woodcock. Using Z: Specification, Refinement and Proof. Prentice Hall International Series in Computer Science, 1996. 7. Dafny Online Tutorial. URL: https://dafny.org/dafny/OnlineTutorial/guide.html 8. The RAISE specification language. Prentice Hall Int.– 1992.– 397 p.

Lecture, independent work, project defense.

Semester assessment: 1. Test 1: LO 1.1., LO 1.2 — 25 pts/15 pts. 2. Test 2: LO 1.3 – 25 pts/15 pts. 3. Project: LO2.1, LO3.1, LO4.1 – 10 pts/6 pts Final evaluation: - maximum points: 40; - learning outcomes that are evaluated: LO1.1, LO1.2, LO1.3, LO2.1, LO3.1, LO4.1; - form of holding: written work Criteria for evaluating the student's answers to questions: - completeness of disclosure of the question 1-4 points; - logic of presentation 2 points; - analytical reasoning 1-4 points.

Ukrainian, English