Resumen
This paper presents the latest results of a three years 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 there 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 were no 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 years 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.