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.


    Zugriff

    Zugriff prüfen

    Verfügbarkeit in meiner Bibliothek prüfen

    Bestellung bei Subito €


    Exportieren, teilen und zitieren



    Titel :

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


    Beteiligte:
    Guo Xie (Autor:in) / Xinhong Hei (Autor:in) / Mochizuki, H. (Autor:in) / Takahashi, S. (Autor:in) / Nakamura, H. (Autor:in)


    Erscheinungsdatum :

    01.11.2012


    Format / Umfang :

    219505 byte




    Medientyp :

    Aufsatz (Konferenz)


    Format :

    Elektronische Ressource


    Sprache :

    Englisch




    WAYSIDE TRAIN HOT BEARING DETECTION SYSTEM

    AGOSTINI ALESSANDRO / RICCI ANDREA / SCHÖNING BJOERN | Europäisches Patentamt | 2019

    Freier Zugriff

    Safety monitor for train‐centric CBTC system

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

    Freier Zugriff

    Safety monitor for train-centric CBTC system

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

    Freier Zugriff

    CBTC (Communication Based Train Control): system and development

    Bin, N. / Tao, T. / Min, Q. K. et al. | British Library Conference Proceedings | 2006