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 die capacity of the classic approval process (manual or automatic). A reduction of the validation cover rate result in practice. This is not compatible in a industrial way. The method presented make 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 operating method for the formal validation of 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. With the proposed method and its associated tools it is completely verified that the system follows all safety properties at all time and does not show superfluous conditions: it replaces all the indoor 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 are surely a key to prove that more safety is not necessarily more expensive. The safety analysis of the state-of-the-art computer based railway interlocking systems is discussed. The fault-tree analysis is selected as a primary method to evaluate the failure behavior of the system. Since the hardware system and the functional tasks of the modern interlocking systems can be very complicated, automatic fault-tree generation is introduced, which provides faster analysis and models without human errors.


    Zugriff

    Zugriff über TIB

    Verfügbarkeit in meiner Bibliothek prüfen

    Bestellung bei Subito €


    Exportieren, teilen und zitieren



    Titel :

    Formal validation method and tools for computerized railway interlocking systems


    Weitere Titelangaben:

    Formales Validierungsverfahren und Werkzeuge für computer-gestützte Schienen-Sicherheitssysteme


    Beteiligte:
    Antoni, Marc (Autor:in) / Ammad, Nadia (Autor:in)


    Erscheinungsdatum :

    2008


    Format / Umfang :

    13 Seiten, 9 Bilder, 1 Tabelle, 4 Quellen



    Medientyp :

    Aufsatz (Konferenz)


    Format :

    Print


    Sprache :

    Englisch




    Formal Validation Method and Tools for French Computerized Railway Interlocking Systems

    Antoni, A.M. / Ammad, N. | British Library Conference Proceedings | 2008



    Validation of Railway Interlocking Systems by Formal Verification, A Case Study

    Bonacchi, A. / Fantechi, A. / Bacherini, S. et al. | British Library Conference Proceedings | 2014


    Computerized interlocking system for railway signaling control: SMILE

    Akita, K. / Watanabe, T. / Nakamura, H. et al. | Tema Archiv | 1985