| Petri网的重写逻辑模型及其属性验证 |
| |
| 引用本文： | 聂锡宁,蔡国永.Petri网的重写逻辑模型及其属性验证[J].桂林电子科技大学学报,2011,31(3):208-212. |
| |
| 作者姓名： | 聂锡宁 蔡国永 |
| |
| 作者单位： | 桂林电子科技大学,计算机科学与工程学院,广西,桂林,541004 |
| |
| 摘 要： | 为了对大规模或复杂结构的系统进行规格,人们在经典的库所/迁移Petri网基础上加入层次、时间等来扩展它.为此,提出使用重写逻辑表达Petri网的新方法来探索对Petri网的替代.通过把异步并发系统的Petri网图形表达转化为重写逻辑理论,可以更容易和更直接地验证原系统的安全性、活性和可达性等行为属性,而不需要建立标识图...
|
| 关 键 词： | Petri网 重写逻辑 验证 形式化方法 Maude |
Research on the rewriting logic model and its properties verification of Petri net |
| |
| Nie Xining,Cai Guoyong.Research on the rewriting logic model and its properties verification of Petri net[J].Journal of Guilin Institute of Electronic Technology,2011,31(3):208-212. |
| |
| Authors: | Nie Xining Cai Guoyong |
| |
| Affiliation: | Nie Xining,Cai Guoyong(School of Computer Science and Engineering,Guilin University of Electronic Technology,Guilin 541004,China) |
| |
| Abstract: | 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 ... |
| |
| Keywords: | Maude |
| 本文献已被 CNKI 万方数据 等数据库收录！ |
|
