(Created page with " == Data Validation == ProB is being used within Siemens, Alstom, Thales and several other companies for data validation of complicated properties for safety critical systems....") |
|||
| Line 1: | Line 1: | ||
== Data Validation == | == 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. | 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: | |||
* [https://www.clearsy.com/en/our-tools/clearsy-data-solver/ ClearSy Data Solver] | |||
* [http://www.data-validation.fr/data-validation-in-the-railways/ 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 | |||
* [http://safecap.cs.ncl.ac.uk/index.php/Safecap_Project_Wiki SafeCap] | |||
== Hybrid Level 3 === | == Hybrid Level 3 === | ||
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:
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.
Together with ClearSy and Alstom we have also worked on a model of a CBTC Zone Controller:, which is described in a scientific article.