Formal Methods
Contents
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.
Synopsis
 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: Kripkestructures, 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 statedependent 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 Petrinet formalism. Dynamic properties of Petrinet 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 Petrinets. Modelling examples.
 Modelling datadependent behaviour: The extension of Petrinets 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 extrafunctional properties: The extension of Petrinets with probabilities and time: Stochastic Petrinets. 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, counterexample 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 smallscale 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 (3535%) and the result of the homework (30%).
 In the examination period: 

Date of the first midterm exam: 12. March, 2019 (Tuesday), 18:1519:45, room: I.B.025
 Results: After signing in as described on the page "Submitting homework and lab assignments", each student may find among her/his assignments "ME1 First midterm exam" and the related evaluation (c.f. Értékelés).
 The evaluations will be presented on 25. March, 2019 (Monday), 17:0017:30, room I.E.320.
 Points and grades: [022) fail / 1, [2228) pass / 2, [2834) satisfactory / 3, [3440) good / 4, [4050] excellent / 5
 Date of the second midterm exam: 14. May, 2019 (Tuesday), 18:1519:45, room: TBD
 Submission deadline for the homework: 27. April, 2019 (Saturday), 23:59:00
Recaps
 Each midterm exam can be repeated once. 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.

Date of the repetition of the first midterm exam: 2. April, 2019 (Tuesday), 18:1519:45, room: QI.
 Results: After signing in as described on the page "Submitting homework and lab assignments", each student may find among her/his assignments "RME1 Repeated first midterm exam" and the related evaluation (c.f. Értékelés).
 The evaluations will be presented on 8. April, 2019 (Monday), 17:0017:30, room I.E.320.
 Points and grades: [022) fail / 1, [2228) pass / 2, [2834) satisfactory / 3, [3440) good / 4, [4050] excellent / 5
 Date of the repetition of the second midterm exam: 23. May, 2019 (Thursday), 10:1511:45, room: TBD
 Late submission deadline for the homework: 22. May, 2019 (Wednesday), 23:59:00