ProB for Railways: Difference between revisions
No edit summary |
|||
| Line 17: | Line 17: | ||
There is also an | There is also an | ||
[http://link.springer.com/article/10.1007/s10009-020-00551-6 open-access scientific article] about this work. | [http://link.springer.com/article/10.1007/s10009-020-00551-6 open-access scientific article] about this work. | ||
Here is an annotated screenshot from the [https://www.youtube.com/watch?v=FjKnugbmrP4 video from the Deutsche Bahn] : | |||
[[File:ProB_HL3_DB_Screenshot.png|600px|center]] | [[File:ProB_HL3_DB_Screenshot.png|600px|center]] | ||
Revision as of 08:40, 17 April 2020
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.