MOSIG 2 - Option DEMIPS - UE Embedded Systems
This is the page for the "Embedded Systems" course of the MOSIG / PDES, 2016-2017 edition.
Long title: The Synchronous Approach for the Design of Safe Embedded Systems
The synchronous approach is a general answer to the problem of designing and implementing safe control systems. The key idea is to provide, at the design level, an idealized vision of time and concurrency (the so-called synchronous hypothesis). The synchronous approach has a growing importance in industry: for instance, the SCADE tool has become a de-facto standard for the design of critical avionics applications.
The course presents several aspects of the approach:
- Programming languages: based on the synchronous approach, actual programming languages can be defined, which adopt different programming "styles". We present Lustre, as a typical example of the "data-flow style" (Lustre was designed in Grenoble in the 80's and it is the core of the industrial tool SCADE), and Esterel as a typical example of the "control-flow style".
- Compilation: we study the problem of compiling high-level (parallel) programs into classical sequential code.
- Formal validation: thanks to the formal semantics of the synchronous languages, it is possible to statically check if a program satisfies the expected functional properties.
- Synchronous approach vs quantitative real-time: in the synchronous approach, time is purely discrete and logical, while the resulting implementation must fulfil quantitative real-time requirements. We discuss the relation between these two visions of time, where the notion of Worst Case Execution Time (WCET) is central.
- Implementation: we present some solutions for implementing synchronous programs on classical execution platforms, from the simplest one (``bare-metal, OS-free), to more sophisticated ones (periodic multi-tasking).
General Information, additional reading
- An article describing a complete automaton-based synchronous language 
- Courses at Collège de France:
- Verimag Laboratory 
- The short story on the map of Part I --the world at the scale 1:1, Jorge Luis Borges, Del rigor en la ciencia - Historia universal de la infamia 
- A note on the DO 178B norm for safety-critical software in avionics 
- 2007 Turing Award, model-checking 
- Ariane 5 crash (flight 501, 1996) 
- Several examples of industrial verification tools:
- The MathWorks/Polyspace 
- Prover Technologies 
- Esterel Technologies  (SCADE Tool, in particular, the Design Verifier)
- Cadence  (Assertion-based Verification)
- Mentor Graphics  (Questa Formal Verification)
- Jasper Design Automation  (Jasper Gold)
- IBM  (Sixth Sense and RuleBase)
- Synopsys  (VCS)
- Z. Manna and A. Pnueli. The Temporal Logic of Reactive and Concurrent Systems: Specification, 1992.
- Z. Manna and A. Pnueli. Temporal Verification of Reactive Systems: Safety, 1995.
- E. Clarke, O. Grumberg, and D. Peled, Model Checking, 2000.
- C. Baier and J.-P. Katoen, Principles of Model Checking, 2008.
- B. Bérard, M. Bidoit, A. Finkel, F. Laroussinie, A. Petit, L. Petrucci and Ph. Schnoebelen. Systems and Software Verification. Model-Checking Techniques and Tools, Springer, 2001. French version: Ph. Schnoebelen, B. Bérard, M. Bidoit, F. Laroussinie and A. Petit. Vérification de logiciels : techniques et outils du model-checking. Vuibert, 1999.