ProB for Railways

Data Validation

ProB is being used within Siemens, Alstom, Thales and several other companies for data validation of complicated properties for safety critical systems. It was used, e.g., for Paris Line1, Sao Paulo line 4, Barcelona line 9 and many more. ProB is certified T2 SIL4 according to the Cenelec EN 50128 standard for use at Thales.

Some data validation tools using ProB:

• ClearSy Data Solver
• DTVT - Data Table Validation Tool for Alstom by ClearSy
• OLAF data validation tool by ClearSy for Alstom and SNCF
• Dave data validation tool by ClearSy for General Electric Transportation
• SafeCap

Hybrid Level 3

In this video from the Deutsche Bahn you can see ProB animating a formal B model of the ETCS hybrid-level 3 principles in real-time, controlling two trains.

There is an article in IRSE news 260 (Nov. 2019) describing the work. There is also an open-access scientific article about this work.

Here is an annotated screenshot from the video from the Deutsche Bahn :

CBTC

Together with ClearSy and Alstom we have also worked on a model of a CBTC Zone Controller:, which is described in a scientific article.