ProB for Railways: Difference between revisions
| Line 7: | Line 7: | ||
It is vital that these assumptions are checked when the system is put in place, as well as whenever the system is adapted (e.g., due to line extension or addition or removal of certain track sections in a railway system). | It is vital that these assumptions are checked when the system is put in place, as well as whenever the system is adapted (e.g., due to line extension or addition or removal of certain track sections in a railway system). | ||
The same issue arises also when a safety critical system was not developed using the B-method: one still needs to ensure that a software system is properly configured to ensure safety. | The same issue arises also when a safety critical system was not developed using the B-method: one still needs to ensure that a software system is properly configured to ensure safety. | ||
The task of checking the configuration data is called <b>data validation</b>. | The task of checking the configuration data is called <b>data validation</b>. | ||
Compared to proof, the difficulty arises that properties now crucially depend on given data, which can be very large. In those cases, the underlying language of B turns out to be very expressive and efficient to cleanly encode a large class of data properties. | Compared to proof, the difficulty arises that properties now crucially depend on given data, which can be very large. In those cases, the underlying language of B turns out to be very expressive and efficient to cleanly encode a large class of data properties. | ||
Revision as of 09:16, 29 April 2020
Data Validation
What is Data Validation
Safety critical system often contain many data parameters that are specific to a particular deployment. E.g. in railway systems these parameters would describe tracks, switches, signals, or possible routes. The proofs of a generic B-model often rely on assumptions about the data parameters, e.g., assumptions about the topology of the track. It is vital that these assumptions are checked when the system is put in place, as well as whenever the system is adapted (e.g., due to line extension or addition or removal of certain track sections in a railway system). The same issue arises also when a safety critical system was not developed using the B-method: one still needs to ensure that a software system is properly configured to ensure safety.
The task of checking the configuration data is called data validation. Compared to proof, the difficulty arises that properties now crucially depend on given data, which can be very large. In those cases, the underlying language of B turns out to be very expressive and efficient to cleanly encode a large class of data properties.
Industrial Uses of ProB for 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.