Modeling and Quantitative Safety Analysis of Chinese Train Control System of Systems

In order to perform the quantitative safety analysis of Chinese Train Control System level 3, Markov Decision Process(MDP) is employed as the foundation of system behavior modelling. The non-deterministic behaviors and stochastic behaviors in physical behavior model, normal behavior model and fault behavior models are all expressed in MDPs. The quantitative analysis results produced by probabilistic model checker PRISM can be used to judge and compare the prototype designs and evaluate the probabilistic risk of hazards. The conclusions show that comprehensive behavior model and PRISM can automatically consider all the paths of the dynamic system behaviors in System of Systems, which makes the behavior model more accurate and complete. The methodology manifests that it is applicable for the safety analysis of CTCS3 and other train control systems.