The EURORADIO system provides communication services for safety-related application processes using open network. The EURORADIO protocol controls the establishment of safety connection between on-board and trackside, and the time for establishment of safety connection is a key parameter to communication system. After describing the requirements in the EURORADIO specification, the probabilistic model checking tool PRISM is used to implement a formal analysis on the property of safety connection, combing the stochastic characters of communication channel. Verification results show that, when the protocol is applied in China Train Control System level 3 in case of 0.01 of message loss, the probability for establishment of safety connection in 8.5 seconds is 0.96059, and the probability is 0.99844 after establishing safety connection twice, it can fulfill the requirements of the specification.


    Zugriff

    Zugriff prüfen

    Verfügbarkeit in meiner Bibliothek prüfen

    Bestellung bei Subito €


    Exportieren, teilen und zitieren



    Titel :

    Analysis on EURORADIO safety critical protocol by probabilistic model checking


    Beteiligte:
    Quan, Hongyu (Autor:in) / Zhao, Huibing (Autor:in) / Zhou, Guo (Autor:in)


    Erscheinungsdatum :

    01.08.2013


    Format / Umfang :

    1168722 byte




    Medientyp :

    Aufsatz (Konferenz)


    Format :

    Elektronische Ressource


    Sprache :

    Englisch



    Probabilistic model checking applied to autonomous spacecraft reconfiguration

    Nardone, Vittoria / Santone, Antonella / Tipaldi, Massimo et al. | IEEE | 2016


    Performance Evaluation of Metro Regulations Using Probabilistic Model-Checking

    Bertrand, Nathalie / Bordais, Benjamin / Hélouët, Loïc et al. | British Library Conference Proceedings | 2019


    Synchronisation in Language-Level Symmetry Reduction for Probabilistic Model Checking

    Valkov, Ivaylo / Donaldson, Alastair F. / Miller, Alice | Springer Verlag | 2024



    Model-Checking Security Protocol with Propositional Projection Temporal Logic

    Yang, C. / Duan, Z. / Wang, X. | British Library Online Contents | 2010