MOSIG 2 - Option DEMIPS - UE Embedded Systems

De Ensiwiki
Aller à : navigation, rechercher

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 [1]
  • Courses at Collège de France:
    • Gérard Berry 2007 [2], in particular [3]
    • Gérard Berry 2009 [4]
  • Verimag Laboratory [5]
  • 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 [6]
  • A note on the DO 178B norm for safety-critical software in avionics [7]
  • 2007 Turing Award, model-checking [8]
  • Ariane 5 crash (flight 501, 1996) [9]
  • Several examples of industrial verification tools: