Research On Dynamic Monitoring Method Of Route Control Based On Runtime Verification

Train-centric train control system has been paid more and more attention in the field of rail transit signalling.Compared with traditional train control systems,parts of the route control and interlocking logic functions are integrated into the on-board equipment,and the track-side equipment are simplified to the maximum extent.Although this improves the level of vehicle intelligence,it also increases the challenges and risks of the system.Due to the safety-critical characteristic of the new train control system,any failure may lead to significant personal casualties and economic losses,so how to ensure the safe operation of such systems is particularly important.Runtime verification,as a lightweight formal method,can effectively reduce the complexity of analysis and verification,and provide additional protection for the safe operation of the system.However,the traditional runtime verification method has the problem of insufficient ability to describe the monitoring properties.Therefore,this thesis studies a new dynamic monitoring method based on runtime verification,and discusses the effectiveness of the method combined with the route control function of the new train control system.The main work of this thesis is as follows:(1)A construction framework of dynamic monitor based on runtime verification is proposed.By establishing a parametric model of the system,the monitoring properties expressed by MTL(Metric Temporal Logic)are extracted from the model,and then the monitor is constructed.The monitor determines whether the execution sequence of the system satisfies the monitoring properties,thus realizing the dynamic monitoring of the system runtime behavior.(2)An extended parametric timed automaton modeling language is proposed.Based on the traditional timed automaton,the parameterized extension is carried out,which enhances the ability of the language to express the parametric model of the system.At the same time,the MTL verification algorithm based on formula rewriting is analyzed,and the real-time properties of the system are verified by the algorithm.(3)The principle of route control for the new train control system is analyzed.Based on the realization process of route control under this principle,the system model is established by using extended parametric timed automaton modeling language.The model is simulated and verified to ensure the functional,real-time and security requirements.(4)Based on the equivalence relationship between automaton model and sequential logic language,the extraction rules of the monitoring properties are given.Aiming at the limitation of Maude verification,a tool that can automatically implement runtime verification is developed and used to monitor the implementation processes of route control in two typical operation scenarios.The results show that the dynamic monitoring method proposed in this thesis can effectively improve the quality of monitoring properties and the ability of the monitor to detect system errors.In this thesis,the problem of insufficient ability of traditional runtime verification to describe the monitoring properties is improved,the combinatorial explosion in the process of modeling is avoided,and the flexibility and construction efficiency of the monitor are improved.The study has certain referential significance for ensuring the correctness and security of the route control function for the new train control system.