Generating System Models for a Highly Configurable Train Control System Using A Domain-Specific Language: A Case Study

In this work, we present a results front case study on testing a highly configurable, safety-critical system from the railway domain using model-based risk-oriented testing. In the construction of the system and test models, we face the following problems: (i) A domain expert will usually not be knowledgeable in the construction of system models, but has very detailed knowledge which configurations of the system will be especially critical (e.g., prone to head-on collisions). Thus, a method for the construction of system and test models from domain-specific descriptions is necessary. (ii) The system model shall be validatable against the system's requirements. (iii) The verification of the system model against safety requirements should be possible. We will demonstrate an approach based on DSLs, compositional construction of Mealy machines and a proof technique as a solution to these three problems.