A Case in Point: Verification and Testing of a EULYNX Interface

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

Research output: Contribution to journalArticleAcademicpeer-review

5 Citations (Scopus)
44 Downloads (Pure)

Abstract

We present a case study on the application of formal methods in the railway domain. The case study is part of the FormaSig project, which aims to support the development of EULYNX — a European standard defining generic interfaces for railway equipment — using formal methods. We translate the semi-formal SysML models created within EULYNX to formal mCRL2 models. By adopting a model-centric approach in which a formal model is used both for analyzing the quality of the EULYNX specification and for automated compliance testing, a high degree of traceability is achieved.

The target of our case study is the EULYNX Point subsystem interface. We present a detailed catalog of the safety requirements, and provide counterexamples that show that some of them do not hold without specific fairness assumptions. We also use the mCRL2 model to generate both random and guided tests, which we apply to a third-party software simulator. We share metrics on the coverage and execution time of the tests, which show that guided testing outperforms random testing. The test results indicate several discrepancies between the model and the simulator. One of these discrepancies is caused by a fault in the simulator, the others are caused by false positives, i.e. an over-approximation of fail verdicts by our test setup.
Original languageEnglish
Article number2
Pages (from-to)1–38
JournalFormal aspects of computing
Volume35
Issue number1
Early online date16 Mar 2023
DOIs
Publication statusPublished - Mar 2023

Keywords

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

Fingerprint

Dive into the research topics of 'A Case in Point: Verification and Testing of a EULYNX Interface'. Together they form a unique fingerprint.

Cite this