Translating EULYNX SysML models into Symbolic Transition Systems for Model-Based Testing of Railway signaling systems
The EULYNX Consortium is a European initiative by 13 infrastructure managers to standardize interfaces and elements of railway signaling systems. The consortium aims to create high quality specifications based on semi-formal SysML models that are understandable for people without a strong mathematical background.
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. In general, MBT is an effective method to promote 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 experiments. For these experiments we utilize the Axini Modeling Language (AML) and the Axini Modeling Platform (AMP) - a commercial MBT software. As our System Under Test (SUT) we use a software simulation of the EULYNX point subsystem, used by EULYNX developers.
Our work reveals several non-conforming behaviors in the SUT such as the interruption of transitions by timeouts and the wrong execution order of behaviors. We conclude that specifications on the interface level of subsystems benefit the applicability of MBT using specification models like AML. We also formulate recommendations on how to improve the application of MBT to the EULYNX SysML specifications with clear separation of data across parallel regions and more specific port definitions.
Thu 7 AprDisplayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change
16:45 - 18:00
|Translating EULYNX SysML models into Symbolic Transition Systems for Model-Based Testing of Railway signaling systems
|Model checking C++ programs
Felipe R. Monteiro Amazon, Mikhail R. Gadelha Igalia, Lucas C. Cordeiro University of Manchester, UKLink to publication DOI
|SIFT: A Tool for Property Directed Symbolic Execution of Multithreaded Software
Tuba Yavuz University of Florida
|Automating Differential Testing with Overapproximate Symbolic Execution
|Discussion and Q&A