What is the point: Formal analysis and test generation for a railway standard

Mark Bouwman, Djurre van der Wal, Bas Luttik, Mariëlle Stoelinga, Arend Rensink

Research output: Chapter in Book/Report/Conference proceedingConference contributionAcademicpeer-review

Abstract

EULYNX is an EU-level collaboration between railway infrastructure managers to standardize signaling interfaces. The main goal of EULYNX is to provide, on an EU scale, a modular and flexible railroad architecture where components can easily be exchanged. This also opens the market for specialized manufacturers that do not supply the full range of control assets, but only single components. Related to EULYNX is FormaSig, an effort to establish the safety of the EULYNX standard with mathematical rigor. In particular, one of the main objectives of FormaSig is to translate the entire EULYNX standard from the semi-formal language SysML to the formal language mCRL2. The resulting mCRL2 models will subsequently be checked for important safety requirements and used for automated testing of actual EULYNX systems. This paper presents a first case study in this direction, focusing on the EULYNX Point interface, which we have converted to an mCRL2 model. We have also derived nine safety requirements, which have all been automatically compared with the mCRL2 model. Finally, we have used the mCRL2 model to test an industrial simulator of the EULYNX Point interface fully automatically.

Original languageEnglish
Title of host publicationProceedings of the 30th European Safety and Reliability Conference and the 15th Probabilistic Safety Assessment and Management Conference
EditorsPiero Baraldi, Francesco Di Maio, Enrico Zio
Place of PublicationSingapore
PublisherResearch Publishing Services
Pages921-928
Number of pages8
ISBN (Print)978-981-14-8593-0
DOIs
Publication statusPublished - 2020
Event30th European Safety and Reliability Conference, ESREL 2020 and 15th Probabilistic Safety Assessment and Management Conference, PSAM15 2020 - Venice, Italy
Duration: 1 Nov 20205 Nov 2020
https://www.esrel2020-psam15.org/

Conference

Conference30th European Safety and Reliability Conference, ESREL 2020 and 15th Probabilistic Safety Assessment and Management Conference, PSAM15 2020
Abbreviated titleESREL 2020 PSAM 15
CountryItaly
CityVenice
Period1/11/205/11/20
Internet address

Keywords

  • Formal analysis
  • MCRL2
  • Railway systems
  • SysML
  • Test automation

Fingerprint

Dive into the research topics of 'What is the point: Formal analysis and test generation for a railway standard'. Together they form a unique fingerprint.

Cite this