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.
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
B. Alpern and F.B. Schneider. Verifying temporal properties without temporal logic. ACM Trans. Prog. Lang. Sys., 11:147–167, 1989.
D. Harel. Statecharts: A visual formalism for complex systems. Sci. Comp. Prog., 8:231–274, 1987.
B.T. Hailpern and S.S. Owicki. Modular verification of computer commuincation protocols. IEEE Trans. on Commun., COM-31(1):56–68, 1983.
L. Lamport. The temporal logic of actions. Technical report, Digital Equipment Corporation, Systems Research Center, 1991.
Z. Manna and A. Pnueli. Verification of concurrent programs: A temporal proof system. In J.W. de Bakker and J. Van Leeuwen, editors, Foundations of Computer Science IV, Distributed Systems: Part 2, pages 163–255. Mathematical Centre Tracts 159, Center for Mathematics and Computer Science (CWI), Amsterdam, 1983.
Z. Manna and A. Pnueli. Adequate proof principles for invariance and liveness properties of concurrent programs. Sci. Comp. Prog., 32:257–289, 1984.
Z. Manna and A. Pnueli. Completing the temporal picture. Theor. Comp. Sci., 83(1):97–130, 1991.
Z. Manna and A. Pnueli. The Temporal Logic of Reactive and Concurrent Systems: Specification. Springer-Verlag, New York, 1991.
Z. Manna and A. Pnueli. Models for reactivity. Acta Informatica, 30:609–678, 1993.
Z. Manna and A. Pnueli. Temporal Verification of Reactive Systems. Springer-Verlag, New York, 1994. To Appear.
V. Nguyen, D. Gries, and S. Owicki. A model and temporal proof system for network of processes. In Proc. 12th ACM Symp. Princ. of Prog. Lang., pages 121–131, 1985.
S. Owicki and L. Lamport. Proving liveness properties of concurrent programs. ACM Trans. Prog. Lang. Sys., 4:455–495, 1982.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1994 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Manna, Z., Pnueli, A. (1994). Temporal verification diagrams. In: Hagiya, M., Mitchell, J.C. (eds) Theoretical Aspects of Computer Software. TACS 1994. Lecture Notes in Computer Science, vol 789. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-57887-0_123
Download citation
DOI: https://doi.org/10.1007/3-540-57887-0_123
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-57887-1
Online ISBN: 978-3-540-48383-0
eBook Packages: Springer Book Archive