1. Home
  2. TRID
  3. View Record
TRB Annual Meeting

Implementation of ERTMS: A Methodology Based on Formal Methods and Simulation with Respect to French National Rules

This paper presents the latest results of a three year project which aims at contributing to the validation and implementation of a European system for railway signaling called ERTMS “European Rail Traffic Management System”. The management of railway trackside signaling in ERTMS is based on rules pertaining to each country and not on global rules. In order to perform a global safety assessment, a system analysis has to consider all these aspects. By the consequence, the main target of the project is to provide some methodological and software tools in order to perform consistency checking. The project named “Perfect” started in November 2012. The first step was to identify some critical scenarii leading to accidents or quasi accidents. The study leads us to focus on maintenance trains. In fact, even if they are not representing a big amount of the traffic, maintenance trains are involved in several critical situations. This intermediate result highlighted that there are no ERTMS running accidents because there was no European Train Control System 2 (ETCS2) implemented in France during the project. Consequently, the second step is to build a logical environment allowing replaying the identified scenarii under the ERTMS framework. This logical environment is obtained by a modeling task. Petri nets and B models may be used in order to provide some formal safety proofs. These two modeling tools are well accepted by some railway actors. Nevertheless ERTMS textual specification is not so formal. A semi-formal language like SysML seems to be well fitted to produce some intermediate models. A petri net model of the interlocking was proposed and a UML4secure Model was presented. The transformations of these two models into B machines have been published. Now we are able to prove some safety invariants on this global model of the system. In the last step of the project, based on the formal model some tests are generated, and then executed on the ERTMS simulation tool compliant with the official specifications. There are two kinds of motivations. The first one is to validate the assumption used by the safety proofs produced by the formal models. The second one is to play the critical scenarii in the 3D environment of the ERTMS compliant simulation tool. The scenarii are obtained from two different procedures. Firstly, the accident database analysis allows defining some critical elements. Secondly, when the formal analysis failed at providing all proofs, the corresponding scenario has to be tested. The influences of infrastructure design and working context have been revealed in this last step. During this three year project, an instrumented methodology based on formal methods and a 3D simulation framework has been developed. This global framework does not avoid all difficulties, but it may allow producing a safety proof in shortest and more deterministic time.

Language

  • English

Media Info

Subject/Index Terms

Filing Info

  • Accession Number: 01604861
  • Record Type: Publication
  • Files: TRIS
  • Created Date: Jul 23 2016 2:43PM