EMBEDDED SYSTEMS: Synchronous Approach

This course was given at MOSIG (Master of Science in Informatics at Grenoble) from 2013 to 2017.

Goal

The objective of the course is to present a general approach for the realization of safe embedded (critical) systems. This approach, called synchronous, aims at reconciling concurrent programming with determinism. The key idea is to separate the design level where time is a purely logical notion, and the implementation where time means real quantitative time. Here is a summary of the topics addressed:

  • General presentation of embedded systems, and their almost synonyms (reactive, real-time, cyber-physical systems etc.)
  • Principle of synchronous approach.
  • Two programming styles for synchronous languages: data-flow (Lustre) and control-flow (Esterel).
  • Compilation: from data-flow programs to sequential code.
  • Formal verification: observers, abstractions and finite state machines exploration.
  • Quantitative Real-time aspects: synchronous programs and worst-case execution time estimation.

Lectures

Exercises

We propose a set of exercises for practicing the languages and methods seen during the lectures. This is mainly a homework, however we will have from time to time a review of progress during the courses.

Tools environment

  • Use the EnsiPc machines (boot on CentOs) available in the practice rooms at Ensimag (if you have an account). In this case you have to execute the following command (hint: copy this line in the file .bashrc in your homedir):
source /user/5/raymond/lustre/setenv.sh
  • Install the lustre distribution on your own laptop

    • Download the Lustre v4 distribution

    • The linux distribution is recommended (more complete)

    • Alternative distribs are available for MacOS and Windows (via Cygwin)i. However: if you are familiar with virtualization, consider the solution of installing the tools on a virtual Linux machine (see VirtualBox for instance).

  • Optional: install Syntax highlight

Past exams