Abstract
In the compositional verification of a concurrent system, one seeks to deduce properties of the system from properties of its constituent modules. This paper supplements our previous work on the same subject to provide a comprehensive compositional framework in linear-time temporal logic. It has been shown by many that specifying properties of a module in the assumption-guarantee style is effective in achieving compositionality. We consider two forms of temporal formulas that correspond to two interpretations of an assumption-guarantee specification and investigate how they can be applied in compositional verification. We argue by examples that the two forms complement each other and both are needed to facilitate the compositional approach. We also show how to handle assumption-guarantee specifications where the assumption contains a liveness property.
This research was supported in part by grants NSC 86-2213-E-002-002 and NSC 87-2213-E-002-015 from the National Science Council, Taiwan (R.O.C.) and a research award from College of Management, National Taiwan University.
Chapter PDF
Similar content being viewed by others
References
M. Abadi and L. Lamport. Composing specifications. ACM Transactions on Programming Languages and Systems, 15(1):73–132, January 1993.
M. Abadi and L. Lamport. Conjoining specifications. ACM Transactions on Programming Languages and Systems, 17(3):507–534, May 1995.
M. Abadi and G.D. Plotkin. A logical view of composition. Theoretical Computer Science, 114(1):3–30, June 1993.
R. Alur and T.A. Henzinger. Local liveness for compositional modeling of fair reactive systems. In Computer Aided Verification, Proceedings of the 7th International Conference, LNCS 939, pages 166–179, 1995.
A. Aziz, T.R. Shiple, V. Singhal, and A.L. Sangiovanni-Vincentelli. Formula-dependent equivalence for compositional CTL model checking. In Computer Aided Verification, LNCS 818, pages 324–337, June 1994.
H. Barringer and R. Kuiper. Hierarchical development of concurrent systems in a temporal logic framework. In S.D. Brookes, A.W. Roscoe, and G. Winskel, editors, Seminar on Concurrency, LNCS 197, pages 35–61. Springer-Verlag, 1984.
K.M. Chandy and J. Misra. Parallel Program Design: A Foundation. Addison-Wesley, 1988.
E.M. Clarke, D.E. Long, and K.L. McMillan. Compositional model checking. In Proceedings of the 4th IEEE Symposium on Logic in Computer Science, pages 353–362, 1989.
P. Collette. Application of the composition principle to Unity-like specifications. In TAPSOFT’ 93: Theory and Practice of Software Development, LNCS 668, pages 230–242. Springer-Verlag, 1993.
P. Collette. Design of Compositional Proof Systems Based on Assumption-Guarantee Specifications — Application to UNITY. PhD thesis, Université Catholique de Louvain, June 1994.
W.-P. de Roever, H. Langmåck, and A. Pnueli. Compositionality: The Significant Difference. Springer-Verlag, 1998. Lecture Notes in Computer Science 1536.
P. Grønning, T.Q. Nielsen, and H.H. Løvengreen. Refinement and composition of transition-based rely-guarantee specifications with auxiliary variables. In K.V. Nori and C.E. Veni Madhavan, editors, Foundations of Software Technology and Theoretical Computer Science, LNCS 472, pages 332–348. Springer-Verlag, 1991.
O. Grumberg and D.E. Long. Model checking and modular verification. ACM Transactions on Programming Languages and Systems, 16(3):843–871, May 1994.
C.A.R. Hoare. An axiomatic basis for computer programs. Communications of the ACM, 12(8):576–580, 1969.
C.B. Jones. Tentative steps towards a development method for interfering programs. ACM Transactions on Programming Languages and Systems, 5(4):596–619, October 1983.
B. Jonsson and Y.-K. Tsay. Assumption/guarantee specifications in linear-time temporal logic. Theoretical Computer Science, 167:47–72, October 1996. An extended abstract appeared earlier in TAPSOFT’ 95, LNCS 915.
O. Kupferman and M.Y. Vardi. Module checking. In O. Grumberg, editor, Computer-Aided Verification, CAV’ 96, LNCS 1102, pages 75–86. Springer-Verlag, August 1996.
O. Kupferman and M.Y. Vardi. Module checking revisited. In Computer-Aided Verification, CAV’ 97, LNCS 1254. Springer-Verlag, June 1997.
L. Lamport. Specifying concurrent program modules. ACM Transactions on Programming Languages and Systems, 5(2):190–222, 1983.
L. Lamport. The temporal logic of actions. ACM Transactions on Programming Languages and Systems, 16(3):872–923, May 1994.
Z. Manna and A. Pnueli. The Temporal Logic of Reactive and Concurrent Systems: Specification. Springer-Verlag, 1992.
Z. Manna and A. Pnueli. Temporal Verification of Reactive Systems: Safety. Springer-Verlag, 1995.
J. Misra and K.M. Chandy. Proofs of networks of processes. IEEE Transactions on Software Engineering, 7(4):417–426, July 1981.
A. Pnueli. The temporal semantics of concurrent programs. Theoretical Computer Science, 13:45–60, 1982.
Y.-K. Tsay. Compositional verification in linear-time temporal logic (the full version). Send requests to tsay@im.ntu.edu.tw.
M.Y. Vardi. On the complexity of modular model checking. In Proceedings of the 10th IEEE Symposium on Logic in Computer Science, pages 101–111, June 1995.
Q. Xu, A. Cau, and P. Collette. On unifying assumption-commitment style proof rules for concurrency. In B. Jonsson and J. Parrow, editors, CONCUR’ 94: Concurrency Theory, LNCS 836, pages 267–282. Springer-Verlag, 1994.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2000 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Tsay, YK. (2000). Compositional Verification in Linear-Time Temporal Logic. In: Tiuryn, J. (eds) Foundations of Software Science and Computation Structures. FoSSaCS 2000. Lecture Notes in Computer Science, vol 1784. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-46432-8_23
Download citation
DOI: https://doi.org/10.1007/3-540-46432-8_23
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-67257-9
Online ISBN: 978-3-540-46432-7
eBook Packages: Springer Book Archive