Room 206
13 January 2022 - 14h00
Formal Methods in Practice: Model Checking in the Railway Industry
by Benjamin BLANC from Prover Tech
Abstract: The railway industry is a long term user of formal methods, especially in France. For more than 30 years, both infrastructure managers and industrial suppliers are intensively using formal tools to increase confidence in the critical parts of railway systems. This is strongly encouraged by the certification authorities, since the standard in the area highly recommends such application. Most famous success stories in this context involve B Method (Siemens/RATP for Line 14 and others), Scade with corresponding tools (eg Thales for Line 13), and HLL the current standard language required in tenders (eg for ARGOS Sncf). Prover is a Swedish company that provides a tool suite for HLL including a model-checker based on SAT solvers. This model-checker is also the basis of the Design Verifier plugin used both in Scade and Simulink suites.
In this talk, I will present the typical activities performed on a daily basis, and the systems along with their properties that are currently analyzed. I will also present some trends and further goals.
