Ensuring the correctness of computer systems used in life-critical applications is very difficult. The most commonly used verification methods, simulation and testing, are not exhaustive and can miss errors. The work describes an alternative verification technique based on symbolic model checking that can automatically and exhaustively search the state space of the system and verify if properties are satisfied or not. The method also provides useful quantitative timing information about the behavior of the system. The authors have applied this technique using the Verus tool to a complex safety-critical system designed to control medium and large-size railway stations. They have identified some anomalous behavior in the model with serious potential consequences in the actual implementation. The fact that errors can be identified before a safety-critical system is deployed in the field not only eliminates sources of very serious problems, but also makes it significantly less expensive to debug the system.


    Zugriff

    Zugriff über TIB

    Verfügbarkeit in meiner Bibliothek prüfen

    Bestellung bei Subito €


    Exportieren, teilen und zitieren



    Titel :

    Verification of a safety-critical railway interlocking system with real-time constraints


    Beteiligte:
    Hartonas-Garmhausen, V. (Autor:in) / Campos, S. (Autor:in) / Cimatti, A. (Autor:in) / Clarke, E. (Autor:in) / Giunchiglia, F. (Autor:in)


    Erscheinungsdatum :

    1998


    Format / Umfang :

    6 Seiten, 12 Quellen




    Medientyp :

    Aufsatz (Konferenz)


    Format :

    Print


    Sprache :

    Englisch




    Verification of Railway Interlocking - Compositional Approach with OCRA

    Limbrée, Christophe / Cappart, Quentin / Pecheur, Charles et al. | British Library Conference Proceedings | 2016



    Novel Online Safety Observer for Railway Interlocking System

    Wang, Haifeng / Xu, Tianhua / Yuan, Tangming | ASCE | 2013


    Novel Online Safety Observer for Railway Interlocking System

    Wang, H. / Xu, T. / Yuan, T. | British Library Online Contents | 2013


    Runtime Verification of Railway Interlocking Software with Parametric Timed Automata

    Chai, Ming / Wang, Haifeng / Zhang, Jian et al. | IEEE | 2018