Performance and quantitative properties
- 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.
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 will be illustrated using industrial use-cases from the automotive, avionics and aerospace domains and through the use of industrial-like tools (about 30% lab time).
This course is divided into two complementary parts. Part 1 is also offered to M2 students of MOSIG GVR (Graphics, Vision, and Robotics).
Part1: Feedback Control and Real-time Systems
Dynamic systems and control
- State-space models of dynamical systems
- Linear time-invariant systems
- Stability, robustness, and sensitivity
- Feedback control
- Principles of real-time systems
- Response-time analysis
Part2: Probabilistic, Timed, and Hybrid Systems
Introduction — Boolean properties vs quantitative properties
Probabilistic and stochastic systems
- Probabilistic and stochastic behaviours — Randomized algorithms
- Discrete-Time and Continuous-Time Markov Chains, and their concurrent extensions
- Steady-state and transient analyses — Probabilistic temporal logics
- Safety analysis — Static and dynamic fault-trees
- Modeling and verification of real-time systems
- WCET (Worst-Case Execution Time)
- Hybrid automata
- Set-based simulation of continuous-discrete behaviour
- Software tools for analyzing hybrid systems
- Applications to electric circuits, automotive systems, biological systems, etc.
3 ECTS for each part – 6 ECTS for the whole HECS “core” course, which comprises both parts.