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.
Analysis on EURORADIO safety critical protocol by probabilistic model checking
01.08.2013
1168722 byte
Aufsatz (Konferenz)
Elektronische Ressource
Englisch
Performance Evaluation of Metro Regulations Using Probabilistic Model-Checking
British Library Conference Proceedings | 2019
|Synchronisation in Language-Level Symmetry Reduction for Probabilistic Model Checking
Springer Verlag | 2024
|Model-Checking Security Protocol with Propositional Projection Temporal Logic
British Library Online Contents | 2010
|