摘要
Petri网是一种应用非常广泛的建模工具,它能深刻、简洁地描述控制系统,特别是能较好地描述并发系统的结构,并能对系统的动态性质进行分析。在探讨了Petri网的模型检查的基础上,采用双DFS算法,对基于Petri网的模型检查的算法进行了改进,提出了针对Petri网的on-the-fly算法,同时给出了基于on-the-fly的Petri网模型检查的实现和测试,从而可以有效地对Petri网表示的系统模型进行模型检查。
Petri net is a very widely used modelling tool,which can describe the control system in a profound and brief way.In particular,it can better describe the structure of concurrent system,and can analyse the dynamic property of a system.In this paper,based on the discussion of model checking of the Petri net,we adopt double DFS algorithm to improve the Petri net-based model checking algorithm,put forward the on-the-fly algorithm in light to the Petri net.Meanwhile,we also present the realisation and test of model checking of Petri net based on on-the-fly algorithm,so that the model checking on the system model expressed by Petri net can be applied effectively.
出处
《计算机应用与软件》
CSCD
2011年第5期82-85,共4页
Computer Applications and Software
基金
国家高技术研究发展计划项目(2007AA01Z144)
