Line 37: | Line 37: | ||
** Panama \cite{DBLP:journals/corr/abs-1210-6815}. | ** 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 | * 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 | * Dave data validation tool by ClearSy for General Electric Transportation | ||
Line 51: | Line 51: | ||
* [http://safecap.cs.ncl.ac.uk/index.php/Safecap_Project_Wiki SafeCap] | * [http://safecap.cs.ncl.ac.uk/index.php/Safecap_Project_Wiki SafeCap] | ||
* Ovady used by RATP for its lines, using a tool developed by | * 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 == | == Hybrid Level 3 == |
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.
The first data validation tool based on \prob{} was independently% \footnote{Initially the \prob{} team was unaware of the development of Ovado.} developed in 2008-2009 within the EU Deploy project (cf. Section~\ref{sec-EU-projects}) with Siemens. Before 2009, the validation of the parameters was conducted by using automated provers. Siemens was using \atelierb{} with custom proof rules and tactics, dedicated to dealing with larger data values \cite{Boite:Memoire2000,DBLP:journals/tsi/Boite02}. 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 \cite{LeuschelEtAl:STS09,DBLP:journals/fac/LeuschelFFP11,DBLP:books/daglib/p/FalampinLLMP13}. It was applied to many railway systems, notably:
ProB is being used within Siemens, Alstom, Thales and several other companies for data validation of complicated properties for safety critical systems.
Most recent tool is CAVAL, also called:
The tool is certified T2 SIL4 according to the Cenelec EN 50128 standard.
ProB is certified T2 SIL4 according to the Cenelec EN 50128 standard for use at Thales.
Some other data validation tools also 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.
Here is an annotated screenshot from the video from the Deutsche Bahn :
Together with ClearSy and Alstom we have also worked on a model of a CBTC Zone Controller:, which is described in a scientific article.