UE Performance and quantitative properties

Diplômes intégrant cet élément pédagogique :


This course is devoted to approaches that compute numerical results, such as the probability of certain situations, the time needed to perform certain scenarios, cost or energy consumption, etc. More generally, we study the analysis of behaviours involving both discrete and continuous parameters.

In probabilistic systems, events may take place with certain probabilities, and one needs to ensure that desired properties are very likely to be satisfied, while undesired properties are quite unlikely to hold.

Real-time systems are systems that should not only be correct, but must in addition guarantee that some timing constraints are guaranteed. For instance, when you are flying and in the landing approach, you hope not only that the landing gear will be deployed, but that it will happen before landing. We show how to design and model real-time systems: how to get guaranteed upper bounds on execution times, how to schedule a set of software tasks.

Continuous and hybrid systems have components that evolve with time, e.g., electrical or mechanical parts. We show how to analyze and design such systems, and how to formally ensure that a design satisfies the specification.

All concepts are illustrated using industrial use-cases from the automotive, avionics and aerospace domains and through the use of industrial-like tools (about 30% lab time).


Target skills:

- Acquire methodologies to design and verify real-time systems (hardware and software)

- Understand the key concepts of systems that evolve continuously with time, and how they can be controlled and verified

- Get a hands-on experience of academic/industrial verification tools for timing and hybrid systems

- Understand the current hot topics in industry (in particular the shift to multicore) and the corresponding open research problems


The course is self-contained. In particular, no specific knowledge about hardware and software systems is required. Basic notions of automata theory would be a plus.

Informations complémentaires

Méthode d'enseignement : En présence
Lieu(x) : Grenoble - Domaine universitaire
Langue(s) : Anglais