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

【Abstract】 With the production and development of high speed parallel computers, and the requirement of many real time application systems, the design, analysis and verification of concurrent programs has become one of the important research fields. Petri nets and temporal logic are efficient tools for studying this problem, but each of them has some shortages. Therefore, they could not satisfy completely requirements of the concurrent programs’ research. To make up these shortages, in this paper, we introduce 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. We use temporal Petri nets 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’ 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’ evaluation, which are difficult to be represented by Petri nets. In addition, the fair requirements of statements’ execution are stated by temporal logic formulas. Then, we 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: < M,α >□, and proposition of liveness properties could be described by temporal logic: < M,α>□(condition◇result ). 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.更多还原