The Study Of Formal Verification Method About Rail Signal Interlocking Logic Relation

As an important part of railway signal system, interlocking system plays an directly role in the safety and efficiency of station operation, As a key component of interlocking system, Interlocking software must have high security and high reliability since it can not only help interlocking system to realize interlocking functions but also ensure interlocking operation correctly.With the rapid development of high-speed railway,the problem of traditional software developing process increasingly exposed because of the application scene of computer interlocking system is becoming more and more complex.For instance,it’s difficult to ensure precise and unambiguous on demands definition, it’s easy to form safety hazard since simulation test is hardly to analysis and verify software security completely and so on.In this paper we proposed an CPN formal method to solute the problems in traditional interlocking software developing process on the basis of further studying of6502 electric centralized interlocking logic control circuits and researched on formal modeling and verification of interlocking system core function- route control.The main work of the paper is as follows:Analyzing the disadvantages of current traditional software developing method and the advantage of using formal method,Researching on the theoretical basis of CPN,Introducing CPN Tools which can used to modeling simulation analysis models based CPN, Proving the possibility of using HCPN to realize interlocking logic verification.Further studying in 6502 electric centralized interlocking logic control circuit and combining station map to analyze route-control process such as route arranging,route locking, signal clearing, route releasing in normal condition, route releasing in abnormal condition and find out the key function requirement of route-control process.Establishing top model for interlocking route-control by using top-down development of HCPN, this model is composed by substitution transitions which can replace sub-pages like route arranging, route locking, signal clearing, route releasing in normal condition, route releasing in abnormal condition, The simulation results of the model show that token moving can describe interlocking route-control process in a good way,in addition, this paper also proposed an formal verification method for more than one route-control condition.The state space analysis tools was used to analyze the model’s state space, the results show that the model has good security, correctness, completeness.The results of the research work in this paper indicates that the CPN based formal modeling and verification method can not only describe the function requirements of interlocking route-control accurately and effectively in dynamic form but also analyzeand verify the safety of the model completely,It can be used in the pro-phase of software development to reduce the security risks of interlocking software.