TY - GEN
T1 - Parametric Spatio-temporal Modeling and Safety Verifying for T2T-CBTC Systems
AU - Zhao, Qianzhu
AU - Liu, Jing
AU - Chen, Xiang
AU - Li, Tengfei
AU - Sun, Junfeng
AU - Zhang, Lipeng
N1 - Publisher Copyright:
© 2021 IEEE.
PY - 2021/8
Y1 - 2021/8
N2 - Safety is critical for the new technology of the communication-based train control (CBTC) system, the train-to-train CBTC (T2T-CBTC) system, which establishes direct communication between trains. In this paper, we define a parametric spatio-temporal hybrid modeling language (StHML(p)), focusing on the extension of spatio-temporal elements and probability parameters, to model the T2T-CBTC system. The parameters are risk states which come from the uncertain environment. To this end, we present a safety-risk prediction method based on a deep recurrent neural network for the T2T-CBTC system, which takes into account highly imbalanced data of the system, to predict the risk states through environment data. To verify StHML(p) model, we propose a mapping algorithm to transform StHML(p) into NSHA (Networks of Stochastic Hybrid Automaton) and employe the statistical model checker UPPAAL-SMC for verifying quantitative properties. Finally, we implement our approach in an T2T-CBTC system.
AB - Safety is critical for the new technology of the communication-based train control (CBTC) system, the train-to-train CBTC (T2T-CBTC) system, which establishes direct communication between trains. In this paper, we define a parametric spatio-temporal hybrid modeling language (StHML(p)), focusing on the extension of spatio-temporal elements and probability parameters, to model the T2T-CBTC system. The parameters are risk states which come from the uncertain environment. To this end, we present a safety-risk prediction method based on a deep recurrent neural network for the T2T-CBTC system, which takes into account highly imbalanced data of the system, to predict the risk states through environment data. To verify StHML(p) model, we propose a mapping algorithm to transform StHML(p) into NSHA (Networks of Stochastic Hybrid Automaton) and employe the statistical model checker UPPAAL-SMC for verifying quantitative properties. Finally, we implement our approach in an T2T-CBTC system.
KW - deep learning
KW - formal modeling and verifying
KW - safety-risk prediction
KW - statistical model checking
KW - train-to-train communication-based train control system
UR - https://www.scopus.com/pages/publications/85116946861
U2 - 10.1109/TASE52547.2021.00032
DO - 10.1109/TASE52547.2021.00032
M3 - 会议稿件
AN - SCOPUS:85116946861
T3 - Proceedings - 2021 International Symposium on Theoretical Aspects of Software Engineering, TASE 2021
SP - 71
EP - 78
BT - Proceedings - 2021 International Symposium on Theoretical Aspects of Software Engineering, TASE 2021
PB - Institute of Electrical and Electronics Engineers Inc.
T2 - 15th International Symposium on Theoretical Aspects of Software Engineering, TASE 2021
Y2 - 25 August 2021 through 27 August 2021
ER -