The Verisoft project aims at developing methods and tools for the verification of computer systems. Those embedded systems rely on different layers . A particular application is designed and compiled to be executed by an real time operating system on several distributed processors. The pervasive verification of such artifacts is achieved by the proof of a theorem stating that the distributed hardware simulates the initial application. This proof must show the formal correctness of safety critical applications, processors, real time operating systems, compilers and communication systems.
In the context of automotive systems, the subproject #6 of Verisoft aims at verifying an emergency call (eCall),
which is automatically emitted on the mobile phone network once sensors of a car have detected an accident.
The hardware supporting this application consists of several electronics control units (ECU) connected through a time triggered bus
designed in a FlexRay like manner.
The emergency call application is divided into four nodes: sensors, eCall software, mobile phone, navigation system. The scenario is that sensors send a message to eCall with the severity of the damages. Then, eCall asks the navigation system for the position of the car. Finally, eCall sends everything to the mobile phone unit. Our goal is to prove that the call is emitted after a bounded time limit.
This web page surveys the formal theory developed to verify the time triggered bus. More will come soon ... :-)