Epsilon-based Model Transformation and Verification of Train Control System Specification

With the development of key technologies, train control system has become network-communicating safety related distributed system. In order to guarantee functions and performances of system meet the design requirements, it is essential to model and verify the specification during system development life cycle. The emergence of model transformation methodology in model-driven engineering bridges the gap between semi-formal modeling and formal verification, and builds links with model-based verification as well. This paper presents an approach to automatic model transformation and code generation atop Epsilon model management platform, and provides a case study of RBC hand-over scenarios described in train control system specification. In this case, system requirements are modeled via UML class and state machine diagram, which are then automatically transformed into SPIN/Promela formal language by means of model-model and model-text transformation via the ETL and EGL within Epsilon, to verify the correctness of hand-over design, accordingly the consistencies between system specification, functional design and model development are assured.