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.
- Formal modelling and analysis of information systems (introduction to the subject): The role of formal methods during the design and development of IT systems: formal requirement specification, modelling, verification (model checking and proof of correctness). The relation of engineering and formal models, model transformations. Design environments that support the application of formal methods (e.g., SCADE).
- Basic formal models and their semantics: Kripke-structures, transition systems, timed automata, network of timed automata.
- Formalization of requirements: Temporal logics: linear time temporal logic (LTL), branching time temporal logics (CTL, CTL*). The comparison of their expressiveness. Practical examples and applications: the Property Specification Language.
- Formal verification using model checking: Model checking by the tableau method. Symbolic model checking. The representation of the state space using reduced ordered binary decision diagrams. Bounded model checking. Verification of time dependent behaviour. Practical applications: Modelling embedded controllers using timed automata, verification of temporal properties, automated test case generation using model checkers. The UPPAAL model checker.
- Modelling state-dependent dynamic behaviour: The formal syntax and semantics of statecharts. Design using statecharts, the formal verification of properties. The typical patterns for software synthesis. Practical applications: UML 2 statecharts, software source code generation and monitor synthesis.
- Modelling and analysis of concurrent systems: The Petri-net formalism. Dynamic properties of Petri-net models (e.g., safety, liveness, boundedness). The verification of dynamic properties by simulation or on the basis of the reachability graph. Structural properties (e.g., conservativeness, consistency, invariants) and their analysis on the basis of the state equation. Property preserving model reduction techniques. Hierarchical Petri-nets. Modelling examples.
- Modelling data-dependent behaviour: The extension of Petri-nets with data types and data processing. The adaptation of the definitions of dynamic and structural properties. Practical applications: Analysis of the consistency of distributed data processing, protocol verification.
- Specification and verification of extra-functional properties: The extension of Petri-nets with probabilities and time: Stochastic Petri-nets. Formalization of properties using stochastic temporal logic. Verification of performance and dependability properties.
- Modelling data processing: The syntax and semantics of data flow networks. Model refinement, checking the consistency of model refinement. The application of data flow networks for modelling and analysis of business processes.
- Formal verification based on software source code: Model checking C programs. The use of abstraction: static analysis using abstract interpretation, predicate abstraction, counter-example guided abstraction refinement in model checking.
- During the semester: The requirements for passing the subject are 2 successful midterm exams and a successful homework. The homework 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: -
- Midterm exams can be repeated taking advantage of two repeated midterm exams. It is possible to repeat one of the unsuccessful midterm exams two times. The homework can be submitted during the repetition period, but this late submission will result in 20% decrease of the score. The submission of the homework cannot be replaced by a repeated midterm exam.