Formal Modeling And Analysis Of CTCS-3 Train Control On-board Equipment Based On CPN

In recent years,with the continuous development of China’s railway industry,its role in transport operation can not be ignored,and ensuring the safety of train operation has become an important issue.At present,China Train Control System level 3(CTCS-3)is the most widely used on high-speed railways in China for trains running at speeds over 250km/h.For the CTCS-3 train operation control system,its core equipment is on-board equipment,which assumes the main control function of the train operation.Once the on-board equipment fails,it will have a serious impact on the train control system.Therefore,it is necessary to verify the safety of on-board equipment.According to the structure and function of the on-board equipment,the safety computer does most of the work.It controls the train according to the information received from other modules,and implements the braking command on the train when necessary.The modules that interact with the on-board equipment mainly include RBC,driver,balise and train,and the correctness of these modules should also be verified.The traditional method of model building can no longer satisfy the functional requirement analysis of complex system.Formal modeling verification method has become the main trend.The main research content of this thesis is to take the CTCS-3 on-board train control equipment as the research object,conduct modeling and verification of it,and analyze the safety of the system.Firstly,the UML static structure class diagram and dynamic behavior state diagram of the on-board equipment are constructed according to the structure and function of the on-board equipment as well as the analysis of the operation scenario.In this way,the analysis object and the transformation state of the object of the on-board equipment can be intuitively displayed,laying a foundation for the construction of the CPN model of the on-board equipment.Then,according to the requirements of existing system requirements specification file(SRS)standard,the CPN model of information interaction between on-board devices,the top-level CPN model and sub-page CPN model of working mode transformation,as well as the CPN model of several peripheral environment modules(RBC,driver,transponder,train)for information interaction with on-board devices are constructed.The CPN model is validated from two aspects.Dynamic attribute verification is to obtain the dynamic attribute verification report through the state space analysis of the model and analyze the characteristics of the system.Systematic verification is to use ASK-CTL branch time-sequence logic formula to describe the properties of the system,such as the self-loop terminal characteristics of the system,deadlock characteristics,to prove whether the system model is executable.The verification results show that the modeling of on-board equipment conforms to the specification of system requirements and the interaction between components conforms to the specification process.The modeling and verification of the system are all under the normal working state of the system.However,the safety should be ensured even when some components of the system do not work normally.Therefore,the algorithm of fault injection technology is adopted to analyze the safety of the system by injecting the fault into the normal system.The analysis results show that the safety performance of the system meets the safety requirements,which provides a reference for the formal modeling and safety analysis of the train control system in the future.