Abstract We propose a novel framework for model-based testing against specifications from EULYNX, a SysML-based standard from the railway industry for the controllers of systems such as points, signals, sensors, and crossings. The main challenge here is the sheer complexity: with state spaces exceeding $10^{10}$ 10 10 states, it is hard to derive test suites that achieve a meaningful type of coverage. We tackle this problem by moving away from the traditional interleaving semantics for SysML. Instead, we propose a synchronous semantics in terms of Finite State Machines (FSMs), leveraging the fact that EULYNX is implemented on Programmable Logic Controllers (PLCs). Then, we deploy Single-Input-Change Deterministic Finite State Machines (SIC-DFSMs), which ensures fully deterministic tests, thus minimizing scalability issues. Our focus lies on the EULYNX specification for point controllers. The generated test suite achieves maximal transition coverage, but test execution time remains substantial. We introduce an additional test suite that achieves maximal transition label coverage. Remarkably, this smaller suite successfully identifies the same four faults as the larger suite.

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.

The EULYNX Consortium is a European initiative by 13 infrastructure managers to standardize interfaces of railway signaling systems. The consortium creates specifications based on semi-formal SysML models. In this paper, we research the feasibility of using the EULYNX SysML models for Model-Based Testing (MBT), which contributes to higher quality specifications and more efficient conformance testing of system implementations. MBT promotes safety, which is one of the most important aspects of railway signaling systems. Our approach is to translate EULYNX SysML models to Symbolic Transition Systems (STS) and to use the STS for MBT. We utilize the Axini Modeling Language (AML) and the Axini Modeling Platform (AMP), which are used by ProRail. As our System Under Test (SUT) we use a software simulation of the EULYNX point subsystem, used by EULYNX developers. We revealed several non-conforming behaviors of the SUT which shows that interface specifications like EULYNX benefit from the application of MBT. However, we observe that better advantage of MBT can be taken if EULYNX SysML specifications abstracted from implementation details, which is currently not the case.