Formal Modeling And Verification Of State Transformation Of Interval Block Partition Occupancy Logic Based On Time Automata

Track circuit equipment is one of the basic equipment of railway signal system,playing an important role in the safety of train running and the improvement of transportation efficiency.However,the frequent track circuit failure-loss of shunt reduces the reliability and safety of the whole signal system and thus has a negative impact on the safety and efficiency of transportation production.In the early stage,railway bureaus adopted various methods to alleviate the problems caused by the loss of shingles in the section of track circuit,but all of these solutions have limitations.The safety protection function cannot be achieved for the section of track that has lost the shingles,and there are still hidden dangers of train running in the section.In recent years,the rectification of train occupation and loss is carried out in the whole railway network.The relay type interval occupying logic check site construction is difficult,and not conducive to the scene maintenance.In this case,the electronic interval occupying logic check system is developed,realizing the logic judgment of train position,branch to track circuit when bad for safety protection.The electronic interval occupation logic inspection system is a software-intensive complex system with strong timing and complex logic functions.If the manual analysis is carried out entirely based on experts’ experience,the completeness of the scene and logic analysis and processing cannot be guaranteed.Hence,this paper adopts formal method to analyze and verify the transformation of block partition logic state which is one of the core parts of interval occupancy logic check.By comparing the advantages and disadvantages of common formal methods,time automata theory is selected as the research method of this paper,and UPPAAL is used as the modeling verification tool.In this paper,the electronic interval occupation logic check is taken as the research subject and the state transformation of block partition logic is taken as the research object.The paper describes the realization process of the interval occupation logic by applying the“three-point check” logic in the station to the interval.Various scenarios of logical state transformation of interval block partition and the judgment logic of occupied/idle state of interval block partition under various scenarios are systemically analyzed.By extracting actions of various subjects,the paper establishes interval block partition logic state transform the various scenarios of timed automata model with UPPAAL.In order to guarantee the integrity of the model information,the block partition logic state information transfer process model and microcomputer monitoring real time receiving the logic state information model are added at the same time,composing the corresponding timed automata product,Finally,the UPPAAL tool is used to verify the functional requirements and time constraints of the system.Through the analysis and verification of the above model,the test results are consistent with the application function of the system,indicating the effectiveness of the interval block partition logical state transformation model,and further verifying the security and feasibility of the interval block partition occupation logic state transformation.