ProB for Railways
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.
First Industrial Use of ProB for Data Validation
The first data validation tool based on ProB was independently (initially the ProB team was unaware of the development of Ovado) developed in 2008-2009 within the EU Deploy project with Siemens. Before 2009, the validation of the parameters was conducted by using automated provers. Siemens was using Atelier-B with custom proof rules and tactics, dedicated to dealing with larger data values. This, however, did not scale to many larger properties or data values, meaning that manual validation was required and thus cost intensive and more error prone. Indeed, the use of ProB did uncover at least one issue that was missed by the manual validation.
The research led to a tool called RDV, built on top of ProB, see FM'2003 article, FAC 2011 journal article (open access), chapter in Deploy book. It was applied to many railway systems, notably:
- Line 1 Paris,
- CDGVAL LISA,
- Sao Paulo line 4,
- ALGER line 1,
- Barcelona line 9
Further 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.
- by Alstom for their URBALIS 400 CBTC system in 2014 using a tool based on ProB called DTVT - Data Table Validation Tool developed by ClearSy for various lines, e.g., in
- Mexico, Toronto,
- Sao Paulo and
- Panama \cite{DBLP:journals/corr/abs-1210-6815}.
- Alstom and SNCF also applied data validation for ETCS-Level 1 software in 2018 using another tool called OLAF developed by ClearSy using ProB.
- Dave data validation tool by ClearSy for General Electric Transportation
Most recent tool is CAVAL, also called:
The tool is certified T2 SIL4 according to the Cenelec EN 50128 standard.
- by Thales using a tool based on ProB called Rubin for checking engineering rules of their ETCS RBC (Radio Block Centre) (some aspects of Rubin are discussed in \cite{10.1007/978-3-319-33600-8_10})
ProB is certified T2 SIL4 according to the Cenelec EN 50128 standard for use at Thales.
Some other data validation tools also using ProB:
- SafeCap
- Ovady used by RATP for its lines, using a tool developed by ClearSy called predicateB as first chain, and ProB as secondary tool chain \cite{DBLP:conf/sefm/AboV13,DBLP:journals/corr/abs-1210-7039}. Together with Systerel, Alstom conducted data validation of the Octys CBTC for RATP in 2017 using the Ovado tool.
Hybrid Level 3
In this video from the Deutsche Bahn (video with English subtitles) 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 inIRSE news 260 (Nov. 2019) describing the work. There is also an open-access scientific journal article about this work, which is an extended version of the ABZ'2018 article.
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.