Modeling And Safety Analysis Of TcCBTC System Based On Statistical Model Checking

With the rapid development of train control technology and the increase of people’s travel demand,urban rail transit is moving towards the goals of high intelligence,high density and high safety.Researchers from various countries have actively carried out the research and development of new train control systems,among which the Train-centric Communication Based Train Control(TcCBTC)system has become a research hotspot.It adopts train-train communication technology to simplify the interaction link of control information.It optimizes the system structure through the redistribution of train control functions,thus improving the intelligence of vehicle and reducing the system life cycle cost.At present,TcCBTC system is in the stage of core technology breakthrough and prototype development.Uncertain behaviors in the system operation process may affect the driving safety.Therefore,the system must undergo strict safety verification to ensure the safe and efficient operation of the system before it is put into use.This thesis puts forward the formal modeling and safety analysis framework of TcCBTC system based on Stochastic Hybrid Automata(SHA)theory as the modeling basis and Statistical Model Checking(SMC)as the safety analysis basis.On this basis,the selected examples are analyzed by UPPAAL-SMC to verify the effectiveness of the method.The research work is as follows:(1)It introduced the research status of TcCBTC system at home and abroad,and deeply analyzed the structure,functions of each subsystem.The structure reference model of TcCBTC system is established.The communication interface of the system and the information exchanged by each subsystem through the interface are analyzed.The model-based method combined with HAZOP-I method is applied to identify the risks in the process of system operation,that is to analyze the uncertain environment of system operation,which provides a basis for subsequent modeling.(2)The research status of formal modeling and verification methods of train control system at home and abroad is analyzed,and the model-based safety analysis method and model checking technology are briefly described.A formal modeling method based on SHA was proposed to describe the hybrid behavior and random behavior of TcCBTC system aiming at the uncertainty of TcCBTC system operating environment.DMTL semantics is used to describe the verified properties,the formal model of the system is established through UPPAAL-SMC,and the security of TcCBTC system is analyzed based on the statistical model detection idea.(3)Case studies on TcCBTC system operation scenario were investigated.Taking the movement authority scenario and train tracking as examples,the functional requirements of the system in each scenario are analyzed.The subsystems involved in the process and their interactive information,and the uncertain factors in the system operation are determined.Then,a network of SHA model containing the uncertain operating environment of the system is established.On the basis of verifying that the built model meets the requirements of system functional attributes in the static environment,quantitative analysis of the system model in UPPAAL-SMC based on SMC algorithm is carried out.The influence of uncertain factors on the system is verified,and the feasible region of parameters under the corresponding quantitative index is obtained through fitting,so as to realize the real-time monitoring of train state and improve system security.