并发程序验证的时序Petri网方法

• 作者: 丁志军 蒋昌俊
• 来源期刊: 计算机学报
• 学科: 工学
• 关键词: 时序Petri网 并发程序 验证 安全性 活性
• 年，卷（期）: 2002,（5）
• 所属期刊栏目: 研究论文与技术报告
• 页码范围: 467-475
• 页数: 9页
• 分类号: TP301
• 字数: 7066字
• 语种: 中文
• DOI: 10.3321/j.issn:0254-4164.2002.05.003

摘要

并发程序的设计、分析和验证已经成为计算机理论界基础理论研究的方向之一.Petri网和时序逻辑被认为是探讨该问题较为有效的两个理论工具,但二者都有局限性.该文引用一种新网子类:时序Petri网,描述了并发程序的时序Petri网建模方法:利用网结构描述程序基本框架及保证语句的原子性,通过时序逻辑公式反映程序的共享逻辑变量的赋值变化及时序关系,从而有效地对基本网无法描述的并发程序进行了建模;在此基础上,结合Petri网的可达图分析技术和时序逻辑的演绎公式,分析和验证了并发程序的安全性和活性性质.

作者信息

序号	姓名	单位	发文数	被引次数	H指数	G指数
1	蒋昌俊	山东科技大学信息科学与工程学院	93	1492	18.0	36.0
5	丁志军	山东科技大学信息科学与工程学院	16	105	5.0	9.0