Formal Methods in SafetyCritical Railway Systems（正式的方法在SafetyCritical铁路系统）.pdfVIP

Formal Methods in Safety-Critical Railway Systems 1 1 1 Thierry Lecomte , Thierry Servat , Guilhem Pouzancre 1 ClearSy, Aix en Provence, France. {thierry.lecomte, Thierry.servat, guilhem.pouzancre}@ 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/SIL4 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 2 qualified by French authorities. 1. Introduction Historically, the B Method was introduced in the late 80s to design correctly safe software (see 3 [Abrial 96]). Promoted and supported by RATP , B and Atelier B, the tool implementing it, have been successfully applied to the industry of transportation. First real success was Meteor line 14 driverless metro in Paris: Over 110 000 lines of B models were written, generating 86 000 lines of Ada. No bugs were detected after the proofs, neither at the functional validation, at the integration validation, at on-site test, nor since the metro lines operate (October 1998). The safety-critical software is still in version 1.0 in year 2007, without any bug detected so far. Today, Alstom Transportation Systems and Siemens Trans