Modeling Train Systems: From High-Level Architecture Graphical Models to Formal Specifications.

Model Driven Engineering (MDE) is a software development methodology applied on complex systems, which are composed of many interacting components. This paper proposes a holistic approach based on MDE for modeling and formally verifying the high-level architectures of such systems, in particular railway systems. The approach contains a three-step process. The first one consists in proposing a high-level architecture modeling using SysML. It produces graphical models of system components, represents and documents the system in a simple way to be discussed with stakeholders and allows them to verify if this architecture corresponds to their expected requirements. We have selected diagrams that facilitate SysML high-level architecture design, namely package, block-definition, state-transition and sequence diagrams. The second step consists in transforming SysML models to Event-B formal models. The input meta-models are those of SysML, the output one is the Event-B meta-model. All of them have been adapted to our objectives. The last step is the verification of Event-B formal specifications using provers, model-checkers and animators. Formal specifications are specifically recommended for complex critical systems with high level of integrity to verify their correctness, accuracy and to allow a complete check of the entire system states and properties. We illustrate this approach on a case study of emerging standard of the ATO system running over ERTMS where compliance with the normative documents will ensure the achievement of a number of safety objectives while providing a graphical representation understandable by domain experts.