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.


    Access

    Check access

    Check availability in my library

    Order at Subito €


    Export, share and cite



    Title :

    Runtime Verification of Railway Interlocking Software with Parametric Timed Automata


    Contributors:
    Chai, Ming (author) / Wang, Haifeng (author) / Zhang, Jian (author) / Tang, Tao (author)


    Publication date :

    2018-12-01


    Size :

    516623 byte




    Type of media :

    Conference paper


    Type of material :

    Electronic Resource


    Language :

    English



    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

    Free access

    Verification of railway interlocking systems

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

    Free access

    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 | European Patent Office | 2025

    Free access