Abstract
We explore the question of the composition of invariance specifications in a context of formal methods applied to concurrent and reactive systems. Depending on how compositionality is stated and how invariants are defined, invariance specifications may or may not be compositional. This paper examines three classic forms of invariants and their compositional properties. After pointing out what we see as deficiencies of these kinds of invariants, a new fourth form is defined and shown to have useful compositional properties that the more classic forms do not enjoy.
This is a preview of subscription content, log in via an institution.
Buying options
Tax calculation will be finalised at checkout
Purchases are for personal use only
Learn about institutional subscriptionsReferences
Abadi, M., Lamport, L.: Composing specifications. ACM Transactions on Programming Languages and Systems 15(1), 73–132 (1993)
Abadi, M., Lamport, L.: Conjoining specifications. ACM Transactions on Programming Languages and Systems 17(3), 507–534 (1995)
Chandy, K.M., Charpentier, M.: An experiment in program composition and proof. Formal Methods in System Design 20(1), 7–21 (2002)
Chandy, K.M., Misra, J.: Parallel Program Design: A Foundation. Addison-Wesley, Reading (1988)
Chandy, K.M., Sanders, B.: Reasoning about program composition, http://www.cise.ufl.edu/~sanders/pubs/composition.ps
Charpentier, M.: Reasoning about composition: A predicate transformer approach. In: Specification and Verification of Component-Based Systems (SAVCBS 2001). Workshop at OOPSLA 2001, October 2001, pp. 42–49 (2001)
Charpentier, M.: An approach to composition motivated by wp. In: Kutsche, R.-D., Weber, H. (eds.) FASE 2002. LNCS, vol. 2306, pp. 1–14. Springer, Heidelberg (2002)
Charpentier, M.: Composing invariants. Technical Report 03-10, University of New Hampshire (May 2003)
Charpentier, M., Chandy, K.M.: Examples of program composition illustrating the use of universal properties. In: Rolim, J.D.P. (ed.) IPPS-WS 1999 and SPDP-WS 1999. LNCS, vol. 1586, pp. 1215–1227. Springer, Heidelberg (1999)
Charpentier, M., Chandy, K.M.: Towards a compositional approach to the design and verification of distributed systems. In: Wing, J.M., Woodcock, J.C.P., Davies, J. (eds.) FM 1999. LNCS, vol. 1708, pp. 570–589. Springer, Heidelberg (1999)
Charpentier, M., Chandy, K.M.: Reasoning about composition using property transformers and their conjugates. In: Watanabe, O., Hagiya, M., Ito, T., van Leeuwen, J., Mosses, P.D. (eds.) TCS 2000. LNCS, vol. 1872, pp. 580–595. Springer, Heidelberg (2000)
Charpentier, M., Chandy, K.M.: Theorems about composition. In: Backhouse, R., Oliveira, J.N. (eds.) MPC 2000. LNCS, vol. 1837, pp. 167–186. Springer, Heidelberg (2000)
Collette, P.: Design of Compositional Proof Systems Based on Assumption- Commitment Specifications. Application to Unity. Doctoral thesis, Faculté des Sciences Appliquées, Université Catholique de Louvain (June 1994)
de Roever, W.-P., de Boer, F., Hannemann, U., Hooman, J., Lakhnech, Y., Poel, M., Zwiers, J.: Concurrency Verification: Introduction to Compositional and Noncompositional Methods, November 2001. Cambridge University Press, Cambridge (2001)
de Roever, W.-P., Langmaack, H., Pnueli, A. (eds.): COMPOS 1997. LNCS, vol. 1536. Springer, Heidelberg (1998)
Dijkstra, E.W., Scholten, C.S.: Predicate calculus and program semantics. Texts and monographs in computer science. Springer, Heidelberg (1990)
Fiadeiro, J.L., Maibaum, T.: Verifying for reuse: foundations of object-oriented system verification. In: Makie, I., Hankin, C., Nagarajan, R. (eds.) Theory and Formal Methods, pp. 235–257. World Scientific, Singapore (1995)
Finkbeiner, B., Manna, Z., Sipma, H.B.: Deductive verification of modular systems. In: de Roever et al. [15], pp. 239–275
Lamport, L.: The Temporal Logic of Actions. ACM Transactions on Programming Languages and Systems 16(3), 872–923 (1994)
Lamport, L.: Composition: A way to make proofs harder. In: de Roever et al. [15], pp. 402–423
Lamport, L.: Specifying Systems: The TLA+ Language and Tools for Hardware and Software Engineers, July 2002. Addison-Wesley, Reading (2002)
Rustan, K., Leino, M., Nelson, G., Saxe, J.B.: ESC/Java User’s Manual. Compaq Systems Research Center (October 2000)
Manna, Z., Pnueli, A.: The Temporal Logic of Reactive and Concurrent Systems: Specification. Springer, Heidelberg (1992)
Meier, D., Sanders, B.: Composing leads-to properties. Theoretical Computer Science 243(1-2), 339–361 (2000)
Misra, J.: The importance of ensuring. In: Notes on Unity. Department of Computer Science, University of Texas at Austin, Note 11 (1990)
Misra, J.: A logic for concurrent programming: Progress. Journal of Computer and Software Engineering 3(2), 273–300 (1995)
Misra, J.: A logic for concurrent programming: Safety. Journal of Computer and Software Engineering 3(2), 239–272 (1995)
Owicki, S., Gries, D.: An axiomatic proof technique for parallel programs. Acta Informatica 6, 319–340 (1976)
Sanders, B.A.: Eliminating the substitution axiom from Unity logic. Formal Aspects of Computing 3(2), 189–205 (1991)
Udink, R.T.: Program Refinement in Unity-like Environments. PhD thesis, Utrecht University (September 1995)
Xu, Q., de Roever, W.-P., He, J.: The rely-guarantee method for verifying shared variable concurrent programs. Formal Aspects of Computing 9(2), 149–174 (1997)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2003 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Charpentier, M. (2003). Composing Invariants. In: Araki, K., Gnesi, S., Mandrioli, D. (eds) FME 2003: Formal Methods. FME 2003. Lecture Notes in Computer Science, vol 2805. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-45236-2_23
Download citation
DOI: https://doi.org/10.1007/978-3-540-45236-2_23
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-40828-4
Online ISBN: 978-3-540-45236-2
eBook Packages: Springer Book Archive