基于Petri网的模型检测研究  

Research on Model-Checking Based on Petri Nets

作　　者：蒋屹新[1] 林闯[1] 曲扬[1] 尹浩[1] 

机构地区：[1]清华大学计算机科学与技术系,北京100084

出　　处：《软件学报》2004年第9期1265-1276,共12页Journal of Software

基　　金：国家自然科学基金;国家高技术研究发展计划(863);国家重点基础研究发展规划(973)~~

摘　　要：模型检测是关于系统属性验证的算法和方法.它通常采用状态空间搜索的方法来检测一个给定的计算模型是否满足某个用时序逻辑公式表示的特定属性.系统模型的状态空间的爆炸问题是模型检测所面临的主要问题,其主要原因是系统自身的并发特性和状态变迁的语义交织.对基于 Petri 网的模型检测理论和验证技术进行了较为详细的研究,着重探讨了基于 Petri 网状态可达图的偏序简化和偏序语义技术、基于自动机的模型etri 网的状态聚合法以及基于系统对称性的参数化和符号模型检测技术,并给出了研究思路以及未来所要进行的重点研究工作.模型检测技术已在通信协议和硬件系统的验证等领域得到成功应用,并且随着各种状态空间简化技术和模型检测算法的不断优化,其在其他应用领域也展示出广泛的应用前景.Model-Checking is a formal verified technique to check on whether a computing model, by searching the model state spaces, satisfies a given property described by an appropriate temporal logic. The main drawback of model checking, the explosion problem of state spaces, is mainly caused by concurrence and the interleaving semantics used to represent any sequences of possible actions. The correlative model-checking theory and techniques based on Petri Nets are investigated in detailed, especially about the following problems, i.e. partial order reduction and partial order semantics techniques based on the state reachability graph, Buchi automata method, state cohesion method based on Petri Nets, and symbolic and parametrized model-checking techniques based on system symmetries. Moreover, the key idea and our main researching work in the future are listed. With the gradual improvement of reducing techniques of state space and optimization of model-checking algorithm, model-checking technique is successfully applied to verify communication protocols and complex hardware logic circuits, and also takes on a wide application prospect in other fields.

关 键 词：时序逻辑 PETRI网 状态空间 模型检测 

分 类 号：TP301[自动化与计算机技术—计算机系统结构]