Research And Implementation Of Symbolic Model Checking Of Concurrent Systems Under Possibility Measurement

Model checking is a formal automatic verification technique.In 1981,it was proposed by Clarke,Emerson,Quielle and Sifakis.Its basic idea is to verify the correctness of the property of the finite state system by exhaustive search in the state space.Not only can it be performed automatically,but it can also provide counterexamples when the system does not satisfy its property.However,with the increase of system complexity in recent years,uncertain information in the system needs to be dealt with urgently,and the problem of state explosion is becoming more and more severe,the existing model detection technology has not been fully applicable to the verification of complex systems.Therefore,it is important and necessary to extend the model detection technology.At present,domestic and foreign scholars have done a lot of research on symbolic model check-ing in the field of classical model checking and probabilistic model checking,but there is no relevant symbolization research on model checking under possibility measure.This paper studies the symbol-ic model checking of the system under the possibility measure,which is an extension of the model checking technology and the symbolic model checking technology under the possibility measure.It has certain significance for the realization and popularization of the model checking of the complex system.This paper studies the symbolic model checking of the concurrent system under the possibility measure,and designs a symbolic model checker under the possibility measure.On the one hand,it deals with uncertain information in the verification of complex systems and on the other hand alleviates the problem of state explosion in the verification of complex systems.The research content of this article is mainly divided into the following points:(1)Propose a symbolic model of the concurrent system under the possibility measure.When there are many concurrent system states,the symbolization model can better represent the transition state between the system state and state and improve the verification efficiency.(2)Studied the symbolic model checking algorithm under the possibility measure.The system model and state are expressed symbolically using a multi-terminal binary tree,and the verification algorithm is implemented using fixed point technology.(3)Based on the NuSMV basis,a symbolic model checker for possibility measure is researched and designed,the realization scheme of the model checker under possibility measure is given,and the implementation method of the model checker are discussed.The research significance mainly:It complements the symbolic model checking theory of con-current systems under the possibility measure.The implementation of the model checker under the possibility measure is given,which lays a foundation for the promotion of concurrent system check under the possibility measure.