Study of implementation of ERTMS with respect to french national rules using a B centred methodology

Interoperability of the rail system within Europe is a key to its competitiveness. It aims at creating a rail network allowing a transport that is safe, compliant with the required performance level of the lines, and which does not necessitate train transfers. This requires the compliance with a set of rules, of technical and operational conditions which ensure that all the safety requirements are met. The main proposition is to contribute to the implementation of a European system for railway signalling called “European Rail Traffic Management System” (ERTMS) using a methodology based on B framework tools. The idea is to assist the writer of the national operating rules. The national operating rules are expected to define the precise implementation of the high level ERTMS Specification Requirement System (SRS). They fulfils the national rule and refines the ERTMS specification in the context of a particular infrastructure. Some parts of the specification may be considered as irrelevant in the context of some particular infrastructures. A second step consists in refining the needed behaviour so that the national safety conditions and the ERTMS can be proved to be fulfilled. The methodology proposes to represent all the needed information using the B formalism in a three stepped methodology: The first step models the useful part of ERTMS specification in the context of the considered infrastructure. A requirements model is obtained. The second step consists in enriching the existing model with a precise description of the functioning of the infrastructure. More precisely, the interlocking implementation and the Automatic Train Protection (ATP) is taken into account and a process model is obtained. The third step consists in consistency checking between the two first models. The second model should be a re