| Line 19: | Line 19: | ||
[[file:ProB_DB_HL3. | [[file:ProB_DB_HL3.png|center||500px]] | ||
== CBTC == | == CBTC == | ||
Together with ClearSy and Alstom we have also worked on a model of a CBTC Zone Controller:, which is described in a [https://doi.org/10.1007/978-3-030-18744-6_13 scientific article]. | Together with ClearSy and Alstom we have also worked on a model of a CBTC Zone Controller:, which is described in a [https://doi.org/10.1007/978-3-030-18744-6_13 scientific article]. | ||
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.
