Component-based development and verification of safety critical software for a brake-by-wire system with synchronous software components

In this paper we describe the development and verification of software for an automotive brake-by-wire system. This is a new brake system without mechanical or hydraulic backup. The system is based on a time-triggered communication architecture. The central control computer in this distributed system, called Brake-by-Wire Manager, is a redundant design in order to tolerate any single failure. The software of this computer is subject to a set of safety related requirements which must be verified. We have developed the software using synchronous software components based on the synchronous ESTEREL. Many safety properties have been verified successfully and the software has been integrated in a prototype brake-by-wire system in a research car