 | "Practical formal validation method for interlocking or automated systems"Marc Antoni SNCF - Infrastructure Direction |
Abstract
Today, a main question is to answer to the following problematic: have we recognized that for software, the delivery of absolute numerical safety targets is considered to be impossible, and the methods contained in the CENELEC standard produce a “probability” that certain (unsafe) failure rates will be archived rather then an absolute assurance? We know that checks before putting safety signalling facilities into service as well as the results of tests are essential but time consuming without guaranty of exhaustiveness in particular for the case of computerised equipments. In the context of greater economic constraints and increasing complexity of computerized tools, the capacities of the classic approval process are today attained. We see in actual practice a reduction of the validation cover rate and more and more numerous unsafe failures as results. This paper assumes that it is possible in practice to give an exhaustive formal proof that the “functional” of the signalling application (functional “white box”) is safe in the context of use (over-system). The presented method makes it possible, after a rigorous and cost effective design, to validate formally the “functional” software of critical computerized systems. The aim of our project was to provide the SNCF (today for delegated infrastructure manager, and tomorrow for rolling stock departments of railway undertaker) with an operating method for the formal validation of critical computerized systems, especially for the Interlocking and ETCS/ERTMS systems. A formal proof method by assertion, applicable to these critical systems, 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 time and does not show superfluous conditions: it replaces the platform checks and is in accordance with the existing SNCF testing procedures. The advantages are a significant reduction of testing time and of the related costs, an increase of the tests cover rate (deterministic safety vs. probabilistic safety), The paper assumes that the formal methods mastery by infrastructure engineers is a main key to prove that, during the life of the system, more safety is not more expensive.