Communication-based Train Control (CBTC) system is a widely-used signaling system. There is an increasing demand for innovating the traditional ground-centric architecture. With the application of train-train communication, object control and other advanced techniques, Train-centric CBTC (TcCBTC) system is expected to be the most promising tendency of train control system. The safe tracking interval would be reduced as well as the life-cycle costs. Formal methods play an essential role in the development of safety-critical systems, which provides an early integration of the verifiable design process. In the paper, the architecture design of TcCBTC is first analyzed. The official system specification of TcCBTC has not issued, so it takes efforts to perform the systematic summarization of the functional requirements. Secondly, we propose an integrated framework that combines the Colored Petri Net (CPN) models with the functional safety verification of the underlying systems. Functional safety depends on the logic accuracy and is a part of overall safety. The framework also specifies what kinds of functions, behaviors or properties need to be verified. The train control procedure of TcCBTC is regarded as the link among new functional modules, thus it is chosen as the modelling content. Thirdly, the scenarios and the color sets are prepared. Models are established with the novel design thought from top to bottom. Simulation and testing are implemented during the model establishment to discover the apparent errors. Lastly, the model checking by state space is performed. All possible states are checked in detail. Standard behavioral properties and other user-defined properties are verified by state space report and ASK-CTL (Computation Tree Logic) queries, respectively. Verification results reveal that the models are reasonable to depict the dynamic behaviors of train control procedure. The functional safety properties are satisfied and prepared for further drafting the system functional specification.


    Access

    Download


    Export, share and cite



    Title :

    Functional safety verification of train control procedure in train-centric CBTC by colored petri net


    Contributors:
    Junting Lin (author) / Qian Xu (author)


    Publication date :

    2020




    Type of media :

    Article (Journal)


    Type of material :

    Electronic Resource


    Language :

    Unknown




    Safety monitor for train‐centric CBTC system

    Wang, Haifeng / Zhao, Ning / Ning, Bin et al. | Wiley | 2018

    Free access

    Safety monitor for train-centric CBTC system

    Wang, Haifeng / Zhao, Ning / Ning, Bin et al. | IET | 2018

    Free access

    Train-Centric CBTC Meets Age of Information in Train-to-Train Communications

    Wang, Xiaoxuan / Liu, Lingjia / Zhu, Li et al. | IEEE | 2020


    Architecture Design of a Novel Train-centric CBTC System

    Chen, Tan / Wang, Haifeng / Ning, Bin et al. | IEEE | 2018