ProB for Railways - Revision history

Michael Leuschel: /* Hybrid Level 3 */

2021-02-04T15:09:26Z

Hybrid Level 3

← Older revision		Revision as of 15:09, 4 February 2021
Line 55:		Line 55:
	== Hybrid Level 3 ==		== Hybrid Level 3 ==

	In this [https://www.youtube.com/watch?v=FjKnugbmrP4 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.		In this [https://www.youtube.com/watch?v=FjKnugbmrP4 video from the Deutsche Bahn] ([https://www.youtube.com/watch?v=K6mS6akRmvA 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 in[https://liveportal.irse.org/LinkClick.aspx?fileticket=x_ZknNxeeMc%3d&portalid=0 IRSE news 260 (Nov. 2019)] describing the work.		There is an article in[https://liveportal.irse.org/LinkClick.aspx?fileticket=x_ZknNxeeMc%3d&portalid=0 IRSE news 260 (Nov. 2019)] describing the work.

Michael Leuschel: /* Further Industrial Uses of ProB for Data Validation */

2020-10-09T12:00:23Z

Further Industrial Uses of ProB for Data Validation

← Older revision		Revision as of 12:00, 9 October 2020
Line 45:		Line 45:
	The tool is certified T2 SIL4 according to the Cenelec EN 50128 standard.		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})		* 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.		ProB is certified T2 SIL4 according to the Cenelec EN 50128 standard for use at Thales.

Michael Leuschel: /* Hybrid Level 3 */

2020-10-09T11:59:50Z

Hybrid Level 3

← Older revision		Revision as of 11:59, 9 October 2020
Line 59:		Line 59:
	There is an article in[https://liveportal.irse.org/LinkClick.aspx?fileticket=x_ZknNxeeMc%3d&portalid=0 IRSE news 260 (Nov. 2019)] describing the work.		There is an article in[https://liveportal.irse.org/LinkClick.aspx?fileticket=x_ZknNxeeMc%3d&portalid=0 IRSE news 260 (Nov. 2019)] describing the work.
	There is also an		There is also an
	[http://link.springer.com/article/10.1007/s10009-020-00551-6 open-access scientific article] about this work, which is an extended version of the [https://link.springer.com/chapter/10.1007%2F978-3-319-91271-4_20 ABZ'2018 article].		[http://link.springer.com/article/10.1007/s10009-020-00551-6 open-access scientific journal article] about this work, which is an extended version of the [https://link.springer.com/chapter/10.1007%2F978-3-319-91271-4_20 ABZ'2018 article].

	Here is an annotated screenshot from the [https://www.youtube.com/watch?v=FjKnugbmrP4 video from the Deutsche Bahn] :		Here is an annotated screenshot from the [https://www.youtube.com/watch?v=FjKnugbmrP4 video from the Deutsche Bahn] :

Michael Leuschel: /* Hybrid Level 3 */

2020-10-09T11:59:20Z

Hybrid Level 3

← Older revision		Revision as of 11:59, 9 October 2020
Line 59:		Line 59:
	There is an article in[https://liveportal.irse.org/LinkClick.aspx?fileticket=x_ZknNxeeMc%3d&portalid=0 IRSE news 260 (Nov. 2019)] describing the work.		There is an article in[https://liveportal.irse.org/LinkClick.aspx?fileticket=x_ZknNxeeMc%3d&portalid=0 IRSE news 260 (Nov. 2019)] describing the work.
	There is also an		There is also an
	[http://link.springer.com/article/10.1007/s10009-020-00551-6 open-access scientific article] about this work.		[http://link.springer.com/article/10.1007/s10009-020-00551-6 open-access scientific article] about this work, which is an extended version of the [https://link.springer.com/chapter/10.1007%2F978-3-319-91271-4_20 ABZ'2018 article].

	Here is an annotated screenshot from the [https://www.youtube.com/watch?v=FjKnugbmrP4 video from the Deutsche Bahn] :		Here is an annotated screenshot from the [https://www.youtube.com/watch?v=FjKnugbmrP4 video from the Deutsche Bahn] :

Michael Leuschel: /* Hybrid Level 3 */

2020-10-09T11:58:06Z

Hybrid Level 3

← Older revision		Revision as of 11:58, 9 October 2020
Line 57:		Line 57:
	In this [https://www.youtube.com/watch?v=FjKnugbmrP4 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.		In this [https://www.youtube.com/watch?v=FjKnugbmrP4 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 an article in[https://liveportal.irse.org/LinkClick.aspx?fileticket=x_ZknNxeeMc%3d&portalid=0 IRSE news 260 (Nov. 2019)] describing the work.
	There is also an		There is also an
	[http://link.springer.com/article/10.1007/s10009-020-00551-6 open-access scientific article] about this work.		[http://link.springer.com/article/10.1007/s10009-020-00551-6 open-access scientific article] about this work.

Michael Leuschel: /* First Industrial Use of ProB for Data Validation */

2020-04-29T10:34:07Z

First Industrial Use of ProB for Data Validation

← Older revision		Revision as of 10:34, 29 April 2020
Line 21:		Line 21:
	The research led to a tool called RDV, built on top of ProB, see		The research led to a tool called RDV, built on top of ProB, see
	[https://link.springer.com/chapter/10.1007%2F978-3-642-05089-3_45 FM'2003 article],		[https://link.springer.com/chapter/10.1007%2F978-3-642-05089-3_45 FM'2003 article],
	[https://link.springer.com/article/10.1007%2Fs00165-010-0172-1 FAC 2011 journal article (open access)], [https://link.springer.com/chapter/10.1007%2F978-3-642-33170-1_4 chapter in Deploy book].		[https://link.springer.com/article/10.1007%2Fs00165-010-0172-1 FAC 2011 journal article (open access)], [https://link.springer.com/chapter/10.1007%2F978-3-642-33170-1_4 chapter in Deploy book]. It was applied to many railway systems, notably:

	It was applied to many railway systems, notably:
	* Line 1 Paris,		* Line 1 Paris,
	* CDGVAL LISA,		* CDGVAL LISA,

Michael Leuschel: /* First Industrial Use of ProB for Data Validation */

2020-04-29T10:33:47Z

First Industrial Use of ProB for Data Validation

← Older revision		Revision as of 10:33, 29 April 2020
Line 13:		Line 13:
	=== First Industrial Use of ProB for Data Validation ===		=== First Industrial Use of ProB for Data Validation ===

	The first data validation tool based on ~~\prob{}~~ was independently%		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.
	~~\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.		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}~~.		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.		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.		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		The research led to a tool called RDV, built on top of ProB, see
Line 27:		Line 26:
	* Line 1 Paris,		* Line 1 Paris,
	* CDGVAL LISA,		* CDGVAL LISA,
	* ~~Sa}o~~ Paulo line 4,		* Sao Paulo line 4,
	* ALGER line 1,		* ALGER line 1,
	* Barcelona line 9		* Barcelona line 9

Michael Leuschel: /* First Industrial Use of ProB for Data Validation */

2020-04-29T10:30:55Z

First Industrial Use of ProB for Data Validation

← Older revision		Revision as of 10:30, 29 April 2020
Line 20:		Line 20:
	Indeed, the use of \prob{} did uncover at least one issue that was missed by the manual validation.		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}~~.		The research led to a tool called RDV, built on top of ProB, see
			[https://link.springer.com/chapter/10.1007%2F978-3-642-05089-3_45 FM'2003 article],
			[https://link.springer.com/article/10.1007%2Fs00165-010-0172-1 FAC 2011 journal article (open access)], [https://link.springer.com/chapter/10.1007%2F978-3-642-33170-1_4 chapter in Deploy book].

	It was applied to many railway systems, notably:		It was applied to many railway systems, notably:
	* Line 1 Paris,		* Line 1 Paris,
	* CDGVAL LISA,		* CDGVAL LISA,
	* ~~S\~{a~~}o Paulo line 4,		* Sa}o Paulo line 4,
	* ALGER line 1,		* ALGER line 1,
	* Barcelona line 9		* Barcelona line 9

Michael Leuschel: /* Further Industrial Uses of ProB for Data Validation */

2020-04-29T10:16:36Z

Further Industrial Uses of ProB for Data Validation

← Older revision		Revision as of 10:16, 29 April 2020
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 ~~\clearsy{}~~ using ~~\prob{}~~.		* 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 ~~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.		* 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 ==

Michael Leuschel: /* Further Industrial Uses of ProB for Data Validation */

2020-04-29T10:16:14Z

Further Industrial Uses of ProB for Data Validation

← Older revision		Revision as of 10:16, 29 April 2020
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 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 ~~% for trains with a drive~~ in 2017 using the Ovado tool.		* 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 ==