Autonomous CTCS-3 Level Train Control System Added Scene Modeling And Safety Analysis

The autonomous CTCS-3 level train control system plays a vital role in ensuring the safe operation of high-speed rail trains.It has complete independent property rights,and has added a lot of content in software and hardware design and functional requirements.Therefore,how to ensure the safety and reliability of the train control system under the new specifications has become an important research topic.At the same time,which method is used to analyze the safety factors of the train control system is not involved in traditional research,and the formal method just makes up for this shortcoming,by selecting appropriate formal methods to model and analyze the safety of the train control system It has become the mainstream research trend of the current train control system safety assurance technology.This subject takes the autonomous CTCS-3 level train control system track circuit permit verification scenario as the research object,and uses two formal methods to carry out the research on the scenario.First,a modeling method based on time automata is proposed.Aiming at the real-time nature of the train control system,the work flow of each device of the control system is analyzed in the following scenes.After reasonable abstraction and simplification,the time automata theory is used to construct the track circuit license verification The time automata model of the scene,the interaction of each module is simulated in the UPPAAL simulator,and the safety function attribute and restricted activity are verified by the verifier,which proves the effectiveness of this modeling method,and finally combined with the Beijing-Shenzhen Passenger Special Liaoning Section test data,compile the test sequence related to the track circuit license verification scenario,and carry out simulation test verification through the autonomous CTCS-3 level train control system scenario controller.At the same time,the UML(Unified Modeling Language,Unified Modeling Language)extension mechanism is used to analyze the safety of track circuit license verification scenarios.In view of the hybrid nature of the train control system,the track circuit permit verification scenario is analyzed.According to the requirements of the UML extension mechanism for modeling,the early stage includes the construction of UML scenario class diagrams and state transition diagram models.For the state transition part and the state transition in the system The dynamic continuous process is combined with the failure expansion model to further describe its behavior,and the hybrid summary description file is established on the basis of the specification requirements of the train control system.Later,the established model is converted using the hybrid automata model inspection tool to analyze the track circuit driving permit Check and describe the possible faults in the verification scene,use the fault model fusion algorithm to fuse the PHAVer model and the fault model to describe the fault situation in the track circuit permit verification scenario and the impact of the scene function caused by the fault,use the fault monitor Begin to calculate the reachability set of the system model,and determine the combination of failure factors related to system safety to realize the safety analysis of the track circuit license verification scenario.The results show that the method proposed in this thesis can meet the safety characteristics requirements of the track circuit permit verification scenario in the train control system requirements design stage,and provide a reference method for the formal modeling and safety assessment of the train control system in the future.