Analysis and Synthesis of Real-Time Systems
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.
Postgraduate doctoral study programme
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
L2 English Level