What is the Point: Formal Analysis and Test Generation for a Railway Standard

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

1 Citation (Scopus)

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
Pages921-928
Number of pages8
DOIs
Publication statusPublished - 1 Nov 2020

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