Author(s)

A. Ferlin, S. Collart-Dutilleul, P. Bon, V. Wiels

Abstract

Interoperability of railway systems is a major concern in the European Union. Therefore, ERTMS (European Railway Train Management System) has been defined. Nevertheless, ERTMS has to be paired with national track rules. The Perfect project studies the implementation of ERTMS on the French territory. We use an ERTMS 3D Simulator framework which is able to simulate trains, track and communication between the trains and the RBC. The simulator records all events that occur in a sequence of states called trace. Each event is timestamped, so the sequence of events can be temporally analysed. We propose a methodology to analyse the results of a scenario performed on this platform, using temporal properties. One of the strengths of this method is the computation of statistical information on the trace during its analysis, according to a dedicated pattern of property. An automatic analysis of a trace can be used in several domains. In safety, verification of critical temporal property makes sense in ensuring that a program is compliant with its specification. An analysis of an accident or near accident using temporal properties can provide a safety problem detection and a first level diagnosis. It can also be an interesting tool to evaluate the efficiency of an operator according to several criteria such as tiredness, expertise, repetitiveness of an event.

Keywords

dynamic analysis, Runtime Verification, trace, linear temporal logic, statistical information, pattern