Verification of Concurrent Programs by Temporal Petri Nets
Ding Zhi · Chinese Journal of Computers · 2002
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.