Research On Real-time Behavior Monitoring Method For On-board Controller Of Railway

Railway is an important component of China's public transportation system.With the improvement of railway transportation system and the increasingly complex function system,safety related issues are becoming more and more prominent.Meanwhile,the train control system is a complicated system which integrates control,communication,computation and signaling.At present,the traditional test and verification methods for the safety verification of train operation control system have their limitations.Runtime verification has emerged as a light-weight formal verification technique which combines traditional test and model checking methods.It can effectively reduce the complexity of verification and improve the efficiency.Currently,the monitoring of linear temporal logic(LTL)is widely researched in this area.However,LTL can only be used for monitoring the state sequence of the system execution trace,but not for the real-time properties of the system.This thesis focuses on the verification of real-time properties of the system.Firstly,the basic theory knowledge of runtime verification is deeply researched.We summarize the characteristics of runtime verification and show two specific monitoring techniques in the area.Also,we discusse their applications in the safety verification of train control system.Secondly,Due to the limited ability of expression,LTL can not be used for the monitoring of real-time propeities of the systems.Therefore,we propose the rewriting semantics of metric temporal logic(MTL)and time propositional temporal logic(TPTL)which can describe the explicit time constraint properties.Based on these semantics,we present new algorithms for the monitoring of MTL and TPTL.These methods enrich the performance of monitoring requirements and can monitor the time-constraint traces of the real-time system,which overcomes the poor expression ability of LTL for real-time properties.Finally,in order to verify the real-time properties of the system more conveniently,we develop runtime verification software which encapsulated a low-level rewriting tool(Maude).To verify the On-Board Controller of the railway,the interface of data transmission with the semi-physical platform in the laboratory is developed.Thus,we can receive the actual datas of the running train and extract the properties according to the high-level specification of the system.We demonstrate the verification and analysis using the monitoring algorithms presented in this thesis.In addition,we verify some important scenes of CTCS-3 train control system,which show the feasibility of the algorithms and their applications in the train control area.