In the development of communication based train control (CBTC) system, while communicating with the control center, the train must be assigned accurately to the wayside network. In order to verify the rigor of this process, the specification is analyzed formally in this paper. After studying the system, the functional requirements are clarified firstly. Followed by the formal specification is established by VDM explicitly, including the state variables and top-level operations. Then the internal consistence of the formal specification is validated, which can prevent potential runtime errors in software program. Lastly, in order to ensure that the specification satisfies requirements, the requirements are transformed to corresponding inference rules, and then validated by discharging proof obligations. The work in this paper indicates that if the software system of a CBTC system is designed strictly in accordance with the specification, it will be internal consistent with high reliability, and satisfy the design requirements.


    Access

    Check access

    Check availability in my library

    Order at Subito €


    Export, share and cite



    Title :

    Formalizing and Analyzing the Train-to-Wayside Network System for CBTC


    Contributors:
    Guo Xie (author) / Xinhong Hei (author) / Mochizuki, H. (author) / Takahashi, S. (author) / Nakamura, H. (author)


    Publication date :

    2012-11-01


    Size :

    219505 byte




    Type of media :

    Conference paper


    Type of material :

    Electronic Resource


    Language :

    English




    WAYSIDE TRAIN HOT BEARING DETECTION SYSTEM

    AGOSTINI ALESSANDRO / RICCI ANDREA / SCHÖNING BJOERN | European Patent Office | 2019

    Free access

    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