Advertisement
Published in:
2018 | OriginalPaper | Chapter
Formalizing Railway Signaling System ERTMS/ETCS Using UML/Event-B
Authors : Abderrahim Ait Wakrime, Rahma Ben Ayed, Simon Collart-Dutilleul, Yves Ledru, Akram Idani
Published in: Model and Data Engineering
Publisher: Springer International Publishing
Activate our intelligent search to find suitable subject content or patents.
Select sections of text to find matching patents with Artificial Intelligence. powered by
Select sections of text to find additional relevant content using AI-assisted search. powered by
Abstract
Critical systems like railway signaling systems need to guarantee important properties such as safety. Formal methods have achieved considerable success in designing critical systems with verified desirable properties. In this paper, we propose a formal model of ERTMS/ETCS (European Rail Traffic Management System/European Train Control System) which is an innovative railway signaling system. This work focuses on Hybrid ERTMS/ETCS Level 3 which is currently under design, by studying and modeling the functionalities and relations of its different sub-systems. The proposed model is based on model transformation from UML (Unified Modeling Language) class diagrams to the Event-B formal language. UML is used as the primary modeling notation to describe the structure and the main characteristics of the studied system. The generated Event-B model is enriched by the formalization of safety properties. We verify and validate the correctness of the proposed formalization using the ProB model-checker and animator.