Skip to main content
SpringerLink
Log in

Composing Invariants

  • Conference paper
  • First Online:
FME 2003: Formal Methods (FME 2003)

Part of the book series: Lecture Notes in Computer Science ((LNCS,volume 2805))

Included in the following conference series:

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 to check access.

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 84.99
Price excludes VAT (USA)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 109.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

References

  1. Abadi, M., Lamport, L.: Composing specifications. ACM Transactions on Programming Languages and Systems 15(1), 73–132 (1993)

    Article  Google Scholar 

  2. Abadi, M., Lamport, L.: Conjoining specifications. ACM Transactions on Programming Languages and Systems 17(3), 507–534 (1995)

    Article  Google Scholar 

  3. Chandy, K.M., Charpentier, M.: An experiment in program composition and proof. Formal Methods in System Design 20(1), 7–21 (2002)

    Article  Google Scholar 

  4. Chandy, K.M., Misra, J.: Parallel Program Design: A Foundation. Addison-Wesley, Reading (1988)

    MATH  Google Scholar 

  5. Chandy, K.M., Sanders, B.: Reasoning about program composition, http://www.cise.ufl.edu/~sanders/pubs/composition.ps

  6. 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)

    Google Scholar 

  7. 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)

    Chapter  Google Scholar 

  8. Charpentier, M.: Composing invariants. Technical Report 03-10, University of New Hampshire (May 2003)

    Google Scholar 

  9. 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)

    Chapter  Google Scholar 

  10. 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)

    Chapter  Google Scholar 

  11. 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)

    Chapter  Google Scholar 

  12. 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)

    Chapter  Google Scholar 

  13. 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)

    Google Scholar 

  14. 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)

    MATH  Google Scholar 

  15. de Roever, W.-P., Langmaack, H., Pnueli, A. (eds.): COMPOS 1997. LNCS, vol. 1536. Springer, Heidelberg (1998)

    Google Scholar 

  16. Dijkstra, E.W., Scholten, C.S.: Predicate calculus and program semantics. Texts and monographs in computer science. Springer, Heidelberg (1990)

    Book  Google Scholar 

  17. 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)

    Google Scholar 

  18. Finkbeiner, B., Manna, Z., Sipma, H.B.: Deductive verification of modular systems. In: de Roever et al. [15], pp. 239–275

    Google Scholar 

  19. Lamport, L.: The Temporal Logic of Actions. ACM Transactions on Programming Languages and Systems 16(3), 872–923 (1994)

    Article  Google Scholar 

  20. Lamport, L.: Composition: A way to make proofs harder. In: de Roever et al. [15], pp. 402–423

    Google Scholar 

  21. Lamport, L.: Specifying Systems: The TLA+ Language and Tools for Hardware and Software Engineers, July 2002. Addison-Wesley, Reading (2002)

    Google Scholar 

  22. Rustan, K., Leino, M., Nelson, G., Saxe, J.B.: ESC/Java User’s Manual. Compaq Systems Research Center (October 2000)

    Google Scholar 

  23. Manna, Z., Pnueli, A.: The Temporal Logic of Reactive and Concurrent Systems: Specification. Springer, Heidelberg (1992)

    Book  Google Scholar 

  24. Meier, D., Sanders, B.: Composing leads-to properties. Theoretical Computer Science 243(1-2), 339–361 (2000)

    Article  MathSciNet  Google Scholar 

  25. Misra, J.: The importance of ensuring. In: Notes on Unity. Department of Computer Science, University of Texas at Austin, Note 11 (1990)

    Google Scholar 

  26. Misra, J.: A logic for concurrent programming: Progress. Journal of Computer and Software Engineering 3(2), 273–300 (1995)

    Google Scholar 

  27. Misra, J.: A logic for concurrent programming: Safety. Journal of Computer and Software Engineering 3(2), 239–272 (1995)

    Google Scholar 

  28. Owicki, S., Gries, D.: An axiomatic proof technique for parallel programs. Acta Informatica 6, 319–340 (1976)

    Article  MathSciNet  Google Scholar 

  29. Sanders, B.A.: Eliminating the substitution axiom from Unity logic. Formal Aspects of Computing 3(2), 189–205 (1991)

    Article  Google Scholar 

  30. Udink, R.T.: Program Refinement in Unity-like Environments. PhD thesis, Utrecht University (September 1995)

    Google Scholar 

  31. 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)

    Article  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Department of Computer Science, University of New Hampshire, Durham, NH, USA

    Michel Charpentier

Authors
  1. Michel Charpentier
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Department of Computer Science and Communication Engineering, Graduate School of Information Science and Electrical Engineering, Kyushu University, 6-10-1-Hakozaki, Higashi-ku, 812-8581, Fukuoka, Japan

    Keijiro Araki

  2. Istituto di Scienza e Tecnologie dell’Informazione “A. Faedo”, ISTI - CNR, Pisa, Italy

    Stefania Gnesi

  3. Dipartimento di Elettronica e Informazione, Politecnico di Milano, Italy

    Dino Mandrioli

Rights and permissions

Reprints 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

Publish with us

Policies and ethics

Search

Navigation