Modeling the hybrid ERTMS/ETCS level 3 standard using a formal requirements engineering approach

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

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

Modeling the hybrid ERTMS/ETCS level 3 standard using a formal requirements engineering approach

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

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

Abstract

This paper presents a specification of the hybrid ERTMS/ETCS level 3 standard in the framework of the case study proposed for the 6th edition of the ABZ conference. The specification is based on the method and tools, developed in the ANR FORMOSE project, for the modeling and formal verification of critical and complex system requirements. The requirements are specified with SysML/KAOS goal diagrams and are automatically translated into B System specifications, in order to obtain the architecture of the formal specification. Domain properties are specified by ontologies with the SysML/KAOS domain modeling language, based on OWL and PLIB. Their automatic translation completes the structural part of the formal specification. The only part of the specification, which must be manually completed, is the body of events. The construction is incremental, based on the refinement mechanisms existing within the involved methods. The formal specification of the case study is composed of seven refinement levels and all the proofs have been discharged with the Rodin prover.

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	262-276
Number of pages	15
ISBN (Print)	9783319912707
DOIs	https://doi.org/10.1007/978-3-319-91271-4_18
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

B System
Domain modeling
Goal diagrams
Ontologies
Requirements engineering
SysML/KAOS

Access to Document

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

Cite this

Tueno Fotso, S. J., Frappier, M., Laleau, R., & Mammar, A. (2018). Modeling the hybrid ERTMS/ETCS level 3 standard using a formal requirements engineering approach. 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. 262-276). (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_18

Tueno Fotso, Steve Jeffrey ; Frappier, Marc ; Laleau, Régine et al. / Modeling the hybrid ERTMS/ETCS level 3 standard using a formal requirements engineering approach. 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. 262-276 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)).

@inproceedings{5b252fd0e4064067b9fbbf31c68f36e8,

title = "Modeling the hybrid ERTMS/ETCS level 3 standard using a formal requirements engineering approach",

abstract = "This paper presents a specification of the hybrid ERTMS/ETCS level 3 standard in the framework of the case study proposed for the 6th edition of the ABZ conference. The specification is based on the method and tools, developed in the ANR FORMOSE project, for the modeling and formal verification of critical and complex system requirements. The requirements are specified with SysML/KAOS goal diagrams and are automatically translated into B System specifications, in order to obtain the architecture of the formal specification. Domain properties are specified by ontologies with the SysML/KAOS domain modeling language, based on OWL and PLIB. Their automatic translation completes the structural part of the formal specification. The only part of the specification, which must be manually completed, is the body of events. The construction is incremental, based on the refinement mechanisms existing within the involved methods. The formal specification of the case study is composed of seven refinement levels and all the proofs have been discharged with the Rodin prover.",

keywords = "B System, Domain modeling, Goal diagrams, Ontologies, Requirements engineering, SysML/KAOS",

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

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\_18",

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 = "262--276",

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",

}

Tueno Fotso, SJ, Frappier, M, Laleau, R & Mammar, A 2018, Modeling the hybrid ERTMS/ETCS level 3 standard using a formal requirements engineering approach. 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. 262-276, 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_18

Modeling the hybrid ERTMS/ETCS level 3 standard using a formal requirements engineering approach. / Tueno Fotso, Steve Jeffrey; Frappier, Marc; Laleau, Régine 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. 262-276 (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 - Modeling the hybrid ERTMS/ETCS level 3 standard using a formal requirements engineering approach

AU - Tueno Fotso, Steve Jeffrey

AU - Frappier, Marc

AU - Laleau, Régine

AU - Mammar, Amel

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

PY - 2018/1/1

Y1 - 2018/1/1

N2 - This paper presents a specification of the hybrid ERTMS/ETCS level 3 standard in the framework of the case study proposed for the 6th edition of the ABZ conference. The specification is based on the method and tools, developed in the ANR FORMOSE project, for the modeling and formal verification of critical and complex system requirements. The requirements are specified with SysML/KAOS goal diagrams and are automatically translated into B System specifications, in order to obtain the architecture of the formal specification. Domain properties are specified by ontologies with the SysML/KAOS domain modeling language, based on OWL and PLIB. Their automatic translation completes the structural part of the formal specification. The only part of the specification, which must be manually completed, is the body of events. The construction is incremental, based on the refinement mechanisms existing within the involved methods. The formal specification of the case study is composed of seven refinement levels and all the proofs have been discharged with the Rodin prover.

AB - This paper presents a specification of the hybrid ERTMS/ETCS level 3 standard in the framework of the case study proposed for the 6th edition of the ABZ conference. The specification is based on the method and tools, developed in the ANR FORMOSE project, for the modeling and formal verification of critical and complex system requirements. The requirements are specified with SysML/KAOS goal diagrams and are automatically translated into B System specifications, in order to obtain the architecture of the formal specification. Domain properties are specified by ontologies with the SysML/KAOS domain modeling language, based on OWL and PLIB. Their automatic translation completes the structural part of the formal specification. The only part of the specification, which must be manually completed, is the body of events. The construction is incremental, based on the refinement mechanisms existing within the involved methods. The formal specification of the case study is composed of seven refinement levels and all the proofs have been discharged with the Rodin prover.

KW - B System

KW - Domain modeling

KW - Goal diagrams

KW - Ontologies

KW - Requirements engineering

KW - SysML/KAOS

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

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

M3 - Conference contribution

AN - SCOPUS:85047413833

SN - 9783319912707

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

SP - 262

EP - 276

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 -

Tueno Fotso SJ, Frappier M, Laleau R, Mammar A. Modeling the hybrid ERTMS/ETCS level 3 standard using a formal requirements engineering approach. 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. 262-276. (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_18

Modeling the hybrid ERTMS/ETCS level 3 standard using a formal requirements engineering approach

Abstract

Publication series

Conference

Keywords

Access to Document

Fingerprint

Cite this