| The computer interlocking system is one of the core systems of railway control,and it is an important link to ensure the safety of railway transportation.As a typical safety-critical system,the design and development of computer interlocking software should be carried out in strict accordance with the relevant regulations and high industry standards.With the rapid development of railway system,using formal verification to find out the existing problems in the requirement analysis phase of interlocking software development is of great significance for ensuring the safe and efficient running of railway transportation system.However,the direct use of formal methods have some disadvantages,such as high requirements for professional knowledge,difficulty in using,and low efficiency of modeling.Therefore,with the continuous improvement of the scale and complexity of the station,it is necessary to develop a more efficient and convenient formal verification method for interlocking software to ensure its correctness.Unified Modeling Language(UML)is now widely used in various stages of software development,it combines multiple views to accurately describe the system from different perspectives,but as a semi-formal language,it does not provide automatic analysis and effective verification method.The New Symbolic Model Verifier(NuSMV)is an efficient and mature formal verification tool,if the interlocking system model could be established by using UML and be transformed into a formal NuSMV model to verify,the purpose of reducing the difficulty and increase the efficiency of the interlocking system formal modeling and verification can be achieved by the indirect way.In view of the above problems,a formal verification method for computer interlock system which UML combined with NuSMV is proposed in this thesis.Firstly,the frame structure of the interlocking system and the requirements of every stage of route control are analyzed,and a route search algorithm based on coordinate and station topology is proposed for route selection stage.A standard station is taken as an example,the class diagram,state diagram and sequence diagram in UML are used to set up the requirements model of interlocking control logic.Secondly,the correlation between UML model and NuSMV formal model in terms of structure and semanteme is analyzed,and a set of transformation rules from UML model to NuSMV model is developed based on the characteristics of device interaction.Then according to these rules,the corresponding model conversion program is written by C#,and the batch conversion of the UML model to the NuSMV model is completed automatically.Finally,the relevant technical specifications of computer interlocking system are analyzed and extracted,some properties of the interlocking system should be followed are described by using Computation Tree Logic(CTL)expression and input into NuSMV verifier as verifyingstatements to complete the verification of the computer interlocking system.The verification results show that the proposed method can effectively and accurately verify the correctness of interlocking system requirements,and counterexamples could be given to correct possible errors,a new idea for the requirements model correctness verification of computer interlocking system is provided. |
PDF Full Text Request