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

Résultats de recherche: Le chapitre dans un livre, un rapport, une anthologie ou une collection › Contribution à une conférence › Revue par des pairs

Résumé

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.

langue originale	Anglais
titre	Abstract State Machines, Alloy, B, TLA, VDM, and Z - 6th International Conference, ABZ 2018, Proceedings
rédacteurs en chef	Michael Butler, Thai Son Hoang, Alexander Raschke, Klaus Reichl
Editeur	Springer Verlag
Pages	353-366
Nombre de pages	14
ISBN (imprimé)	9783319912707
Les DOIs	https://doi.org/10.1007/978-3-319-91271-4_24
état	Publié - 1 janv. 2018
Evénement	6th International Conference on ABZ Conference on ASM, Alloy, B, TLA, VDM, and Z, ABZ 2018 - Southampton, Royaume-Uni Durée: 5 juin 2018 → 8 juin 2018

Série de publications

Nom	Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume	10817 LNCS
ISSN (imprimé)	0302-9743
ISSN (Electronique)	1611-3349

Une conférence

Une conférence	6th International Conference on ABZ Conference on ASM, Alloy, B, TLA, VDM, and Z, ABZ 2018
Pays/Territoire	Royaume-Uni
La ville	Southampton
période	5/06/18 → 8/06/18

Accès au document

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

Autres fichiers et liens

Lien vers la publication dans Scopus

Contient cette citation

Mammar, A., Frappier, M., Tueno Fotso, S. J., & Laleau, R. (2018). An event-B model of the hybrid ERTMS/ETCS level 3 standard. Dans 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 (p. 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. Editeur / 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)).

@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. Dans 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, p. 353-366, 6th International Conference on ABZ Conference on ASM, Alloy, B, TLA, VDM, and Z, ABZ 2018, Southampton, Royaume-Uni, 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).

Résultats de recherche: Le chapitre dans un livre, un rapport, une anthologie ou une collection › Contribution à une conférence › Revue par des pairs

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. Dans Butler M, Hoang TS, Raschke A, Reichl K, rédacteurs en chef, 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

Résumé

Série de publications

Une conférence

Accès au document

Autres fichiers et liens

Empreinte digitale

Contient cette citation