An event-B model of the hybrid ERTMS/ETCS level 3 standard

Amel Mammar; Marc Frappier; Steve Jeffrey Tueno Fotso; Régine Laleau

doi:10.1007/978-3-319-91271-4_24

An event-B model of the hybrid ERTMS/ETCS level 3 standard

Amel Mammar
, Marc Frappier
, Steve Jeffrey Tueno Fotso
, Régine Laleau

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › peer-review

Abstract

This paper presents an Event-B model of the ABZ2018 case study on the European Rail Traffic Management System (ERTMS) standard. The case study focusses on the management of fixed virtual sub-sections (VSS). We model the hybrid level 3 of the standard, which assumes that trains may be either equipped with an on-board train integrity monitoring system (TIMS) and that they report their position and integrity, ERTMS trains not fitted with TIMS that report only their front position or non-ERTMS trains that do not report any information about their position. We take into account most of the main features of the case study. Our model is decomposed into four refinements. All proof obligations have been discharged using the Rodin provers, except those related to the computation of the VSS state machine, which was found to be ambiguous (nondeterministic). Our model has been validated using ProB. The main safety property, which is that ERTMS trains do not collide, is proved.

Original language	English
Title of host publication	Abstract State Machines, Alloy, B, TLA, VDM, and Z - 6th International Conference, ABZ 2018, Proceedings
Editors	Michael Butler, Thai Son Hoang, Alexander Raschke, Klaus Reichl
Publisher	Springer Verlag
Pages	353-366
Number of pages	14
ISBN (Print)	9783319912707
DOIs	https://doi.org/10.1007/978-3-319-91271-4_24
Publication status	Published - 1 Jan 2018
Event	6th International Conference on ABZ Conference on ASM, Alloy, B, TLA, VDM, and Z, ABZ 2018 - Southampton, United Kingdom Duration: 5 Jun 2018 → 8 Jun 2018

Publication series

Name	Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume	10817 LNCS
ISSN (Print)	0302-9743
ISSN (Electronic)	1611-3349

Conference

Conference	6th International Conference on ABZ Conference on ASM, Alloy, B, TLA, VDM, and Z, ABZ 2018
Country/Territory	United Kingdom
City	Southampton
Period	5/06/18 → 8/06/18

Keywords

Control system
Event-B
Hybrid ERTMS/ETCS level 3
ProB

Access to Document

10.1007/978-3-319-91271-4_24

Cite this

Mammar, A., Frappier, M., Tueno Fotso, S. J., & Laleau, R. (2018). An event-B model of the hybrid ERTMS/ETCS level 3 standard. In M. Butler, T. S. Hoang, A. Raschke, & K. Reichl (Eds.), Abstract State Machines, Alloy, B, TLA, VDM, and Z - 6th International Conference, ABZ 2018, Proceedings (pp. 353-366). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 10817 LNCS). Springer Verlag. https://doi.org/10.1007/978-3-319-91271-4_24

Mammar, Amel ; Frappier, Marc ; Tueno Fotso, Steve Jeffrey et al. / An event-B model of the hybrid ERTMS/ETCS level 3 standard. Abstract State Machines, Alloy, B, TLA, VDM, and Z - 6th International Conference, ABZ 2018, Proceedings. editor / Michael Butler ; Thai Son Hoang ; Alexander Raschke ; Klaus Reichl. Springer Verlag, 2018. pp. 353-366 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)).

@inproceedings{812d453379534abeb4ae5f709b593096,

title = "An event-B model of the hybrid ERTMS/ETCS level 3 standard",

abstract = "This paper presents an Event-B model of the ABZ2018 case study on the European Rail Traffic Management System (ERTMS) standard. The case study focusses on the management of fixed virtual sub-sections (VSS). We model the hybrid level 3 of the standard, which assumes that trains may be either equipped with an on-board train integrity monitoring system (TIMS) and that they report their position and integrity, ERTMS trains not fitted with TIMS that report only their front position or non-ERTMS trains that do not report any information about their position. We take into account most of the main features of the case study. Our model is decomposed into four refinements. All proof obligations have been discharged using the Rodin provers, except those related to the computation of the VSS state machine, which was found to be ambiguous (nondeterministic). Our model has been validated using ProB. The main safety property, which is that ERTMS trains do not collide, is proved.",

keywords = "Control system, Event-B, Hybrid ERTMS/ETCS level 3, ProB",

author = "Amel Mammar and Marc Frappier and \{Tueno Fotso\}, \{Steve Jeffrey\} and R{\'e}gine Laleau",

note = "Publisher Copyright: {\textcopyright} Springer International Publishing AG, part of Springer Nature 2018.; 6th International Conference on ABZ Conference on ASM, Alloy, B, TLA, VDM, and Z, ABZ 2018 ; Conference date: 05-06-2018 Through 08-06-2018",

year = "2018",

month = jan,

day = "1",

doi = "10.1007/978-3-319-91271-4\_24",

language = "English",

isbn = "9783319912707",

series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",

publisher = "Springer Verlag",

pages = "353--366",

editor = "Michael Butler and Hoang, \{Thai Son\} and Alexander Raschke and Klaus Reichl",

booktitle = "Abstract State Machines, Alloy, B, TLA, VDM, and Z - 6th International Conference, ABZ 2018, Proceedings",

}

Mammar, A, Frappier, M, Tueno Fotso, SJ & Laleau, R 2018, An event-B model of the hybrid ERTMS/ETCS level 3 standard. in M Butler, TS Hoang, A Raschke & K Reichl (eds), Abstract State Machines, Alloy, B, TLA, VDM, and Z - 6th International Conference, ABZ 2018, Proceedings. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 10817 LNCS, Springer Verlag, pp. 353-366, 6th International Conference on ABZ Conference on ASM, Alloy, B, TLA, VDM, and Z, ABZ 2018, Southampton, United Kingdom, 5/06/18. https://doi.org/10.1007/978-3-319-91271-4_24

An event-B model of the hybrid ERTMS/ETCS level 3 standard. / Mammar, Amel; Frappier, Marc; Tueno Fotso, Steve Jeffrey et al.
Abstract State Machines, Alloy, B, TLA, VDM, and Z - 6th International Conference, ABZ 2018, Proceedings. ed. / Michael Butler; Thai Son Hoang; Alexander Raschke; Klaus Reichl. Springer Verlag, 2018. p. 353-366 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 10817 LNCS).

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › peer-review

TY - GEN

T1 - An event-B model of the hybrid ERTMS/ETCS level 3 standard

AU - Mammar, Amel

AU - Frappier, Marc

AU - Tueno Fotso, Steve Jeffrey

AU - Laleau, Régine

N1 - Publisher Copyright: © Springer International Publishing AG, part of Springer Nature 2018.

PY - 2018/1/1

Y1 - 2018/1/1

N2 - This paper presents an Event-B model of the ABZ2018 case study on the European Rail Traffic Management System (ERTMS) standard. The case study focusses on the management of fixed virtual sub-sections (VSS). We model the hybrid level 3 of the standard, which assumes that trains may be either equipped with an on-board train integrity monitoring system (TIMS) and that they report their position and integrity, ERTMS trains not fitted with TIMS that report only their front position or non-ERTMS trains that do not report any information about their position. We take into account most of the main features of the case study. Our model is decomposed into four refinements. All proof obligations have been discharged using the Rodin provers, except those related to the computation of the VSS state machine, which was found to be ambiguous (nondeterministic). Our model has been validated using ProB. The main safety property, which is that ERTMS trains do not collide, is proved.

AB - This paper presents an Event-B model of the ABZ2018 case study on the European Rail Traffic Management System (ERTMS) standard. The case study focusses on the management of fixed virtual sub-sections (VSS). We model the hybrid level 3 of the standard, which assumes that trains may be either equipped with an on-board train integrity monitoring system (TIMS) and that they report their position and integrity, ERTMS trains not fitted with TIMS that report only their front position or non-ERTMS trains that do not report any information about their position. We take into account most of the main features of the case study. Our model is decomposed into four refinements. All proof obligations have been discharged using the Rodin provers, except those related to the computation of the VSS state machine, which was found to be ambiguous (nondeterministic). Our model has been validated using ProB. The main safety property, which is that ERTMS trains do not collide, is proved.

KW - Control system

KW - Event-B

KW - Hybrid ERTMS/ETCS level 3

KW - ProB

UR - https://www.scopus.com/pages/publications/85047441770

U2 - 10.1007/978-3-319-91271-4_24

DO - 10.1007/978-3-319-91271-4_24

M3 - Conference contribution

AN - SCOPUS:85047441770

SN - 9783319912707

T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

SP - 353

EP - 366

BT - Abstract State Machines, Alloy, B, TLA, VDM, and Z - 6th International Conference, ABZ 2018, Proceedings

A2 - Butler, Michael

A2 - Hoang, Thai Son

A2 - Raschke, Alexander

A2 - Reichl, Klaus

PB - Springer Verlag

T2 - 6th International Conference on ABZ Conference on ASM, Alloy, B, TLA, VDM, and Z, ABZ 2018

Y2 - 5 June 2018 through 8 June 2018

ER -

Mammar A, Frappier M, Tueno Fotso SJ, Laleau R. An event-B model of the hybrid ERTMS/ETCS level 3 standard. In Butler M, Hoang TS, Raschke A, Reichl K, editors, Abstract State Machines, Alloy, B, TLA, VDM, and Z - 6th International Conference, ABZ 2018, Proceedings. Springer Verlag. 2018. p. 353-366. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)). doi: 10.1007/978-3-319-91271-4_24

An event-B model of the hybrid ERTMS/ETCS level 3 standard

Abstract

Publication series

Conference

Keywords

Access to Document

Other files and links

Fingerprint

Cite this