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
Case Study Digital Printed Abstract View Cite Source
Type
Conference paper
Publication
6th International Conference on ASM, Alloy, B, TLA, VDM, and Z (ABZ'18)

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.

Document

Reference

% BibTex
@InProceedings{10.1007/978-3-319-91271-4_18,
author="Tueno Fotso, Steve Jeffrey
and Frappier, Marc
and Laleau, R{\'e}gine
and Mammar, Amel",
editor="Butler, Michael
and Raschke, Alexander
and Hoang, Thai Son
and Reichl, Klaus",
title="Modeling the Hybrid ERTMS/ETCS Level 3 Standard Using a Formal Requirements Engineering Approach",
booktitle="Abstract State Machines, Alloy, B, TLA, VDM, and Z",
year="2018",
publisher="Springer International Publishing",
address="Cham",
pages="262--276",
isbn="978-3-319-91271-4"
}

Sources

  • Model Archive: ZIP
  • Presentation: PDF
  • Used formal method: Event-B, B Method, and SysML/KAOS Requirements Engineering Method
  • Resources and tools: Openflexo, Rodin, The SysMLKaos Domain Modeling Tool
  • Required OS: Linux, Mac, Windows
  • Website: https://github.com/stuenofotso/SysML_KAOS_Domain_Model_Parser/tree/master/ABZ18_ERTMS
  • Remarks and recommendation: The developed model focuses on formal verification of the main requirements of the protocol. Its main objective is to assess the SysML/KAOS method and to compare it with direct specification approaches using only plain Event-B.
ABZ'18

Related