Abstract
The simulation preorder on state transition systems is widely accepted as a useful notion of refinement, both in its own right and as an efficiently checkable sufficient condition for trace containment. For composite systems, due to the exponential explosion of the state space, there is a need for decomposing a simulation check of the form P< s Q into simpler simulation checks on the components of P and Q. We present an assume-guarantee rule that enables such a decomposition. To the best of our knowledge, this is the first assume-guarantee rule that applies to a refinement relation different from trace containment. Our rule is circular, and its soundness proof requires induction on trace trees. The proof is constructive: given simulation relations that witness the simulation preorder between corresponding components of P and Q, we provide a procedure for constructing a witness relation for P< s Q. We also extend our assume-guarantee rule to account for fairness assumptions on transition systems.
This research was supported in part by the Office of Naval Research Young Investigator award N00014-95-1-0520, by the National Science Foundation CAREER award CCR-9501708, by the National Science Foundation grant CCR-9504469, by the Defense Advanced Research Projects Agency grant NAG2-1214, by the Army Research Office MURI grant DAAH-04-96-1-0341, and by the Semiconductor Research Corporation contract 97-DC-324.041.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
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.
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.
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.
D.L. Dill. Trace Theory for Automatic Hierarchical Verification of Speed-independent Circuits. The MIT Press, 1989.
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, O. Kupferman, and S. K. Rajamani. Fair simulation. In CONCUR 97: Theories of Concurrency, Lecture Notes in Computer Science 1243, pages 273–287. Springer-Verlag, July 1997.
R.P. Kurshan. Computer-aided Verification of Coordinating Processes. Princeton University Press, 1994.
N.A. Lynch. Distributed Algorithms. Morgan-Kaufmann, 1996.
K.L. McMillan. A compositional rule for hardware design refinement. In CAV 97: Computer-Aided Verification, Lecture Notes in Computer Science1254, pages 24–35. Springer-Verlag, 1997.
R. Milner. An algebraic definition of simulation between programs. In Proceedings of the 2nd International Joint Conference on Artificial Intelligence, pages 481–489. The British Computer Society, 1971.
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.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 1998 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Henzinger, T.A., Qadeer, S., Rajamani, S.K., TaŞiran, S. (1998). An Assume-Guarantee Rule for Checking Simulation. In: Gopalakrishnan, G., Windley, P. (eds) Formal Methods in Computer-Aided Design. FMCAD 1998. Lecture Notes in Computer Science, vol 1522. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-49519-3_27
Download citation
DOI: https://doi.org/10.1007/3-540-49519-3_27
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-65191-8
Online ISBN: 978-3-540-49519-2
eBook Packages: Springer Book Archive