为了对大规模或复杂结构的系统进行规格,人们在经典的库所/迁移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.
展开▼
