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

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