Degrees incorporating this pedagocial element :
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 largescale infrastructures, which may be deployed over an entire country ("cyberphysical 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 nonfunctional 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.
 Realtime 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 realtime systems: how to get guaranteed upper bounds on execution times, how to schedule a set of software tasks. Furthermore, in the context of multicore 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 continuousdiscrete 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 usecases in various domains (in particular telecommunication, automotive, aerospace and avionics) and through the use of industriallike 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
 Concurrencyrelated issues in real life
 Principal concepts of concurrency: lineartime vs branching time, interleaving vs true concurrency, localities
 Automatabased models of concurrency
 Labelled transition systems and Kripke structures
 Communicating automata / communicating state machines
 Timed automata
 Higherlevel languages for concurrent systems
 Process calculi / process algebra
 A simple calculus: CCS
 Valuepassing languages: LNT
 Possible semantics for concurrency: denotational, axiomatic, operational
 Structured Operational Semantics (Plotkin rules, SOS)
 Temporal logic and modelchecking verification
 State space, reachability analysis, and statespace explosion issues
 Basic properties: deadlocks, livelocks, starvation, fairness, etc.
 Onthefly verification
 Lineartime vs branchingtime logics
 Classical logics: mucalculus, LTL, CTL, CTL*, PDL
 Predefined temporallogic patterns
 Examples of modelchecking verification tools
 Lab exercises
Part 2 (3 ECTS):
 Timing analysis of systems
 Response time analysis
 WCET (Worstcase execution time) analysis
 Interference analysis in multicore systems
 Probabilistic and stochastic systems
 Probabilistic and stochastic behaviours — Randomized algorithms
 DiscreteTime and ContinuousTime Markov Chains, and their concurrent extensions
 Steadystate and transient analyses — Probabilistic temporal logics
 Safety analysis — Static and dynamic faulttrees
 Hybrid systems

 Hybrid automata
 Setbased simulation of continuousdiscrete 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 realtime systems at first, to avoid painful issues of debugging poorlydesigned 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, realtime, stochastics or hybrid (analog/digital) properties.
Recommended prerequisite
 Basic knowledge of software engineering (sequential programming, possibly functional programming).
 Basic notions of mathematics (firstorder logic and automata theory).
 No specific knowledge about hardware and software systems is required.
In brief
Period : Semestre 9Credits : 6
Number of hours
 Lectures (CM) : 36h
Contact(s)
Frederic Lang