Formal Methods
Alapadatok
Course coordinator
habilitated associate professor
Szoba: IB421
Tel.:
+36 1 463-3598 Email: majzik (*) mit * bme * hu |
Lecturers
PhD student
Szoba: IB414 |
assistant lecturer
Szoba: IB 414 |
PhD student
Szoba: IB 414 |
Announcements
Introduction
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.