Temporal verification diagrams

Abstract

Most formal approaches to the verification of temporal properties of reactive programs infer temporal conclusions from verification conditions that are state formulas, i.e., contain no temporal operators. These proofs can often be effectively presented by the use of verification diagrams. In this paper, we present a self-contained presentation of verification diagrams for proving various temporal properties.

Beginning with safety properties, we present WAIT-POR and INVARIANCE diagrams for proving wait-for (precedence) and invariance formulas. Proceeding to liveness properties, we present verification diagrams for response properties that require a bounded number of helpful steps (CHAIN diagrams) and response properties that require an unbounded number of helpful steps (RANK diagrams).

Additional types of diagrams are proposed for handling response properties for parameterized programs (e.g., P-RANK diagrams) and response properties that rely on the full spectrum of fairness requirements, including compassionate helpful transitions (e.g., F-CHAIN diagrams).

This research was supported in part by the National Science Foundation under grant CCR-92-23226, by the Defense Advanced Research Projects Agency under contract NAG2-703, by the United States Air Force Office of Scientific Research under contract F49620-93-1-0139, by the European Community ESPRIT Basic Research Action Project 6021 (REACT), and by the France-Israel project for cooperation in Computer Science.