Parametric Spatio-temporal Modeling and Safety Verifying for T2T-CBTC Systems

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.