Formal Modeling of a New On-Board Train Integrity System ETCS Compliant

Several European railway actors are committed to develop a new train monitoring system that is implemented on-board trains, to replace the trackside integrity monitoring function. Having such an on-board integrity monitoring system is key issue toward operation in moving block, namely as in ERTMS Level 3 such an operation allows not only for increasing the capacity of the line, but also for achieving substantial cost saving as various trackside equipment can be removed. Using an on-board control-command system for the train integrity functionality, transfers more responsibility, in terms of train operation safety, from infrastructure managers to railway operators. To ensure the implementation of a safety critical functions, such as the on-board train integrity (OTI) function, a particular care should be paid to its specifications. The present paper falls in this context and proposes formal verification of the OTI specifications to ensure their completeness and correctness, while tackling ambiguity inherent in textual specifications.Model checking is brought into play to check various types of properties automatically, in particular safety properties. This automatic formal verification technique allows for exhaustively checking the system behavior. An extended variant of timed automata that are supported by the UPPAAL tool are used as a modelling notation.