Topology Features Oriented Modeling And Verification Theoretical Method Of Train Control System

The train operational control system(hereinafter referred to as the train control system)is the core technical equipment to ensure the safety and improve the efficiency of railway transportation,and the "brain and nerve center" of railway transportation.With the application of computer and electronic equipment in the train control system,more and more safety-related control functions are carried by software,which makes the train control system show different characteristics from the traditional railway signal equipment.With the increasing complexity of the system and the increasingly frequent communication between subsystems,the system operation extends from the closed static environment to the open and dynamic distributed environment.There are a lot of uncertainties in the environment,which makes it very difficult to realize the accurate and safe control of train operation.With the further development of communication technology and computer intelligence technology,the future train control system will present the characteristics of integration,intelligence,automation,etc.The tight coupling of system functions,real-time dynamic adjustment of train control,and the emergence of fully automatic train operation further increase the difficulty of realizing safety control of the train control system.For the train control system under the new requirements,how to model its typical features,and conduct efficient verification for the complex large-scale train control system model behavior has become an urgent problem to ensure the safe operation of trains.Based on the train control system of the current high-speed railway and its future development trend,this thesis mainly studies the feature analysis,modeling,and verification methods based on the operation characteristics of the train control system,aiming at the safety guarantee of the train control system.Based on the characteristics of the train control system,a set of formal regulations applicable to the train control system are established to model the characteristics of the train control system,to make the system model close to the actual behaviors of a physical system to the maximum extent.Then,according to the established system model,an efficient verification method is proposed to solve the problem that the traditional verification method cannot verify the complex large-scale system,effectively solve the problem of design defects in the current system,and avoid the accidents caused by this.This dissertation carries out the following research work:(1)Ensuring the data correctness of the train control system is critical for the safety of the train operation.A graph-theory based unified train control data model and a verification method are proposed.Starting from the design concept of separating the data from the control logic of the train control system,the topology elements of the train control and the relationships among them are studied.The formalism of the train control static data is given.Based on the connections of train control topology elements,a unified data model of train control data based on graph-theory was established.Based on this model,several theorems for data safety verification are proposed and theoretical proofs are provided.In theory,it provides a formalized and accurate description method for train control logic data,which can effectively support the automatic verification of train control data.(2)Aiming at the issue of formal modeling train control logic,a novel formalism based on topological manifold theory of train safety control logic is proposed.Firstly,formal descriptions of the dynamic operation behavior curve and train operation limit curve of the train are given,the safety line condition is given based on the topological manifold representation.A formal representation of the movement authority logic of virtual coupling control system is given,theorems for the safety assurance of the logic are proved.The problem of formalizing control logic considering dynamic train behavior is solved based on the topological manifold theory.(3)Because of the traditional method cannot deal with the large-scale system verification problem,based on topological manifold theory,this dissertation proposes a runtime verification method which is suitable for safety control logic of train control system.On the basis of the safety logic formalism and the dynamic interval control logic of train control system,a set of theorems are proposed to verify the runtime data correctness,to verify the safety of train control logic and the safety of train control commands,theoretical proofs and algorithms are provided.The proposed method shows a novel approach to ensure the safety of the dynamic interval control logic of train control system.(4)Since it is difficult to verify the train control system considering its hybrid nature,a hybrid monitoring method for train overspeeding protection logic is proposed.The method is based on reachability analysis,which takes both continuous behavior and discrete state of train control system.A dynamic parameter model of the system is built based on the overspeeding protection principle of CTCS-3.The corresponding parameters of the model are updated in real time according to the train operation information,and the dynamic continuous monitoring of the train is realized by calculating the reachable set of the train operation behavior.The proposed mehtod improves the monitoring accuracy and provides an effective way for the train control system verification considering its hybrid nature.Based on the features of modern train control system,a set of modeling and verification methods are proposed for train control data and safety control logic.Experiments are conducted based on the real railway engineering data,the results show that the probolem to construct and verify the model of the data and the safety logic of train control system could be solved efficiently with the help of the method.The proposed method could also support the development of the train control system and ensure the safe operation of train control system.