Formal validation method for computerized railway interlocking systems

SNCF is responsible for putting into service all interlocking systems on the French railway network. It is therefore essential, especially for computerized SIL4 systems that, SNCF has its own approval process to ensure that new interlocking systems are safe in the context of the French network. 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 validation cover rate could result in practice. The method and the tool presented in this paper makes it possible to formally validate new computerized systems or evolutions of existing French interlocking systems with real-time functional interpreted Petri nets. The aim of our project is to provide SNCF with an effective 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 all times 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 coverage rate, an answer to the new demand of railway infrastructure maintenance engineering to modify and validate computerized interlocking systems. Formal methods mastery by infrastructure engineers is surely a key to prove that more safety is not necessarily more exp- ensive.