In railways, computer-based interlocking (CBI) systems are safety critical systems, and should be proved that there is no defect leading to catastrophes during their whole life cycles. Runtime verification is able to provide on-going protection during the operational phase. Unfortunately, as being a variantrich system, it is hard to build monitors for CBI with standard runtime verification frameworks. To overcome this shortcoming, we propose parametric timed automata (PTA) to build feature models for the system. We prove that the language of PTA has more expressive power than timed automata. Based on PTA, we build monitors for a concrete CBI used in Beijing Metro Line 7. The experiment results show that complicated variant-rich CBI systems can be specified with a unique PTA feature model, and monitors can be quickly derived from the model by assign values to parameters. Therefore, this approach is feasible for monitoring CBI systems.


    Zugriff

    Zugriff prüfen

    Verfügbarkeit in meiner Bibliothek prüfen

    Bestellung bei Subito €


    Exportieren, teilen und zitieren



    Titel :

    Runtime Verification of Railway Interlocking Software with Parametric Timed Automata


    Beteiligte:
    Chai, Ming (Autor:in) / Wang, Haifeng (Autor:in) / Zhang, Jian (Autor:in) / Tang, Tao (Autor:in)


    Erscheinungsdatum :

    01.12.2018


    Format / Umfang :

    516623 byte




    Medientyp :

    Aufsatz (Konferenz)


    Format :

    Elektronische Ressource


    Sprache :

    Englisch



    Runtime Verification of Communications-based Train Control with Parametric Hybrid Automata

    Chai, Ming / Wang, Haifeng / Liu, Hongjie et al. | IEEE | 2019


    Verification of railway interlocking systems

    Simon Busard / Quentin Cappart / Christophe Limbrée et al. | DOAJ | 2015

    Freier Zugriff

    Verification of railway interlocking systems

    Busard, Simon / Cappart, Quentin / Limbrée, Christophe et al. | ArXiv | 2015

    Freier Zugriff

    Verification of Railway Interlocking - Compositional Approach with OCRA

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


    RAILWAY INTERLOCKING

    BEMMENT SAMUEL DAVID | Europäisches Patentamt | 2025

    Freier Zugriff