Analysis and Synthesis of Real-Time Systems

Course Description

Reactive system as a set of communicating processes. Formal description methods. Algebra of communicating processes, automata, Petri nets and logic models. Synthesis, specification and verification of reactive systems. UML, SDL and synchronous languages. Analysis and synthesis with model transformations. Algorithms for synthesis, reachability algorithms, theorem proving. Synthesis as a constraint satisfaction problem. Deductive and inductive synthesis, Data science: process mining. Scheduling and allocation. Tools. Examples: concurrent reactive systems, protocols, parallel algorithms, model extraction.

Study Programmes

Post-graduation study


Klaus Schneider (2004.), Verification of Reactive Systems, Springer Science & Business Media
Gerard J. Holzmann (2004.), The Spin Model Checker, Edward Elgar Publishing
Marco Bernardo, Flavio Corradini (2004.), Formal Methods for the Design of Real-Time Systems, Springer Science & Business Media


ID 154685
  Winter semester
L2 English Level
L1 e-Learning