Petri网的重写逻辑模型及其属性验证  

Research on the rewriting logic model and its properties verification of Petri net

作　　者：聂锡宁[1] 蔡国永[1] 

机构地区：[1]桂林电子科技大学计算机科学与工程学院,广西桂林541004

出　　处：《桂林电子科技大学学报》2011年第3期208-212,共5页Journal of Guilin University of Electronic Technology

基　　金：国家自然科学基金(61063039)

摘　　要：为了对大规模或复杂结构的系统进行规格,人们在经典的库所/迁移Petri网基础上加入层次、时间等来扩展它。为此,提出使用重写逻辑表达Petri网的新方法来探索对Petri网的替代。通过把异步并发系统的Petri网图形表达转化为重写逻辑理论,可以更容易和更直接地验证原系统的安全性、活性和可达性等行为属性,而不需要建立标识图或搜索网络不变量。以银行家问题为例,展示模型转化过程,并检测了该模型的无死锁性。结果表明,库所/变迁Petri网可以等效转化为重写规则代数组合的重写逻辑,并能在重写逻辑软件Maude中验证保留的基本属性。For the specification of the large scale or high complexity systems,the classical place/translation Petri net was extended with hierarchy and timing.Thus,a new approach of expressing Petri net was proposed to explore some replacement of Petri net.By transforming graphic Petri net expressions of asynchronous and concurrent systems into rewriting logic theory,the behavioral properties of the original systems such as safety,liveness and reachability were directly verified,without building the marking graph or searching for net invariants.Banker problem was used to illustrate the transformation,and its deadlock free was checked.The result shows that the place/transition Petri Net can be transformed into equivalent algebraic composition of rewrite rules of rewriting logic system,and the preserved essential properties are verified in Maude.

关 键 词：PETRI网 重写逻辑 验证 形式化方法 MAUDE 

分 类 号：TP311.5[自动化与计算机技术—计算机软件与理论]