Analysis and Synthesis of Real-Time Systems

Course Description

Real-Time system as a set of communicating processes. Formal description methods. Comunicating algebras, 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. Scheduling and allocation. Tools. Examples: concurrent reactive systems, protocols, parallel algorithms, model extraction.

Grading System

6 ECTS