Formal Modeling And Verification Analysis Of Medium Speed Maglev Vehicle Control System

With the maglev line in Changsha and Beijing "S1 line" have been opened up,set off a boom in magnetic levitation and research.Changsha Maglev Express and Beijing"S1 Line" are short stator linear induction motor drive,the maximum operating speed is generally not more than 120km/h.In order to improve the running speed of medium and low speed maglev train,the 13th Five-Year Science and Technology Major Proposal put forward a long-stator synchronous traction medium speed maglev program.For this new scheme,the subsystems of the maglev,including the operational control system,need to be re-engineered and the vehicle running control system also needs to be adapted accordingly as part of the operational control system.At the same time,it needs to be pointed out that in the process of localization,follow the technological route abroad or combine the latest technological development trend,there are many disputes using the new architecture and protocol.This paper aims to use the method of formal analysis,to study in theory,to do some discussion for a new generation of medium-speed meglev vehicle operation control system.This paper presents a new solution for medium-speed magnetic levitation vehicle positioning system,vehicular communication network and communication system to meet the needs of localization,and uses Petri nets to model and analyze the improved scheme.The feasibility of the new scheme is verified theoretically,the details are as follows:(1)A magnetic levitation vehicle positioning system based on multi-sensor information fusion is designed.Cross-induction loop technology is used to achieve absolute positioning.Kalman filtering is used to estimate the relative position of the global positioning system(GPS)and inertial navigation system(INS)information.Simulation results of the maglev communication system using Matlab show that Positioning accuracy to meet the requirements,and the use of Petri nets modeling of the overall positioning system to prove that the program positioning system failure rate in line with the standards.(2)Maglev automotive communication network based on CANOpen bus technology and Industrial Ethernet Ethernet Powerlink technology is designed.Found the inadequacies of the original vehicle communication network program and proposed improvement programs,and at the same time designed the corresponding maglev vehicle network communication frame format through the magnetic levitation vehicle signal.Finally,the simulation of the original vehicle network system and the improved vehicle network system were modeled separately,and the verified system non-failure rate of the improved plan was obviously better than the original one.(3)The principle of magnetic levitation communication system was researched.The existing wireless communication system was changed from 38G millimeter-wave technology to long-term evolution technology(LTE).According to the principle of colored Petri net,the original communication system and the improved communication system were modeled,By comparing the two models,it is concluded that the communication delay of the improved communication system and the failure rate of information transmission can reach the standard.