Circular Compositional Reasoning about Liveness
Compositional proofs about systems of many components often involve apparently circular arguments. That is, correctness of component A must be assumed when verifying component B, and vice versa. The apparent circularity of such arguments can be resolved by induction over time. However, previous methods for such circular compositional proofs apply only to safety properties. This paper presents a method of circular compositional reasoning that applies to liveness properties as well. It is based on a new circular compositional rule implemented in the SMV proof assistant. The method is illustrated using Tomasulo’s algorithm for out-of-order instruction execution. An implementation is proved live for arbitrary resources using compositional model checking.
- 3.R. Alur and T. A. Henzinger. Reactive modules. In 11th annual IEEE symp. Logic in Computer Science (LICS’ 96), 1996.Google Scholar
- 4.R. Alur, T. A. Henzinger, F. Mang, S. Qadeer, S. K. Rajamani, and S. Tasiran. Mocha:Modularity in model checking.In CAV’ 98, number 1427 LNCS, pages 521–525. Springer-Verlag.Google Scholar
- 5.L. Lamport. The temporal logic of actions. Research report 79,Digital Equipment Corporation, Systems Research Center, Dec. 1991.Google Scholar
- 6.K. L. McMillan. Verification of infinite state systems by compositional model checking. this volume.Google Scholar
- 7.K. L. McMillan. Verification of an implementation of Tomasulo’s algorithm by compositional model checking. In CAV’98,number 1427 in LNCS,pages 100–121. Springer-Verlag, 1998.Google Scholar