一种基于P/T网的低级并发程序验证模型

• 作者: 梁英毅 王生原 董渊
• 来源期刊: 中国科学(信息科学)
• 学科: 工学
• 关键词: 低级并发程序 Petri网 抽象机器 程序验证 分离逻辑
• 年，卷（期）: 2010,（1）
• 页码范围: 13-32
• 页数: 20页
• 分类号: TN407
• 语种: 中文

摘要

随着片上多处理器/多核技术的不断发展,采用机器级语言的并发程序(低级并发程序)有了更加广阔的应用前景.然而,低级并发程序的验证问题也成为程序语言领域一种新的挑战.并发程序安全性验证领域现有的工作多数是针对高级语言、规范或者演算,而针对机器级语言的甚少.这种情况的主要原因之一是缺少低级抽象模型.文中描述一种可验证的低级并发编程模型P-PMCC.P-PMCC程序是一个扩展的P/T网系统,其网结构用来刻画低级并发线程(原子的顺序汇编级代码)之间的并发关系.P-PMCC程序的验证采取模型检查和定理证明相结合的方法,分开考虑并发行为与顺序线程的规范和验证:前者借助于Petri网领域已有的方法,后者则借助现有的顺序程序的正确性证明方法.P-PMCC程序也可以看作并发程序的一种可验证的低级中间表示.

作者信息

序号	姓名	单位	发文数	被引次数	H指数	G指数
1	董渊	清华大学计算机科学与技术系	33	386	10.0	18.0
2	王生原	清华大学计算机科学与技术系	33	235	8.0	14.0
3	梁英毅	清华大学计算机科学与技术系	1	0	0.0	0.0