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

Verification of Concurrent Programs by Temporal Petri Nets

作　　者：丁志军[1] 蒋昌俊[1] 

机构地区：[1]山东科技大学信息科学与工程学院,泰安271019

出　　处：《计算机学报》2002年第5期467-475,共9页Chinese Journal of Computers

基　　金：国家自然科学基金 (69973 0 2 9;6993 3 0 2 0 );国家"九七三"重点基础研究发展规划项目 (G19980 3 0 60 4);国家杰出青年科学基金 (60 12 5 2 0 5 );全国优博士论文作者专项基金 (19993 4);上海市重点基础研究计划资助;教育部优秀青年教师教学科研奖励计划

摘　　要：并发程序的设计、分析和验证已经成为计算机理论界基础理论研究的方向之一 .Petri网和时序逻辑被认为是探讨该问题较为有效的两个理论工具 ,但二者都有局限性 .该文引用一种新网子类 :时序 Petri网 ,描述了并发程序的时序 Petri网建模方法 :利用网结构描述程序基本框架及保证语句的原子性 ,通过时序逻辑公式反映程序的共享逻辑变量的赋值变化及时序关系 ,从而有效地对基本网无法描述的并发程序进行了建模 ;在此基础上 ,结合Petri网的可达图分析技术和时序逻辑的演绎公式 。This paper introduces a new class of Petri nets, called temporal Petri nets, in which temporal constraints of a given net are represented by the temporal logic formulas. The Temporal Petri nets is used as a tool for modeling, analyzing and verifying concurrent programs. Firstly, the method of modeling concurrent programs is introduced. On the one hand, the basic frameworks of programs are described by net structures and the atomic actions of statements is execution are represented by the transition firing. On the other hand, temporal logic could describe effectively the changes and temporal relationships of share logic variants is evaluation, which are difficult to be represented by Petri nets. In addition, the fair requirements of statements is execution are stated by temporal logic formulas. Then, authors analyze and verify the safety and liveness properties of concurrent programs using temporal Petri net models. That is, combining the method of reachability of Petri nets and deduction of temporal logic formulas, we could use temporal logic formulas for describing and deducting dynamic behaviors and the states of markings. Not only safety properties of programs are analyzed and verified, but also liveness properties, which are difficult to be described by Petri net models, are verified formally through above method. Generally, proposition of safety properties could be stated formally by temporal logic, and proposition of liveness properties could be described by temporal logic. In short, the explanation in this paper indicates that temporal Petri nets provide a new and useful way for modeling concurrent programs and verifying correctness of programs.

关 键 词：并发程序 验证 时序PETRI网 计算机 

分 类 号：TP31[自动化与计算机技术—计算机软件与理论]