The Research And Application Of NuSMV Model Verifier

Increasing complexity of computer hardware and software systems, the accuray and reliability of the hardware and software systems has become a hot research field among a number of methods and theory, model checking with its clear, concise and high degree of automation got much attention. The key problem of model checking is the state explosion problem, specifically, how to use the streamlined way to describe the system, avoid the state explosion caused by the model complexity.The successful application of model checking must be based on efficient verification tools. NuSMV as an effective analysis of the logical consistency of concurrent systems verification model checking tool has been more widely used. This paper describes the mechanism of the formal analysis and temporal logic supported by the NuSMV, especially analysis the protocol of PCI bus by the model verifier NuSMV. detailed analysis of the requirements of the specification of PCI bus protocol, we modeled bus signals and bus command action of the PCI bus protocol, including the bus signals and commands, master and slave devices read/write transactions and equipment scheduling modeling. We substantiate the PCI bus protocol model and tested its properties on the requirements of the specification. the results show that:If the NuSMV test result is FALSE, then that property is not satisfied, and NuSMV counterexamples can be given to detailed description of the violation of property so that the checker can easily detected the error. the test results with the actual PCI bus protocol is the same logic,and our model of PCI bus protocol is reliable.Article describing the detection method has a certain universality, which can be used for higher accuracy and reliability requirements of the system.