Research On Parallelization Of Model Checking Of Complex System Based On Fuzzy Petri Net

Model checking was proposed by Clarke and Emerson in the early 1980s,which is an effective automated verification technology for analyzing the correctness of hardware and software.Because the model checking can be automatically imple-mented and can output counterexample path when the system is not satisfied,it has been widely used and achieved remarkable results.However,with the complication of the real system,the model checking technology must be updated to solve two problems.One is to deal with the uncertain information contained in the system,and the other is to deal with the state explosion problem in system verification.Fuzzy Petri nets can be used to describe complex concurrent systems intuitively and succinctly.Therefore,it is of practical significance to study the checking of complex system models based on fuzzy Petri nets.This thesis will study in the following two aspects to solve the problem of uncertain information processing and state explosion in the checking of complex system models.1.The LTL model checking algorithm based on fuzzy petri net is presented.Firstly,the fuzzy Petri net is transformed into a special reachable graph.The state identifier in the reachable graph is a vector,and each element of the vector is in the interval[0,1];the transition relationship between states is also a[0,1]interval parameter;Then it can be transformed into a generalized possible Kripke Structure(GPKS).Based on this,it can be verified by using the generalized possibility model checking algorithm,which effectively solves the problem of uncertain information processing in complex system model checking.2.A distributed model checking algorithm is presented.Firstly,according to the state relationship,the GPKS is divided,and the state of close relationship is di-vided as much as possible on a computing node,which provides a good base for the execution efficiency of the distributed verification algorithm.Qualitative property is expressed using Buchi automaton,and the quantitative property is expressed using fuzzy automaton.On the different computing nodes,an extended LTL distribut-ed verification algorithm is used to complete the system's qualitative verification and quantitative verification,thereby effectively alleviating the state explosion in complex systems.The contribution of this thesis lies in:proposes the LTL distributed verification method under the generalized possibility measure,which can alleviate the state explosion problem faced by the model checking under the generalized possibility measure;it provides a feasible solution for the model checking of complex systems in the real environment.