12:00, Seminar Hall
Zero-Defect Software in Space: A True Mission!
Joost-Pieter Katoen
RWTH-Aachen University, Germany.
05-02-16

---

Abstract

Building modern aerospace systems is highly demanding. They should be extremely dependable. They must offer service without interruption (i.e., without failure) for a very long time. Faults are costly and may severely damage reputations. Dramatic examples are known. Fatal defects in the control software of the Ariane-5 rocket and the Mars Pathfinder have led to headlines in newspapers all over the world. Rigorous design support and analysis techniques are called for. Bugs must be found as early as possible in the design process while performance and reliability guarantees need to be checked whenever possible. The effect of fault diagnosis, isolation and recovery must be quantifiable.

In this talk, I will report on our experiences of almost a decade in applying formal methods, in particular component-based modeling together different variants of model checking, to the design of aerospace systems.