Safety Critical Systems: from design to verification

On June 4, 1996 the Ariane 5 rocket launched by the European Space Agency exploded just forty seconds after its lift-off. The rocket was valued at $500 million. A malfunction in Therac-25 radiation therapy caused mortal radiation overdoses leading to people death. These failures were due to software bugs. These systems are critical: Failure is not an option

Lecture's Goal:

Airplanes, trains, dams, nuclear power plants... all are now driven or monitored by computerized systems. However, programming is notoriously error-prone. Software has bugs, this is a daily experience for all of us. The question is therefore: How can we make sure that critical software works properly?

The answer is that such critical software is not developed like most software is. It is carefully specified, programming languages tailored towards real-time applications are used, it is carefully tested, and, in some cases, formal methods are used to prove that it performs as specified.

Scientific content:

The lecture is about methods and tools that increase the reliability of a computer system. It focuses on automated verification techniques that are well-known in the safety-critical industry:

• Model-checking
• Proof assistants
• SAT/SMT solving
• Abstract interpretation

We will explain the difficulties (undecidability, high algorithmic complexity) and some of the algorithmic methods to counteract them.

Practical applications and Labs

This lecture is assisted by practical labs with software tools such as Frama-C.

Some of the academic teaching staff has been involved in the development of commercial tools used in industry (Airbus…). Depending on availability, certain classes will be taught by engineers from companies who design and sell tools for designing safe computer systems.

Targeted skills

• Be aware about the importance of this topic, because automated control systems are omnipresent (e.g. fully automated subways, or adaptive cruise control), and new generation of critical systems is finding its way in our lives (e.g. self-driving cars).
• Develop skills in verification and testing, which is welcomed in most job offers in software engineering
• Improve your abstraction and analysis abilities

Lecturers

• Under construction