Runtime Monitoring Of Train Control System For Overspeed Protection Based On Hybrid Automata

The train control system has the characteristics of distribution,dynamic,multi-scene fusion and so on.Defects in system design are hard to be fully eliminated during the development phase.Therefore,runtime monitoring is required after the system deployment and leads the system to its safe side when danger occurs.Runtime verification uses a formal language to describe monitoring specifications that the system expects to satisfy and detects danger of the system with a monitor by checking whether runtime executions meet the monitoring specifications,so as to perform the runtime monitoring.Monitoring specifications of the overspeed protection function include complicated hybrid behaviors and are highly dependent on the running environment of trains.The conventional runtime verification methods are hard to build effective monitoring specifications of the overspeed protection function.Therefore,the research on the building method for monitoring specifications of the overspeed protection function is significant.The main work of the paper is as follows:(1)The building method for the dynamic monitoring specification of the overspeed protection function is proposed.A parameterized hierarchical model of train control is established by a hybrid automaton.The reachable set of the model is computed with respect to a top-level safety requirement of the overspeed protection function,"the train reaches the end of authority,the train speed is not greater than zero".The part of the reachable set that meets the safety requirement is the dynamic monitoring specification of the overspeed protection function.Since the reachable set changes with the executions of trains,the established monitoring specification of the overspeed protection function is dynamic.(2)An algorithm based on deep learning and spline regression for calculating the speed monitoring curves is proposed.Based on this algorithm,the calculation platform of the speed monitoring curve is built,which can interact with the parameterized hierarchical model of train control in real time to realize the calculation function of the speed monitoring curve in the model.This method is used to improve the automation and accuracy of the dynamic monitoring specification in different train running environments.(3)An online runtime monitoring prototype system of the overspeed protection function is developed with hybrid automata verification theories.The runtime monitor of the overspeed protection function periodically receives the runtime executions from the train control system and the curve parameters from the calculation platform of the speed monitoring curve,in order to instantiate the hierarchical model of train control,and then determines whether the runtime executions of the system conform to the dynamic monitoring specification.(4)Two typical dangerous scenarios of the train control system are monitored.The monitoring effectiveness of the proposed method in this paper is verified by comparing it with the conventional methods.The experimental results show that the proposed novel monitoring method is able to reduce false alarm rates and fail alarm rates significantly,and has high verification efficiency,which can detect danger in advance and protect trains to stop within the movement authority areas.The proposed building method for the dynamic monitoring specification of the overspeed protection function based on hybrid automata is able to exhaustedly verify all possible subsequent running behaviors of the system starting from the runtime executions.Therefore,the generated monitor based on this method has predictability.The research in this paper is significant to improve the safety of train operations.This paper has 48 figures,19 tables and 61 references.