Model-based verification method for solving the parameter uncertainty in the train control system. (January 2016)

• Record Type: Journal Article
• Authors: Cheng, Ruijun; Zhou, Jin; Chen, Dewang; Song, Yongduan
• Is Part Of: Reliability engineering & system safety. Volume 145(2016:Jan.)
• Page Start: 169
• Page End: 182
• Publication Date: 2016-01
• Subjects: Parameter uncertainty -- System safety verification -- Linear hybrid automata -- Reachable state analysis -- Stochastic time petri nets -- High-speed train control system; Reliability (Engineering) -- Periodicals; System safety -- Periodicals; Industrial safety -- Periodicals; Fiabilité -- Périodiques; Sécurité des systèmes -- Périodiques; Sécurité du travail -- Périodiques; 620.00452
• DOI: 10.1016/j.ress.2015.09.014
• Languages: English
• ISSNs: 0951-8320

Abstract

Abstract: This paper presents a parameter analysis method to solve the parameter uncertainty problem for hybrid system and explore the correlation of key parameters for distributed control system. For improving the reusability of control model, the proposed approach provides the support for obtaining the constraint sets of all uncertain parameters in the abstract linear hybrid automata (LHA) model when satisfying the safety requirements of the train control system. Then, in order to solve the state space explosion problem, the online verification method is proposed to monitor the operating status of high-speed trains online because of the real-time property of the train control system. Furthermore, we construct the LHA formal models of train tracking model and movement authority (MA) generation process as cases to illustrate the effectiveness and efficiency of the proposed method. In the first case, we obtain the constraint sets of uncertain parameters to avoid collision between trains. In the second case, the correlation of position report cycle and MA generation cycle is analyzed under both the normal and the abnormal condition influenced by packet-loss factor. Finally, considering stochastic characterization of time distributions and real-time feature of moving block control system, the transient probabilities of wireless communication process are obtained by stochastic time petri nets. Abstract : Highlights: We solve the parameters uncertainty problem by using model-based method. We acquire the parameter constraint sets by verifying linear hybrid automata models. Online verification algorithms are designed to monitor the high-speed trains. We analyze the correlation of key parameters and uncritical parameters. The transient probabilities are obtained by using reliability analysis.