Formal Modeling And Verification Of Section Occupancy Logic Check Based On Model Checking

As the basic equipment of railway signal system,track circuit is mainly used to reflect the occupancy of block section,and its reliability and safety play an important role in the safety of railway transportation.In case of bad shunting or fault occupation of track circuit,the status of track relay will change wrongly.At this time,it is unable to accurately judge the condition of the occupied section of the train,resulting in "red light strip","lost train" and other phenomena,causing potential safety hazards.The section occupancy logic check is the solution to the above track circuit fault at this stage.It uses the "three-point check" principle of station interlocking for reference,adds timing constraints,and carries out corresponding logic calculation according to the running direction of the train in the section and the sequence of occupying and clearing the block area.It preprocesses the status change information of the untrusted track relays to effectively reduce the risk of driving.Therefore,it is of great significance to analyze and study the logical check of section occupancyDue to the complexity of the principle of section occupancy logic check and the real-time requirements of the inspection process,the traditional simulation test methods can not detect the human analysis errors in the process of logic formulation in time,Therefore,this paper uses the formal method to analyze and verify the section occupancy logic check in order to improve its logical correctness and ensure the safety.By analyzing the functional characteristics of section occupancy logic check,comparing the advantages and disadvantages of the formal modeling and verification methods commonly used in the current railway field,the time automata theory is used as the research method,and UPPAAL is used as the verification tool.This paper takes the software type section occupancy logic check as the research object,and takes the logic check principle as the research target,and elaborates the implementation process of section occupancy logic check.In order to reduce the complexity,according to the functional characteristics and scope of function of the section occupancy logic check,it is divided into two sub processes: the own station occupation logic check and the two station logic check information interactions.Analyze the implementation process and functional scenarios of the two sub-processes separately,determine the objects included in each sub-process,extract the behaviors of each object,describe it in formal language,and construct a time automaton model for each object,At the same time,in order to increase the integrity of the model and simulate the real driving state of the section as much as possible,the block partition fault model is injected into the own station occupation logic check,and the communication fault model is injected into the two station logic check information interactions to form the corresponding time automata product.Then,the verification tool UPPAAL is used to verify its functionality and real-time performance,and the result is derived Security application scenarios.Based on the above model analysis and verification,the design and development of simulation system is realized by programming,and its function is tested.The test results are consistent with the expected results,which shows the correctness of the section occupancy logic check model,and further verifies the security and feasibility of the section occupancy logic check.