A method for formal proof by assertion is presented in this paper, which is applicable to industrial automatisms such as interlocking systems. This kind of application needs a SIL4 (Safety Integrity Level) real time machine, is strictly deterministic and based on a real time interpretation of the specification (functional Petri nets). This method is using a formal proof by assertion, which covers equally the specification and its real software implementation. The method is now under industrialization for the existing French PIPC (computerized interlocking system with personal computers ) and, later on, for the new future system under development. The tool is able to validate formally new systems or evolutions of existing systems with a better safety level as currently used manual procedures. The safety properties have been written in a general way and are parameterised to validate each interlocking system. Upstream the proof tool, a tool masterminds automatically the safety properties from the topologic description of the tracks and the signalling. Down river the proof tool, a tool generates the system states tree, marks the system transitions which don't follow the safety properties or show overabundant conditions. All this information makes it possible to realise the correct end of the proof or determine the reason for the safety property violation. This method can easily be included in the existing SNCF testing procedures. The algorithms defined allow providing the tools with a security level so that all the tests fulfil their own requested security level.


    Zugriff

    Zugriff über TIB

    Verfügbarkeit in meiner Bibliothek prüfen

    Bestellung bei Subito €


    Exportieren, teilen und zitieren



    Titel :

    Feasibility study for the implementation of a formal proof of interpretable specification (for an interlocking system)


    Beteiligte:
    Antoni, M. (Autor:in) / Ammad, N. (Autor:in) / Maillot, P. (Autor:in)


    Erscheinungsdatum :

    2007


    Format / Umfang :

    9 Seiten, 7 Bilder



    Medientyp :

    Aufsatz (Konferenz)


    Format :

    Print


    Sprache :

    Englisch






    Formal Methods for Industrial Interlocking Verification

    Chadwick, Simon / James, Phillip / Roggenbach, Markus et al. | IEEE | 2018


    Interlocking condition configurable implementation method, interlocking system and electronic equipment

    GUO SIWEN / ZHANG LIFENG / NIE ZHIGUO et al. | Europäisches Patentamt | 2023

    Freier Zugriff

    Principles of formal verification of interlocking software

    Pavlovic, O. / Pinger, R. / Kollmann, M. et al. | Tema Archiv | 2007