Online hazard prediction of train operations with parametric hybrid automata based runtime verification

• DOI: 10.1016/j.ress.2023.109621
• Publication Date: 2023-09-04T04:59:15Z
• Authors: Ming Chai; Xinyi Zhang; Bernd-Holger Schl...; Tao Tang; Hongjie Liu
• Keywords: System safety; Runtime Verification

Automatic train control systems are complex and software-intensive cyber–physical systems. Hazard prediction at runtime for such has emerged as an essential research topic. Since hazards in operations have a wide range of causal factors, the current monitoring approaches based on pre-programmed safety properties generally ineffective guaranteeing system safety. This paper proposes reachable set-based verification approach. In this approach, top-level operation predicted directly by analysing all possible time-position states from observation. First, model is formalised with parametric hybrid automata (PHA) to capture discrete-continuous mixed multi-variant features operations. Then, refinement algorithm proposed over-approximation linearisation method reduce computational complexity. The set refined computed well-developed tool SpaceEx. We prove that approximation approach does not compromise hazard ability. Furthermore, concrete example Beijing Yizhuang metro line, we analyse feasibility practice. results indicate high performance accuracy predicting improves