HECS-3

Performance and quantitative properties

Lecturers

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

Prerequisite

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.

Contents

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. Furthermore, in the context of multi-core platforms, concurrent accesses to shared resources must not generate unbounded delay: we will study interference analysis delay and solutions to get isolated implementation on such platforms.

Hybrid systems are dynamical systems with mixed continuous-discrete dynamics. The continuous dynamics are often described by differential equations and discrete dynamics by automata. They have become a commonly used mathematical model for embedded and cyber-physical systems. This course will cover fundamental notions and concepts in modeling, analysis, verification of hybrid systems, and some recent applications of hybrid systems.

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 (course ref. WMM9MO50)

 

Dynamic systems and control

  • State-space models of dynamical systems
  • Linear time-invariant systems
  • Stability, robustness, and sensitivity
  • Feedback control

Real-time systems

  • Principles of real-time systems
  • Scheduling
  • Response-time analysis

Part2: Probabilistic, Timed, and Hybrid Systems (course ref. WMM9MO49)

 

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

Real-time systems

  • Modeling and verification of real-time systems
  • WCET (Worst-Case Execution Time)analysis, main steps
  • Bounding interference delays on multi-core platforms

Hybrid systems

  • Hybrid automata
  • Set-based simulation of continuous-discrete behaviour
  • Software tools for analyzing hybrid systems
  • Applications to electric circuits, automotive systems, biological systems, etc.

Credits

3 ECTS for each part –  6 ECTS for the whole HECS “core” course, which comprises both parts.

Comments are closed.