Safety critical systems

Safety critical systems require the use of formal models and rely on exhaustive analysis techniques to ensure that a piece of software actually does what it is supposed to do (with regards to the requirements) et does it correctly (without bugs). This lecture gives an overview of some techniques and languages used in that context.

This course introduces several models, languages and tools dedicated to the design of safety-critical systems. This includes solutions for describing the system under design, the expected properties, perform verification and generate certified code. Scade is one example of industrial success story that builds on works from various academic languages and that is successful in both the avionics and train domains.

Content

• state-based languages ;
• dataflow languages ;
• languages to express functional properties ;
• logical time and realtime extensions ;
• exhaustive verification tools.

Grading

Contrôle continu intégral :

• 1 written exam 2h (50%)
• 1 lab work (50%).