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

• 作者: 聂锡宁 蔡国永
• 来源期刊: 桂林电子科技大学学报
• 学科: 工学
• 关键词: Petri网 重写逻辑 验证 形式化方法 Maude
• 年，卷（期）: 2011,（3）
• 页码范围: 208-212
• 分类号: TP311.5
• 字数: 4685字
• 语种: 中文
• DOI: 10.3969/j.issn.1673-808X.2011.03.009

摘要

为了对大规模或复杂结构的系统进行规格,人们在经典的库所/迁移Petri网基础上加入层次、时间等来扩展它.为此,提出使用重写逻辑表达Petri网的新方法来探索对Petri网的替代.通过把异步并发系统的Petri网图形表达转化为重写逻辑理论,可以更容易和更直接地验证原系统的安全性、活性和可达性等行为属性,而不需要建立标识图或搜索网络不变量.以银行家问题为例,展示模型转化过程,并检测了该模型的无死锁性.结果表明,库所/变迁Petri网可以等效转化为重写规则代数组合的重写逻辑,并能在重写逻辑软件Maude中验证保留的基本属性.

作者信息

序号	姓名	单位	发文数	被引次数	H指数	G指数
1	蔡国永	桂林电子科技大学计算机科学与工程学院	98	400	12.0	15.0
2	聂锡宁	桂林电子科技大学计算机科学与工程学院	1	1	1.0	1.0