| 并发程序验证的时序Petri网方法 |
| |
| 引用本文： | 丁志军,蒋昌俊.并发程序验证的时序Petri网方法[J].计算机学报,2002,25(5):467-475. |
| |
| 作者姓名： | 丁志军 蒋昌俊 |
| |
| 作者单位： | 1. 山东科技大学信息科学与工程学院,泰安,271019
2. 山东科技大学信息科学与工程学院,泰安,271019;同济大学计算机科学与工程系,上海,200092 |
| |
| 基金项目： | 本课题得到国家自然科学基金(69973029,69933020)、国家"九七三"重点基础研究发展规划项目(G1998030604)、国家杰出青年科学基金(60125205)、全国优秀博士论文作者专项基金(199934)、上海市重点基础研究计划、教育部优秀青年教师教学科研奖励计划资助. |
| |
| 摘 要： | 并发程序的设计、分析和验证已经成为计算机理论界基础理论研究的方向之一。Petri网和时序逻辑被认 为是探讨该问题较为有效的两个理论工具,但二者都有局限性。该文引用一种新网子类;时序Petri网,描述了并发程序的时序Petri网建模方法;利用网结构描述程序基本框架及保证语句的原子性,通过时序逻辑公式反映程序的共享逻辑变量的赋值变化及时序关系,从而有效地对基本网无法描述的并发程序进行了建模;在此基础上,结合Petri网的可达图分析技术和时序逻辑的演绎公式,分析和验证了并发程序的安全性和活性性质。
|
| 关 键 词： | 并发程序 验证 时序Petri网 计算机 |
| 修稿时间： | 2000年8月24日 |
Verification of Concurrent Programs by Temporal Petri Nets |
| |
| Abstract: | |
| |
| Keywords: | |
| 本文献已被 维普 万方数据 等数据库收录！ |
|
