The communications-based train control (CBTC) is a typical safety-critical system that protects and directs train operations in urban rail transit. It is suggested to provide on-going safety protections for the automatic train protection, which is a kernel function of the CBTC. Runtime verification is a technique for monitoring system executions against safety requirements. A particular challenge in implementing of a runtime verification system for the CBTC is the appropriate monitor specification. This paper presents a novel dynamic monitoring generation method to the problem. The train control procedures of the CBTC is formalized by parametric hybrid automata (PHA), which introduces notations of parametric expressions for flow, transition conditions and invariants. With an observation, the PHA is instantiated to a standard hybrid automaton. The monitor specification is then generated automatically by calculating the reachable set of the automaton with respect to some selected safety-related properties. The presented method is evaluated in a hard-ware in the loop CBTC platform, which is developed with realistic engineering data of Beijing Yizhuang metro line. The experiment results show that the approach is feasible, and various dangerous of the CBTC system are prevented from developing into accidents of train collisions.


    Access

    Check access

    Check availability in my library

    Order at Subito €


    Export, share and cite



    Title :

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


    Contributors:
    Chai, Ming (author) / Wang, Haifeng (author) / Liu, Hongjie (author) / Lv, Jidong (author) / Hu, Qian (author)


    Publication date :

    2019-10-01


    Size :

    871871 byte




    Type of media :

    Conference paper


    Type of material :

    Electronic Resource


    Language :

    English



    Runtime Verification of Railway Interlocking Software with Parametric Timed Automata

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



    Runtime Verification

    Alwyn E Goodloe | NTRS


    Logical verification and systematic parametric analysis in train control

    Platzer, Andre / Quesel, Jan-David | Tema Archive | 2008


    DANGER PREDICTION METHOD AND SYSTEM OF TRAIN SCHEDULING OPERATION BASED ON RUNTIME VERIFICATION

    CHAI MING / SU HAOXIANG / LIU HONGJIE et al. | European Patent Office | 2023

    Free access