Verification of parallel systems using constraint programming

摘要: Liveness properties of parallel systems usually specify that in every execution certain states are eventually reached. Therefore, violation such a property can only be detected infinite executions. In this paper we introduce semi-decision method is baseprogramming*d on structural Petri net analysis and makes use the constraint programming paradigm. By understand procedure which may answer 'yes', so case system satisfies property, or 'don't know'. We give an implementation our terms tool 21p. An application approach to snapshot algorithm demonstrates how program ming beat classical exact methods as model checking.