Academic catalogue

Degrees incorporating this pedagocial element :

• Master in Computer science

Description

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).

Overview:

This course consists of 2 parts.

Part 1 (3 ECTS), joint with Ensimag (3rd year)

• Introduction to concurrency theory
  • Concurrency-related issues in real life
  • Principal concepts of concurrency: linear-time vs branching time, interleaving vs true concurrency, localities
• Automata-based models of concurrency
  • Labelled transition systems and Kripke structures
  • Communicating automata / communicating state machines
  • Timed automata
• Higher-level languages for concurrent systems
  • Process calculi / process algebra
  • A simple calculus: CCS
  • Value-passing languages: LNT
  • Possible semantics for concurrency: denotational, axiomatic, operational
  • Structured Operational Semantics (Plotkin rules, SOS)
• Temporal logic and model-checking verification
  • State space, reachability analysis, and state-space explosion issues
  • Basic properties: deadlocks, livelocks, starvation, fairness, etc.
  • On-the-fly verification
  • Linear-time vs branching-time logics
  • Classical logics: mu-calculus, LTL, CTL, CTL*, PDL
  • Predefined temporal-logic patterns
  • Examples of model-checking verification tools
• Lab exercises

Part 2 (3 ECTS):

• Timing analysis of systems
  • Response time analysis
  • WCET (Worst-case execution time) analysis
  • Interference analysis in multicore systems
• 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
• Hybrid systems
  1. • Hybrid automata
  • Set-based simulation of continuous-discrete behaviour
  • Software tools for analyzing hybrid systems
  • Applications to electric circuits, automotive systems, biological systems, etc.
• Lab exercises

• 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.

Recommended prerequisite

• 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.