| With the increasing complexity of computer hardware and software systems, how to ensure their accuracy and reliability become increasingly urgent. Ensuring the reliability of these systems become important in the field of computer science. Among a number of methods and theories, Model checking has received much attention because of concise and a high degree of automation . Model Checking is one of the most successful techniques of automatic verification, and its successful application is due to the support of efficient verification tools. SPIN is a well-known model checking tool which use to analysis the complicated systems to verify their logical consistency .The bottleneck problem of model checking is the state of the explosion, so how to describe the system in the streamline way and how to avoid state of the explosion which was caused by complexity of the model is a worthy research direction.In this article it is description of SPIN model checker's mechanism of formal analysis and linear temporal logic LTL property, a detailed analysis of concurrent process, channel operation, the basic data structure and the function in the SPIN-based modeling language Promela, and a designment of method for solvingdiscrete problems——that is the establishment of Promela model and describing theSystem Properties (nature) using the technology of Branch-and-Bound , LTL formula dynamic changes during the verification process, aimed at reducing the state-space of the model to improve the efficiency of search, This method is verified correctly by analysising examples; At the same time it is adopted a method of heuristic to optimize model, that is, according to SPIN model checking the principle of depth-first search, using the methods of static analysis and dynamic analysis to optimize the model, and the experimental results show that SPIN will not only verify the system model of solving problems correct but also that can search for the optimal solution to problems. |
PDF Full Text Request