Formal validation method and tools for French computerized railway interlocking systems

Checks and tests before putting safety facilities into service as well as the results of these tests are essential, time consuming and may show great variations between each other. Economic constraints and the increasing complexity associated with the development of computerized tools tend to limit the capacity of the classic approval process (manual or automatic). A reduction of the cover rate could be stated in practice. This is not compatible with the French national plan to renew the interlocking systems of the national network. The method and the tools presented in this paper make it possible to validate formally new computerized systems or evolutions of existing French interlocking systems with realtime functional interpreted Petri nets. The aim of our project is to provide the SNCF with an operating method for the formal validation of French interlocking systems. A formal proof method by assertion, which is applicable to industrial automation equipment such as interlocking systems, and which covers equally the specification and its real software implementation, is presented in this paper. With the proposed method and its associated tools we completely verify that the system follows all safety properties at any time and does not show superfluous conditions: it replaces all the indoor checks (not the outdoor checks). It can easily be included in the existing SNCF testing procedures. The immediate advantages expected are a significant reduction of testing time and of the related costs, an increase of the test cover rate, an answer to the new demand of the railway infrastructure maintenance engineering in situation of modify and validate computerized interlocking systems. Formal methods mastery by infrastructure engineers are surely a key to prove that more safety is not necessary more expensive.