UE System design: concurrency, realtime, stochastics, and analog/digital

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

Descriptif

This course deals with the design of systems, where a system may be any combination of physical components and digital controlers, ranging from small mobile devices ("embedded systems") to large-scale infrastructures, which may be deployed over an entire country ("cyber-physical systems).

Designing such systems is intrinsically complex and expensive, especially because they must stay safe and secure while working in environments that are often unreliable or even hostile.

This design activity goes far beyond programming, because traditional programming languages are not sufficient. Instead, one needs "modeling languages" that can properly represent systems deployed in many locations and subject to non-functional constraints (time, intermittent faults, attacks). Such modeling languages must be supported by verification and validation (V&V) tools that can find design mistakes on the system models or provide guarantees that the system will function properly.

This course provides an overview of the fundamental problems present behind such industrial systems, and to provide students with knowledge and skills required to design such systems.

This course will introduce mathematically founded methods and tools in this respect, covering software, hardware, and networking protocols. In particular, it will expose how various formal models of a system can be built and analysed:

  • In concurrent systems, the emphasis is put on how components run in parallel and how they interact. These models take into account the asynchrony that is inherent in many systems, where components may not evolve at the same speed. Their analysis aim at showing that they achieve the desired functionality while avoiding undesired behaviour.
  • 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 realize the timing verification of 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 estimation of delays due to interference.
  • In probabilistic and stochastic systems, the environment is considered to be nondeterministic, but one knows that certain events take place according to probability laws. The goal is then to estimate the probability that the system will function properly during a given time or, inversely, to predict the probability of failures. The course also introduces the key concepts of (static and dynamic) fault trees.
  • Hybrid systems are dynamical systems with mixed continuous-discrete dynamics. The continuous dynamics are often described bydifferential equations and discrete dynamics by automata. They have become a commonly used mathematical model for analog/digital systems, in which digital components (such as computers) may interact with analog components (such as physical processes).

All concepts will be illustrated using industrial use-cases in various domains (in particular telecommunication, automotive, aerospace and avionics) and through the use of industrial-like tools (about 25% lab time).

  • Understand the key concepts of concurrent systems: parallel and interleaved execution, mutual exclusion, race conditions, deadlocks, livelocks.
  • Understand the key concepts of systems that evolve continuously with time, and how they can be controlled and verified.
  • Acquire methodologies to build correct concurrent and real-time systems at first, to avoid painful issues of debugging poorly-designed systems.
  • Discover modern ways of modelling concurrent systems using formal languages.
  • Get acquainted with software tools that automatically find design mistakes in concurrent systems.
  • Discover the ideas of famous computer scientists: Dijkstra, Hoare, Milner, Clarke, Emerson, Sifakis, who all received the prestigious Türing award.
  • Understand cyberphysical embedded systems specifications, design and verify systems with concurrency, real-time, stochastics or hybrid (analog/digital) properties.

Pré-requis recommandés

  • Basic knowledge of software engineering (sequential programming, possibly functional programming).
  • Basic notions of mathematics (first-order logic and automata theory).
  • No specific knowledge about hardware and software systems is required.

Informations complémentaires

Langue(s) : Anglais