《计算机学报》文章摘要   全文下载
文章题目	并发程序验证的时序Petri网方法
作者	丁志军1) 蒋昌俊1),2)
作者单位	１）（山东科技大学信息科学与工程学院 泰安　271019） ２）（同济大学计算机科学与工程系 上海 200092）
发表年份	2002
发表月份	5期　（页码：467—475)
文章摘要	并发程序的设计、分析和验证已经成为计算机理论界基础理论研究的方向之一.P etri网和时序逻辑被认为是探讨该问题较为有效的两个理论工具，但二者都有局限性.该文 引用一种新网子类：时序Petri网，描述了并发程序的时序Petri网建模方法：利用网结构描 述程序基本框架及保证语句的原子性，通过时序逻辑公式反映程序的共享逻辑变量的赋值变 化及时序关系，从而有效地对基本网无法描述的并发程序进行了建模；在此基础上，结合Petri网的可达图分析技术和时序逻辑的演绎公式，分析和验证了并发程序的安全性和活性性质. 关键词 时序Petri网，并发程序，验证，安全性，活性 中图法分类号：TP301