Abstract
Assume-guarantee reasoning has long been advertised as an important method for decomposing proof obligations in system verification. Refinement mappings (homomorphisms) have long been advertised as an important method for solving the language-inclusion problem in practice. When confronted with large verification problems, we therefore attempted to make use of both techniques. We soon found that rather than offering instant solutions, the success of assume-guarantee reasoning depends critically on the construction of suitable abstraction modules, and the success of refinement checking depends critically on the construction of suitable witness modules. Moreover, as abstractions need to be witnessed, and witnesses abstracted, the process must be iterated. We present here the main lessons we learned from our experiments, in limn of a systematic and structured discipline for the compositional verification of reactive modules. An infrastructure to support this discipline, and automate parts of the verification, has been implemented in the tool Mocha.
This work is supported in part by ONR YIP award N00014-95-1-0520, by NSF CAREER award CCR-9501708, by NSF grant CCR-9504469, by ARO MURI grant DAAH-04-96-1-0341, and by the SRC contract 97-DC-324.041.
Chapter PDF
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
R. Alur and T.A. Henzinger. Reactive modules. In Proceedings of the 11th Annual Symposium on Logic in Computer Science, pages 207–218. IEEE Computer Society Press, 1996.
R. Alur, TA. Henzinger, F.Y.C. Mang, S. Qadeer, S.K. Rajamani, and S. Tasiran. Mocha: Modularity in model checking. In A. Hu and M. Vardi, editors, CAV 98: Computer Aided Verification, Lecture Notes in Computer Science. Springer-Verlag, 1998.
M. Abadi and L. Lamport. The existence of refinement mappings. Theoretical Computer Science, 82(2):253–284, 1991.
M. Abadi and L. Lamport. Conjoining specifications. ACM Transactions on Programming Languages and Systems, 17(3):507–534, 1995.
S. Bensalem, A. Bouajjani, C. Loiseaux, and J. Sifakis. Property-preserving simulations. In G. von Bochmann and D.K. Probst, editors, CAV 92: Computer Aided Verification, Lecture Notes in Computer Science 663, pages 260–273. Springer-Verlag, 1992.
E.M. Clarke, O. Grumberg, and D.E. Long. Model checking and abstraction. In Proceedings of the 19th Annual Symposium on Principles of Prograrnrning Languages, pages 343–354. ACM Press, 1992.
E.M. Clarke, D.E. Long, and K.L. McMillan. Compositional model checking. In Proceedings of the 4th Annual Symposium on Logic in Computer Science, pages 353–362. IEEE Computer Society Press, 1989.
W. Damm and A. Pnueli. Verifying out-of-order executions. In Proceedings of the IFIP Working Conference on Correct Hardware Design and Verification Methods, CHARME, 1997.
O. Grumberg and D.E. Long. Model checking and modular verification. ACM Transactions on Programming Languages and Systems, 16(3):843–871, 1994.
T.A. Henzinger, S. Qadeer, and S.K. Rajamani. You assume, we guarantee: Methodology and case studies. Technical report, Electronics Research Lab, Univ. of California, Berkeley, CA 94720, 1998.
R.P. Kurshan. Computer-aided Verification of Coordinating Processes. Princeton University Press, 1994.
L. Lamport. Specifying concurrent program modules. ACM Transactions on Programming Languages and Systems, 5(2):190–222, 1983.
N.A. Lynch and M.R. Tuttle. Hierarchical correctness proofs for distributed algorithms. In Proceedings of the 6th Annual Symposium on Principles of Distributed Computing, pages 137–151. ACM Press, 1987.
N.A. Lynch and F. Vaandrager. Forward and backward simulations, Part l: Untimed systems. Information and Computation, 121(2):214–233, 1995.
K.L. McMillan. A compositional rule for hardware design refinement. In O. Grumberg, editor, CAV 97: Computer Aided Verification, Lecture Notes in Computer Science 1254, pages 24–35. Springer-Verlag, 1997.
K.L. McMillan. Verification of an implementation of Tomasulo's algorithm by compositional model checking. In A. Hu and M. Vardi, editors, CAV 98: Computer Aided Verification, Lecture Notes in Computer Science. Springer-Verlag, 1998.
E. W. Stark. A proof technique for rely/guarantee properties. In Proceedings of the 5th Conference on Foundations of Software Technology and Theoretical Computer Science, Lecture Notes in Computer Science 206, pages 369–391. Springer-Verlag, 1985.
Andrew S. Tanenbaum. Computer Networks. Prentice-Hall Inc., 1992.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1998 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Henzinger, T.A., Qadeer, S., Rajamani, S.K. (1998). You assume, we guarantee: Methodology and case studies. In: Hu, A.J., Vardi, M.Y. (eds) Computer Aided Verification. CAV 1998. Lecture Notes in Computer Science, vol 1427. Springer, Berlin, Heidelberg. https://doi.org/10.1007/BFb0028765
Download citation
DOI: https://doi.org/10.1007/BFb0028765
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-64608-2
Online ISBN: 978-3-540-69339-0
eBook Packages: Springer Book Archive