Abstract
This paper presents a methodology for the verification of temporal properties of systems based on the gradual construction and algorithmic checking of fairness diagrams. Fairness diagrams correspond to abstractions of the system and its progress properties, and have a simple graphical representation.
In the proposed methodology, a proof of a temporal property consists of a chain of diagram transformations, starting from a diagram representing the original system and ending with a diagram that either corresponds directly to the specification, or that can be shown to satisfy it by purely algorithmic methods. Each diagram transformation captures a natural step of the gradual process of system analysis and proof discovery. The structure of fairness diagrams simplifies reasoning about progress properties, and the graphical representation provided by the diagrams enables the user to direct the construction of the proof. The resulting methodology is complete for proving specifications written in first-order lineartime temporal logic, provided no temporal operator appears in the scope of a quantifier.
This research was supported in part by the National Science Foundation under grant CCR-92-23226, the Advanced Research Projects Agency under NASA grant NAG2-892, the United States Air Force Office of Scientific Research under grant F49620-93-1-0139, and the Department of the Army under grant DAAH04-95-1-0317.
Chapter PDF
Similar content being viewed by others
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
I.A. Browne, Z. Manna, and H.B. Sipma. Generalized verification diagrams. In Found, of Software Technology and Theoretical Comp. Sci., volume 1026 of Lect. Notes in Comp. Sci., pages 484–498. Springer-Verlag, 1995.
L. de Alfaro and Z. Manna. Temporal verification by diagram transformations. Technical report, Stanford University, 1996.
O. Grumberg and D.E. Long. Model checking and modular verification. ACM Trans. Prog. Lang. Sys., 16(3):843–871, May 1994.
Y. Kesten, Z. Manna, and A. Pnueli. Temporal verification of simulation and refinement. In Proc. of the REX Workshop ”A Decade of Concurrency”, volume 803 of Lect. Notes in Comp. Sci., pages 273–346. Springer-Verlag, 1994.
L. Lamport. The temporal logic of actions. ACM Trans. Prog. Lang. Sys., 16(3):872–923, May 1994.
O. Lichtenstein and A. Pnueli. Checking that finite state concurrent programs satisfy their linear specifications. In Proc. 12th ACM Symp. Princ. of Prog. Lang., pages 97–107, 1985.
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 diagrams. In TACS 94, Lect. Notes in Comp. Sci. Springer-Verlag, 1994.
S. Safra. On the complexity of ω-automata. In Proc. 29th IEEE Symp. Found. of Comp. Sci., 1988.
S. Safra and M.Y. Vardi. On ω-automata and temporal logic. In Proc. 21th ACM Symp. Theory of Comp., pages 127–137, 1989.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1996 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
de Alfaro, L., Manna, Z. (1996). Temporal verification by diagram transformations. In: Alur, R., Henzinger, T.A. (eds) Computer Aided Verification. CAV 1996. Lecture Notes in Computer Science, vol 1102. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-61474-5_77
Download citation
DOI: https://doi.org/10.1007/3-540-61474-5_77
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-61474-6
Online ISBN: 978-3-540-68599-9
eBook Packages: Springer Book Archive