The Reliable Design Of Safety And Critical Software Of Computer Interlocking

With the continuous development of 3C technology(computer technology, control technology, communication technology), in popularization of the computer interlocking technology, railway industry are increasingly using computer interlocking to replace electric centralized control. Railway transportation involves the personal safety and property loss, so it is very high to the requirement of safety and reliability, which is important for the safety and reliability of the computer interlocking, if the computer interlocking software is failure, it will cause big losses of life and property. How to improve the safety and reliability of the computer interlocking software are problems which a computer interlocking designers constantly think and research.In order to improve the safety and reliability of the computer interlocking software, the developers must demonstriate and analysize in the early stage of software development. First of all, software need be built a model and model will be demonstriated. The developers Commonly used way of modeling with structural modeling, formal modeling, object-oriented modeling, UML modeling, but the various method has its advantages and disadvantages, this thesis mainly adopts the formal modeling method. Formal method is to use mathematical language to replace natural language, because natural language is often a ambiguity, developers can’t understand the problem well, which will bring serious error to the late development of software. But the formal methods is to use mathematical language to describe the model,it has the advantages which is rigorous structure and unambiguous and facilitate design, and at the same time also can improve the reliability of software.Petri net is a kind graphical modeling language, it has the advantages which is easy for developers to understand. Through the analysis of the software requirements and rules, its mathematical model is set up using petri net and developers can prove and analysize with petri net unique validation method, which provide a great help for the developer to find the defects of the software. This paper adopts the CPN(colored petri net) to task for modeling and analysis. Analog system and discrete system modeling can be built a model with CPN, and if token are different properties, they will have different colors. In coloured petri net, a different colors token represent a kind of behavior characteristics. Its color sets can be discrete values or continuous values. The model are simulated by special simulation tool CPN TOOLS. In order to analysis the model whether there is a deadlock.In this paper, first introduces the structure and function of computer interlocking system and design requirements of the reliability of the computer interlocking software and put forward superiority of the modeling in formal way. Then this paper also introduces the definition of petri net of formal modeling language and the modeling method. CPN models of switch, track section and signal have be built and the model of the road of the computer interlocking software has be set up by rules of the computer interlocking software. Finally, the properties of the model have also be demonstriated and analysized by CPN TOOLS simulation, the state space analysis method, reachability tree method and relating matrix method. The results show that CPN models meet the requirements of the model design and the reliability of the model is also proved. Therefore, CPN model is a very effective method in the guarantee of reliability of computer interlocking software.