Formal methods and strict safety requirements regulate the development of railway signalling and train control systems, covered by the CENELEC (European Committee for Electro-technical Standardization) EN 5012x rail standards, which constitute a variation of the generic standard IEC/IEC 61508. The development guidelines and recommendations set by the CENELEC directive have considered the specificities and successful experiences of the rail industry, such as the SACEM system implemented in Paris RER A, the SAET system in Paris metro line 1 or the SNCF TVM train control system used in French high speed trains.
The EN50128 standard specifies neither a precise development methodology, nor a particular software programming technique. However, the standard classifies a wide range of commonly adopted techniques using three levels: “Forbidden”, “Highly Recommended” and “Mandatory”, with respect to the established SIL of the component. In particular, one highly relevant recommendation of the EN 50128 standard is the use of formal techniques for the specification of systems/components with the highest SIL levels as well as for the verification activities. Indeed, formal methods allow developers to ensure that safety properties are captured in the system requirements and software specifications, and to mathematically prove that the final software product satisfies all specifications. CCS, CSP, HOL, LOTOS, OBJ, Temporal Logic, VDM, Z and B are some of the formal techniques cited.
The B method: A success story
The B method is a formal method designed by the French mathematician Jean-Raymond Abrial, and destined to be used in the specification, code generation, and verification & validation phases of software development. This mathematical method took advantage of its extensive tool support and has been successfully applied to railway signalling systems and adopted by a number of providers and operators such as SIEMENS, ALSOM and RATP… The first application dates back to the 80s, during the development of the SACEM train control system running on the Paris regional express line RER A. B industrial tools, such as the Atelier B by Clearsy, have been developed since this first application and the method has been used for many train control and safety critical systems (from Meteor 1998 to Octys 2016).
Of the 27,800 proven lemmas during the B development of the Meteor system, which is implemented in Paris metro line 1, around 90% were proven automatically using the Atelier B tool, leaving the other 10% lemmas to be interactively proven. Many errors were discovered during proof activities, but no further bugs have been detected later in the testing phases or since the commissioning of the line.
Did you like this post? Would you like to be informed about the last railway signalling technical and commercial news? Join us on LinkedIn and stay updated!
railwaysignalling.eu | walk the rail talk
What are the specific formal methods utilized in the design and development of railway signaling systems, and how do these methods contribute to ensuring the safety, reliability, and resilience of such critical infrastructure?