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

This paper presents a specification of the hybrid ERTMS/ETCS level 3 standard in the framework of the case study proposed for ABZ2018. The specification is based on methods and tools, developed in the ANR FORMOSE project, for the modeling and formal verification of critical and complex system requir...

Full description

Saved in:
Bibliographic Details
Published in:International journal on software tools for technology transfer 2020-06, Vol.22 (3), p.349-363
Main Authors: Tueno Fotso, Steve Jeffrey, Frappier, Marc, Laleau, Régine, Mammar, Amel
Format: Article
Language:English
Subjects:
Abz 2018
Complex systems
Computer Science
Domains
Formal specifications
Knowledge representation
Modelling
Programming languages
Requirements specifications
Software Engineering
Software Engineering/Programming and Operating Systems
Theory of Computation
Citations: Items that this one cites
Items that cite this one
Online Access:Get full text
Tags: Add Tag
No Tags, Be the first to tag this record!
Description
Summary:This paper presents a specification of the hybrid ERTMS/ETCS level 3 standard in the framework of the case study proposed for ABZ2018. The specification is based on methods 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 that must be manually completed is the body of events. The construction is incremental, based on refinement mechanisms that exist within the involved methods. Regarding the case study, the formal specification includes seven refinement levels and all proofs have been discharged under the Rodin platform.
ISSN:1433-2779
1433-2787
DOI:10.1007/s10009-019-00542-2