Conformance in the railway industry: Single-Input-Change testing a EULYNX controller

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 1010 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.