Quantitative safety analysis of train control system based on statistical model checking

Junting Lin; Xiaoqin Min

doi:10.5604/01.3001.0015.8147

Authors

Junting Lin University, School of Automation and Electrical Engineering, Lanzhou Author https://orcid.org/0000-0002-5763-5256
Xiaoqin Min University, School of Automation and Electrical Engineering, Lanzhou Author https://orcid.org/0000-0002-3374-4108

DOI:

https://doi.org/10.5604/01.3001.0015.8147

Keywords:

train control systems, statistical model checking, safety analysis, hybrid automata, UPPAAL-SMC

Abstract

With the rapid development of communication technology, the Train-centric Communication-based Train Control (TcCBTC) system adopting the train-train communication mode to reduce the transmission link of control information, will become the direction of urban rail transit field development. At present, TcCBTC system is in the stage of key technology research and prototype development. Uncertain behavior in the process of system operation may lead to operation accidents. Therefore, before the system is put into use, it must undergo strict testing and security verification to ensure the safe and efficient operation of the system. In the paper, the formal modeling and quantitative analysis of train tracking operation under moving block are carried out. Firstly, the structure of TcCBTC system and the train tracking interval control strategy under moving block conditions are analyzed. The subsystem involved in train tracking and the uncertain factors in system operation are determined. Then, based on the Stochastic Hybrid Automata (SHA), a network of SHA model of train dynamics model, communication components and on-board controller in the process of train tracking is established, which can formally describe the uncertain environment in the process of system operation. UPPAAL-SMC is used to simulate the change curve of train position and speed during tracking, it is verified that the model meets the safety requirements in static environment. Finally, taking Statistical Model Checking (SMC) as the basis of safety analysis, the probability of train collision in uncertain environment is calculated. The results show that after accurately modeling the train tracking operation control mechanism through network of SHA, the SMC method can accurately calculate the probability of train rearend collision, which proves that the method has strong feasibility and effectiveness. Formal modeling and analysis of safety-critical system is very important, which enables designers to grasp the hidden dangers of the system in the design stage and safety evaluation stage of train control system, and further provides theoretical reference for the subsequent TcCBTC system design and development, practical application and related specification improvement.

References

Bao, Y. X., Chen, M., Zhu, Q., et al. (2017). Quantitative performance evaluation of uncertainty-aware hybrid AADL designs using statistical model checking, IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems, 36(12), 1989-2002.

Basile, D., Beek, M. H., Ferrari, A., et al. (2019). Modelling and analysing ERTMS L3 moving block railway signalling with SIMULINK and UPPAAL SMC, Formal Methods for Industrial Critical Systems - 24th International Conference (FMICS). Amsterdam, The Netherlands, 1-21.

Chen, T. (2019). Research on safety protection methods of train-centric CBTC system. Beijing: Bejjng Jiaotong University.

Chrzan, M., (2021). Study of the possibility of using transmission in the LTE system on a selected railway line for the purpose of running railway traffic. Archives of Transport, 57(1), 91-101.

David, A., Du, D., Larsen, K. G., et al. (2012). Statistical model checking for stochastic hybrid systems. Electronic Proceedings in Theoretical Computer Science, 92, 187-199.

David, A., Larsen, K. G., Legay, A., et al. (2015). UPPAAL SMC tutorial. International Journal on Software Tools for Technology Transfer, 17(4), 397-415.

Du, D. H., Cheng, B., Liu, J. (2015). Statistical model checking for rare-event in safety-critical system. Journal of Software, 26(2), 305-320.

Gao, C. H. (2018). Communication-based Train Control System. China Railway Publishing House. Beijing, (Chapter 2).

Guo, H. N. (2019). Online testing safety function of new train control system on-board ATP. Beijing: Beijing Jiaotong University.

Guo, S. N., Wu, X. C. (2018). Safety assessment of TSR processing function in train control center based on evidence theory. Railway Standard Design, 62(06), 156-160.

Lin, J. T, Min, X. Q. (2021). Modeling and analysis of TcCBTC movement authority based on statistical model checking. Control Engineering of China, (20210119), 1-8.

Lin, J. T., Xu, Q. (2020). Functional safety verification of train control procedure in train-centric CBTC by colored petri net. Archives of Transport, 54(2), 43-58.

Liu, J. T., (2015). A safety analysis method for high-speed railway train control system in requirements phase based on STPA. Beijing: Beijing Jiaotong University.

Pan, D., Luo, Q., Zhao, L. T., et al. (2018). A new calibration method for the real-time calculation of dynamic safety following distance under railway moving block system. Mathematical Problems in Engineering, 2018(PT.10): 3061034. 1- 3061034.11.

Qiao, S., Huang, Z. Q., Wang, J. Y., et al. (2020). DFT quantitative analysis method based on statistical model checking. Systems Engineering and Electronics, 42(02), 480-488.

Wang, H. F, Zhao, N., Ning, B., et al. (2018). Safety monitor for train-centric CBTC system. IET Intelligent Transport Systems, 12(8), 931- 938.

Wang, X., Liu, L., Tao, T., et al. (2018). Enhancing communication-based train control systems through train-to-train communications. IEEE Transactions on Intelligent Transportation Systems, 20(4), 1-18.

Wu, D. H., Schnieder, E. (2016). Scenario-based modeling of the on-board of a satellite-based train control system with colored petri net. IEEE Transaction on Intelligent Transportation System, 17(11), 3045–3061.

Yang, J. F., Zhang, Y. P. (2016). Reliability analysis on ATP system of CTCS-3 based on D-S evidence inference and Bayesian network. International Journal of Control and Automation, 9(7), 59-70.

Yao, D. Y. (2018). Reliability analysis of next generation train control data communication system based on DSPN. Beijing: Beijing Jiaotong University.

Zhang, F., Bu, B., Zhao, J. Y. (2020). Risk assessment method for information safety of train operation control system. China Safety Science Journal, 30(S1), 172-178.

Zhang, Z. H., Wang, Y. R., Dang, J. W. (2020). Reliability analysis of on-board subsystem of train control system based on evidence theory and Bayesian network method. Journal of Railway Science and Engineering, 17(09), 2208-2215.

Zhao, M. Y., Chen, X. H., Sun, H. Y., et al. (2020). Formalizing railway interlocking domain specific language. Journal of Software, 31(06), 1638-1653.

Zhu, L., Yao, D. Y., Zhao, H. L. (2018). Reliability analysis of next generation CBTC data communication systems. IEEE Transactions on Vehicular Technology, 68(3), 2024-2034.