Research On Modeling Of Computer Interlocking Software At Railway Stations

Computer interlocking system at railway stations is to use fault-security technology,computer technology,network technology and fault-tolerant technology to achieve the function of route control.It is not only a real-time system,but also a security-critical system.Computer interlocking software at railway stations is a kind of security-critical software,which plays a key role in ensuring the safety and efficiency of train in the ascension,and is important to computer interlocking system at railway stations.At the present time,natural language is applied to the interlocking software design,which may show a lot of ambiguities.It can greatly clear software structures and functions to establish models of the interlocking system access control process and its sub-processes,based on the Object-Oriented Technology,and integrated with Class Diagram,Use Case Diagram,Collaboration Diagram,Sequence Diagram,State Diagram and Activity Diagram.And based on the formal methods with strict mathematics and strict logic theory,the formal system ALCQI-CTL is applied to formalize and explain the model,which can efficiently eliminate the defects and errors of the software design stage.This paper studies the modeling of interlocking software at railway stations.(1)Kripke Model and its semantics are given.The Description Logic ALCQI with qualified number restriction and inverse role is presented.The semantics of ALCQI are given.Also,the formalization method of sequence diagram based on formal system ALCQI-CTL is proposed.The formal semantics of the model of the system are studied.And the feasibility of the system is analyzed.(2)The static models of the system are established.The composition and function of the hardware and software of the computer interlocking system are analysed.In view of the users,the composition and function of the computer interlocking software are described.The data descriptions of the signal,switch,section and route are designed by Class Diagram,and the changes of them are designed by State Diagram.(3)The dynamic models of the system are established.Based on a series of dynamic diagrams of UML,the dynamic models of the overall model and process of the route control process are built.The Kripke models of the control process and subproceses are established.Based on formal system ALCQI-CTL,the formal description and explanation are showed.(4)The models are simulated and validated.The experimental results show that the models of railway interlocking system are stable,reliable and complete.The research results show that comprehensive uses of Unified Modeling Language and Formal Methods,on the one hand,can effectively eliminate the software design defects and errors caused by human differences,make the experts in the field of interlocking and developers in the field of software development interrract closer,and improve safety and reliability of computer interlocking software.On the other hand,it is possible to discover defects and errors in software design at the initial stage of software development,to a large degree,reducing the economic cost of software testing and verification.The verification results show that the models of computer interlocking software can be applied to practical needs.