PristupačnostAnalysis and Synthesis of Real-Time Systems
Data is displayed for academic year: 2023./2024.
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
Postgraduate doctoral study programme
Literature
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
For students
General
ID 154685
Winter semester
6 ECTS
L2 English Level
L1 e-Learning