Abstract
In this paper we present a visual approach to proving progress properties of parameterized systems using induction on verification diagrams. The inductive hypothesis is represented by an automaton and is based on a state-dependent order on process indices, for increased flexibility. This approach yields more intuitive proofs for progress properties and simpler verification conditions that are more likely to be proved automatically.
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
M. Abadi and L. Lamport. Composing specifications. In Stepwise Refinement of Distributed Systems: Models, Formalism, Correctness, vol. 430 of LNCS, pages 1–41. Springer-Verlag, 1990.
N.S. Bjørner, U. Lerner, and Z. Manna. Deductive verification of parameterized fault-tolerant systems: A case study. In Intl. Conf. on Temporal Logic. Kluwer, 1997. To appear.
A. Browne, Z. Manna, and H.B. Sipma. Generalized temporal verification diagrams. In 15th Conference on the Foundations of Software Technology and Theoretical Computer Science, vol. 1026 of LNCS, pages 484–498. Springer-Verlag, 1995.
A. Browne, Z. Manna, and H.B. Sipma. Hierarchical verification using verification diagrams. In 2nd Asian Computing Science Conf., vol. 1179 of LNCS, pages 276–286. Springer-Verlag, December 1996.
L. Lamport. A new solution of Dijkstra’s concurrent programming problem. Communications of the ACM, 17(8):435–455, 1974.
L. Lamport. Proving the correctness of multiprocess programs. IEEE Trans. Software Engin., 3:125–143, 1977.
Z. Manna, A. Browne, H.B. Sipma, and T.E. Uribe. Visual abstractions for temporal verification. In A. Haeberer, editor, AMAST’98, vol. 1548 of LNCS, pages 28–41. Springer-Verlag, December 1998.
Z. Manna and A. Pnueli. Temporal verification diagrams. In M. Hagiya and J.C. Mitchell, editors, Proc. International Symposium on Theoretical Aspects of Computer Software, vol. 789 of LNCS, pages 726–765. Springer-Verlag, 1994.
Z. Manna and A. Pnueli. Temporal Verification of Reactive Systems: Safety. Springer-Verlag, New York, 1995.
Z. Manna and A. Pnueli. Temporal verification of reactive systems: Progress. Draft Manuscript, 1996.
A. Pnueli. Lecture notes: the Bakery algorithm. Draft Manuscript, Weizmann Institute of Science, Israel, May 1996.
W. Thomas. Automata on infinite objects. In J. van Leeuwen, editor, Handbook of Theoretical Computer Science, vol. B, pages 133–191. Elsevier Science Publishers (North-Holland), 1990.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 1999 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Manna, Z., Sipma, H.B. (1999). Verification of Parameterized Systems by Dynamic Induction. In: Halbwachs, N., Peled, D. (eds) Computer Aided Verification. CAV 1999. Lecture Notes in Computer Science, vol 1633. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-48683-6_5
Download citation
DOI: https://doi.org/10.1007/3-540-48683-6_5
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-66202-0
Online ISBN: 978-3-540-48683-1
eBook Packages: Springer Book Archive