Formal Modeling And Verification Of Interlocking Software Based On UML-Promela

As the core part of railway control system,the computer interlocking system plays an irreplaceable role in ensuring the safety of railway traffic.As a typical safety-critical system,computer interlocking system must ensure its safety and reliability.The formal method is an effective means to improve the accuracy and safety of the system,so it is very important for the safety of railway traffic to use the formal method to model and verify the interlocking system.However,modeling the interlocking system directly using formal methods not only requires developers to have strong professional knowledge,but also becomes more difficult as the scale of the station increases.Therefore,it is necessary to find a simpler and more efficient way to model and verify the interlocking system.UML(Unified Modeling Language)is widely used in the field of software development.The model built with UML is composed of multiple views,and each view describes the system from a different perspective.However,UML is only a semi-formal language,which can not be directly verified by formal methods.SPIN is a formal verification tool that uses Promela as the input language,and it can efficiently verify the Promela model.If a UML model of interlocking system can be automatically converted into a formal Promela model,the difficulty of formal modeling can be reduced and the efficiency of modeling and verification can be improved.In summary,the author proposes a formal modeling method based on UML and Promela,which is used to model and verify the interlocking system during the requirements analysis phase.The main work of the paper is as follows:(1)First,in order to obtain the functional requirements of the interlocking system,the paper analyzes the overall framework of the interlocking system in conjunction with "Technical Conditions for Computer Interlocking of Railway Stations" and establishes a UML use case diagram.Then the paper analyzes the outdoor equipment and its interface circuit,and establishes the class diagram and state diagram of each equipment.Finally,the paper analyzes the main control process of the interlocking system in detail,and establishes a sequence chart for each control process.(2)The UML model and Promela model are compared and analyzed,and the conversion rules of UML three views to Promela model are formulated.Then,according to these rules,the paper develops a model transformation tool based on MFC framework in visual studio environment,and realizes the automatic transformation from UML model to Promela model.(3)The technical specifications that the interlocking demand model should meet are extracted,and the LTL(Linear-time Temporal)formula is used to express these technical specifications.Finally,the LTL formula and the formal model are input into the SPIN together to verify the correctness of the model.(4)Based on the established interlocking demand model,a computer interlocking simulation platform is built for the example station,and the correctness of the model is further verified by simulation.The result shows that the method can reduce the modeling difficulty of the interlocking system and ensures the accuracy of the model.The modeling method provides a new idea for the formal verification of the computer interlocking system.Figure 88,table 2,reference 58.