Formal Methods

As the complexity of information systems and the costs of potential failures are increasing, it becomes more and more important to prove that the design of the critical system components is correct. One of the typical solutions for the challenge of provably correct design is the application of formal methods. Mathematically precise formal models allow the precise and unambiguous specification of requirements and construction of designs; formal verification allows the checking of design decisions and proof of design properties; while the verified models allow automated software synthesis. The subject provides an overview of the formal background needed for the elaboration and analysis of the formal models of IT components and systems: the modelling paradigms, the widely used formal modelling languages, and the related verification and validation techniques. The subject demonstrates the application of formal methods in the field of requirement specification, system and software design, model based verification and source code synthesis. The participants of the course who pass the requirements will be able to - understand and apply various formal methods; - construct formal models on the basis of informal descriptions; - understand the advantages and disadvantages of various formal verification techniques; - and apply tools that support the application of formal methods.

Lectures.

- Pataricza András (editor): Formális módszerek az informatikában. Második kiadás, TypoTeX Kiadó, 2006. (in Hungarian); - G. Behrmann, A. David, K. G. Larsen: A Tutorial on UPPAAL 4.0. http://www.it.uu.se/research/group/darts/papers/texts/new-tutorial.pdf; Recommended:; - D. Peled: Software Reliability Methods. Springer Verlag, 2001.; - B. Berard et al.: Systems and Software Verification: Model-Checking Techniques and Tools. Springer Verlag, 2010.; - E. M. Clarke, O. Grumberg, D. Peled:  Model Checking. MIT Press, 1999.; - W. Reisig, G. Rozenberg (eds.): Lectures on Petri Nets. Vol I-II, Springer Verlag, 1998.

Requirements: - During the semester: The requirements for passing the subject are 2 successful midterm exams and a successful homework assignment. The homework assignment includes modelling of a small-scale IT system and the verification of its required properties. The homework is assigned on the 4th week of the semester and it has to be submitted and presented from the 10th week of the semester. The final result is calculated from the results of the two midterm exams (35-35%) and the result of the homework (30%). - In the examination period: - Additional possibilities: Each midterm exam can be repeated once. The homework assignment can be submitted during the repetition period, but this late submission will result in 20% decrease of the score.