David Deharbe

Thierry Lecomte, David Deharbe, Paulin Fournier et al.

The CLEARSY Safety Platform (CSSP) was designed to ease the development of safety critical systems and to reduce the overall costs (development, deployment, and certification) under the pressure of the worldwide market. A smart combination of hardware features (double processor) and formal method (B method and code generators) was used to produce a SIL4-ready platform where safety principles are built-in and cannot be altered by the developer. Summarizing a 5-year return of experience in the effective application in the railways, this article explains how this approach is a game-changer and tries to anticipate the future of this platform for safety critical systems. In particular, the education of future engineers and the seamless integration in existing engineering processes with the support of Domain Specific Languages are key topics for a successful deployment in other domains. DSL like Robosim to program mobile robots and relay circuits to design railway signalling systems are connected to the platform.

Thierry Lecomte, David Deharbe, Denis Sabatier et al.

Developing safety critical applications often require rare human resources to complete successfully while off-the-shelf block solutions appear difficult to adapt especially during short-term projects. The CLEARSY Safety Platform fulfils a need for a technical solution to overcome the difficulties to develop SIL3/SIL4 system with its technology based on a double-processor and a formal method with proof to ensure safety at the highest level. The formal method, namely the B method, has been heavily used in the railways industry for decades. Using its IDE, Atelier B, to program the CLEARSY Safety Platform ensures a higherlevel of confidence on the software generated. This paper presents this platform aimed at revolutionising the development of safety critical systems, developed through the FUI project LCHIP (Low Cost High Integrity Platform).

Thierry Lecomte, David Deharbe, Etienne Prun et al.

Industrial applications involving formal methods are still exceptions to the general rule. Lack of understanding, employees without proper education, difficulty to integrate existing development cycles, no explicit requirement from the market, etc. are explanations often heard for not being more formal. Hence the feedback provided by industry to academics is not as constructive as it might be. Summarizing a 25-year return of experience in the effective application of a formal method - namely B and Event-B - in diverse application domains (railways, smartcard, automotive), this article makes clear why and where formal methods have been applied, explains the added value obtained so far, and tries to anticipate the future of these two formalisms for safety critical systems.