PhD Defence Djurre van der Wal | What is... the Point? - Single-Input-Change Testing a EULYNX Specification

What is... the Point? - Single-Input-Change Testing a EULYNX Specification

Djurre van der Wal is a PhD student in the Department of Formal Methods and Tools. (Co)Promotors are prof.dr.ir. A. Rensink, prof.dr. M.I.A. Stoelinga and dr. M. Gerhold from the Faculty of Electrical Engineering, Mathematics and Computer Science.

The EULYNX standard is a collection of specifications from the railway industry that is part of the gradual transition from monolithic to modular railway systems. The increase in modularity makes it easier and more cost-effective to maintain, replace, and upgrade system components such as switches. At the same time, this shift requires efficient methods to verify whether systems meet the specifications. Until now, testing based on manually crafted scenarios has been the most common approach in the railway industry. In this dissertation, we explore how this process can be improved using an automatable technique known as model-based testing.

First, we developed jEULYNX, a Java-embedded domain-specific language that allows EULYNX specifications to be entered and modified for our research purposes. We then transform the jEULYNX code into behavioral models to derive test suites. Initially, we express the derived behavioral models in mCRL2, a well-known process algebra designed for modeling concurrent systems, and generate test suites based on the ioco theory. However, this approach does not scale well, suffers from unreliable test outcomes, and does not work seamlessly when applied to a system. To obtain smaller behavioral models, we adjust the semantics of the EULYNX specifications, and to ensure tests are reliable and directly applicable, we limit our scope to tests consisting solely of so-called Single-Input-Changes.

To validate the Single-Input-Changes approach, we apply it to the EULYNX Point, a representative EULYNX specification. We generate a behavioral model and a test suite and compare the test suite with a scenario-based test suite from the railway industry. Our test suite examines up to ten times more states of the behavioral model and identifies four errors in a software simulator of the EULYNX Point—two more than were previously known. These results confirm that the approach is effective within the context of the EULYNX standard and significantly improves the quality of test suites.