Automating Model Transformations for Railway Systems Engineering

Abstract

Model-Based Systems Engineering (MBSE) enables system development and analysis on a suitable level of abstraction. In the context of railway systems engineering, system verification is of major importance as software failures can cause serious damage. At DB Netz AG, a railway infrastructure manager that operates large parts of the German railway system, the challenge of enabling both high-level system modelling and formal system verification is addressed by employing SysML, a widespread systems modelling language, and Event-B, a formal systems modelling language particularly suited for automated system verification. In the currently applied completely manual development process, engineers (i) create models using SysML, (ii) translate relevant parts of these models to Event-B for verification, (iii) possibly improve the Event-B models based on verification results, and finally (iv) reflect these improvements in the original SysML models. This process is both tedious and error-prone, clearly indicating a need for an increase in the level of automation. In this paper, we argue that steps (ii) and (iv) can be viewed as a coupled forward transformation and a backward synchronisation, respectively, as the SysML models cannot be completely reconstructed from their Event-B counterparts. Exploiting this observation, we demonstrate that steps (ii) and (iv) can be suitably automated using a bidirectional transformation (bx) language. With Triple Graph Grammars (TGGs) as a rule-based bx language, we establish a tool chain connecting the modelling tools used at DB Netz AG for SysML and Event-B. We show the feasibility of our automation solution by solving three representative case studies provided by DB Netz AG. Based on these case studies, we conduct a qualitative evaluation via semi-structured interviews with domain experts.