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

摘要

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