Formal methods in safety-critical railway systems

Abstract. In this article we would like to present some recent applications of the B formal method to the development of safety critical systems, namely platform screen door controllers. These SIL3/SIL41 compliant systems have their functional specification based on a formal model. This model has been proved, guaranteeing a correct by construction behaviour of the system in absence of failure of its components. The constructive process used during system specification and design leads to a high quality system which has been qualified2 by French authorities. 1