Font Size: a A A

# On-the-fly Model Checking Based On Petri Nets

Posted on:2009-11-20Degree:MasterType:Thesis
Country:ChinaCandidate:Y Y WangFull Text:PDF
GTID:2178360245981519Subject:Computer software and theory
Abstract/Summary:PDF Full Text Request
As an important mathematics tool,the Petri nets are effectively applied in the description and making model of the concurrent systems.Meanwhile,linear temporal logic(LTL for short)is one of the most significant formal tools,which could exactly describe and check the properties of the concurrent systems,and describe the important properties of the concurrent system accurately,such as safety and liveness.The theory of automaton play an important role in model checking,whose cornerstone is temporal logic and the theory of automaton.In fact,model checking is a formal verification technique to detect whether a computing model,by searching the state spaces,satisfies a given property described by an appropriate temporal logic. However,the main disadvantage of model checking is the state explosion problem.This article described the Petri nets,linear temporal logic,Büchi automaton and the intersection of the reachable graph of the Petri net and the automaton,an efficient model checking policy of the reachable graph of the Petri net are detailed discussed based on the linear temporal logic and the theory of automaton,and compared to the other polices,this policy is based on the on-the-fly technique.In on-the-fly model checking,we only need to construct the automaton correspondence to the verified property and the Petri net model of the system,through the search of the state spaces,if new state is needed,then the intersection of the reachable graph of the Petri net and the property automaton is constructed dynamically,at the same time,we use the property automaton to guide the procedure of the constructing of the reachable graph of the Petri net dynamically.Thus,after finding a counter-example of the verified property,it is possible that we only need to construct a small part of state spaces of the reachable graph of the Petri net and the intersection of the automaton, thus we can avoid searching the entire state spaces of the intersection of the automaton, and this policy can reduce the search spaces,and can slow down the state explosion problem.And the memory we needed to save the reachable graph of the Petri net as well as the synchronous product will be reduced,thus it is solved the insufficient of the memory.
Keywords/Search Tags:Petri net, linear temporal logic, Büchi automaton, model checking, on-the-fly
PDF Full Text Request
Related items
 1 Model Checking Propositional Projection Temporal Logic With Infinite Model 2 Research On Heuristic Model Checking Method For CPN Model Of Parallel Software Based On LTL 3 An Automaton Method For Generalized Possible Linear Sequential Logic 4 Based On Temporal Logic Uml Interaction Model Checking 5 Model Checking Of Petri Nets Based On Projection Temporal Logic 6 Petri Net-based Workflow Technology Research And Applications 7 Research On Consistency Checking Between Model Refinements 8 Simulation Based Model Checking 9 Bi-directional Consistency Checking Based On Temporal Logic 10 The Design And Implementation Of Linear Temporal Logic Satisfiability Tool