Formal Modeling And Verification Analysis Of High Speed Maglev Zoning Handover

Partition handover is an important function of the high-speed maglev operation control system.Train partition handover module is an important guarantee for the safe operation of the maglev train and a key module in the high-speed maglev operation control system.At present,the existing high-speed maglev lines,including the Shanghai Maglev Line,because the line is short,the zoning switching occurs in the low-speed area(speed below 120 km / h).However,the 600 km / h high-speed magnetic levitation developed locally in the 13 th Five-Year Plan will be applied to the long-distance trunk line.It is necessary to perform zone switching under the high-speed operation of 600km/h.When the train is required to stop in the current partition,this puts a high requirement on the wireless communication system that can hardly be achieved.The research goal of this paper is to propose a partition switching scheme suitable for high-speed situations,design the switching process and pass the formal analysis method Verify that the new handover scheme is reasonable and effective.The new scheme will reduce the requirements of the original scheme for wireless communication systems.The main work of the thesis is as follows:(1)Analyze the composition structure and working principle of the high-speed maglev train control system related to the zone handover,analyze the existing high-speed maglev zone switching scheme,and point out that the existing zone handover scheme exists through the calculation of the safety braking curve Problem,the existing zoning handover scheme is not suitable for high-speed zoning handover at 600 kilometers per hour.(2)Based on the shortcomings of the original scheme,a new zoning handover scheme is proposed and the difference between the new scheme and the existing scheme is compared.The new scheme changes the time sequence flow of the original scheme and eliminates the redundancy in the train handover process The system can reduce the number of communications while ensuring the communication quality,increase the redundancy of the on-board safety computer system,and improve the communication security.Based on this,the requirements of the original scheme for the wireless communication system can be reduced.(3)Introduce the petri principle,CPN modeling method and CPN modeling application in rail transit,use CPN to model the new scheme hierarchically,and use the top-down method to establish the high-speed maglev zone handover process respectively The system layer model of each stage,as well as the functional layer model of each subsystem responsible for data processing and the communication layer model responsible for data distribution,finally use CPN Tools to generate state space reports for model verification.(4)The modeling study of the communication layer model is carried out.Through the analysis of the simple communication layer model and the wireless communication failure model,the time loss and delay in the process of zone handover are calculated,and the impact of the zone switching on its efficiency is clearly defined factor.The new zoning handover solution was implemented by the research team as a module of the operation control system and passed the laboratory test.