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