Skip to main content
SpringerLink
Log in
Book cover

International Conference on Concurrency Theory

CONCUR 2010: CONCUR 2010 - Concurrency Theory pp 162–176Cite as

A Theory of Design-by-Contract for Distributed Multiparty Interactions

  • Conference paper

Part of the book series: Lecture Notes in Computer Science ((LNTCS,volume 6269))

Abstract

Design by Contract (DbC) promotes reliable software development through elaboration of type signatures for sequential programs with logical predicates. This paper presents an assertion method, based on the π-calculus with full recursion, which generalises the notion of DbC to multiparty distributed interactions to enable effective specification and verification of distributed multiparty protocols. Centring on global assertions and their projections onto endpoint assertions, our method allows clear specifications for typed sessions, constraining the content of the exchanged messages, the choice of sub-conversations to follow, and invariants on recursions. The paper presents key theoretical foundations of this framework, including a sound and relatively complete compositional proof system for verifying processes against assertions.

This work is partially supported by EPSRC EP/F003757, EP/F002114, EP/G015635 and EP/G015481, Leverhulme Trust Award “Tracing Networks”.

This is a preview of subscription content, 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 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

Learn about institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. Acciai, L., Borale, M.: A type system for client progress in a service-oriented calculus. In: Degano, P., De Nicola, R., Meseguer, J. (eds.) Concurrency, Graphs and Models. LNCS, vol. 5065, pp. 625–641. Springer, Heidelberg (2008)

    Chapter  Google Scholar 

  2. Berger, M., Honda, K., Yoshida, N.: Completeness and logical full abstraction for modal logics for the typed π-calculus. In: Aceto, L., Damgård, I., Goldberg, L.A., Halldórsson, M.M., Ingólfsdóttir, A., Walukiewicz, I. (eds.) ICALP 2008, Part II. LNCS, vol. 5126, pp. 99–111. Springer, Heidelberg (2008)

    Chapter  Google Scholar 

  3. Bettini, L., et al.: Global Progress in Dynamically Interfered Multiparty Sessions. In: van Breugel, F., Chechik, M. (eds.) CONCUR 2008. LNCS, vol. 5201, pp. 418–433. Springer, Heidelberg (2008)

    Chapter  Google Scholar 

  4. Bhargavan, K., Corin, R., Deniélou, P.M., Fournet, C., Leifer, J.: Cryptographic protocol synthesis and verification for multiparty sessions. In: CSF, pp. 124–140 (2009)

    Google Scholar 

  5. Bhargavan, K., Fournet, C., Gordon, A.D.: Modular verification of security protocol code by typing. In: POPL, pp. 445–456 (2010)

    Google Scholar 

  6. Bonelli, E., Compagnoni, A., Gunter, E.: Correspondence assertions for process synchronization in concurrent communications. JFC 15(2), 219–247 (2005)

    MATH  MathSciNet  Google Scholar 

  7. Bravetti, M., Zavattaro, G.: A foundational theory of contracts for multi-party service composition. Fundamenta Informaticae XX, 1–28 (2008)

    MathSciNet  Google Scholar 

  8. Buscemi, M., Montanari, U.: CC-Pi: A constraint-based language for specifying service level agreements. In: De Nicola, R. (ed.) ESOP 2007. LNCS, vol. 4421, pp. 18–32. Springer, Heidelberg (2007)

    Chapter  Google Scholar 

  9. Caires, L., Vieira, H.T.: Conversation types. In: Castagna, G. (ed.) ESOP 2009. LNCS, vol. 5502, pp. 285–300. Springer, Heidelberg (2009)

    Chapter  Google Scholar 

  10. Castagna, G., Padovani, L.: Contracts for mobile processes. In: Bravetti, M., Zavattaro, G. (eds.) CONCUR 2009. LNCS, vol. 5710, pp. 211–228. Springer, Heidelberg (2009)

    Chapter  Google Scholar 

  11. Dam, M.: Proof systems for pi-calculus logics. In: Logic for Concurrency and Synchronisation. Trends in Logic, Studia Logica Library, pp. 145–212. Kluwer, Dordrecht (2003)

    Google Scholar 

  12. De Nicola, R., et al.: A Basic Calculus for Modelling Service Level Agreements. In: Coordination. LNCS, vol. 3454, pp. 33–48. Springer, Heidelberg (2005)

    Google Scholar 

  13. Floyd, R.W.: Assigning meaning to programs. In: Proc. Symp. in Applied Mathematics, vol. 19 (1967)

    Google Scholar 

  14. Frankel, D.S.: Model Driven Architecture: Applying MDA to Enterprise Computing. Wiley, Chichester (2003)

    Google Scholar 

  15. Freeman, T., Pfenning, F.: Refinement types for ml. SIGPLAN Not. 26(6), 268–277 (1991)

    Article  Google Scholar 

  16. Guttman, J.D., et al.: Trust management in strand spaces: A rely-guarantee method. In: Schmidt, D. (ed.) ESOP 2004. LNCS, vol. 2986, pp. 325–339. Springer, Heidelberg (2004)

    Chapter  Google Scholar 

  17. Hennessy, M., Milner, R.: Algebraic laws for non-determinism and concurrency. JACM 32(1) (1985)

    Google Scholar 

  18. Hoare, T.: An axiomatic basis of computer programming. CACM 12 (1969)

    Google Scholar 

  19. Honda, K., Vasconcelos, V.T., Kubo, M.: Language primitives and type disciplines for structured communication-based programming. In: Hankin, C. (ed.) ESOP 1998. LNCS, vol. 1381, pp. 22–138. Springer, Heidelberg (1998)

    Google Scholar 

  20. Honda, K., Yoshida, N., Carbone, M.: Multiparty asynchronous session types. In: POPL, pp. 273–284. ACM, New York (2008)

    Google Scholar 

  21. The Java Modeling Language (JML) Home Page

    Google Scholar 

  22. Jones, C.B.: Specification and design of (parallel) programs. In: IFIP Congress, pp. 321–332 (1983)

    Google Scholar 

  23. Leino, K.R.M.: Verifying object-oriented software: Lessons and challenges. In: Grumberg, O., Huth, M. (eds.) TACAS 2007. LNCS, vol. 4424, p. 2. Springer, Heidelberg (2007)

    Chapter  Google Scholar 

  24. Mendelson, E.: Introduction to Mathematical Logic. Wadsworth Inc., Bermont (1987)

    Google Scholar 

  25. Meyer, B.: Applying “Design by Contract”. Computer 25(10), 40–51 (1992)

    Article  Google Scholar 

  26. Meyer, B.: Object-Oriented Software Construction, ch. 31. Prentice Hall, Englewood Cliffs (1997)

    MATH  Google Scholar 

  27. Nienaltowski, P., Meyer, B., Ostroff, J.S.: Contracts for concurrency. Form. Asp. Comput. 21(4), 305–318 (2009)

    Article  MATH  Google Scholar 

  28. OMG: Object Constraint Language Version 2.0 (May 2006)

    Google Scholar 

  29. Peyton Jones, S., et al.: Composing contracts: an adventure in financial engineering. In: ICFP, pp. 281–292. ACM, New York (2000)

    Google Scholar 

  30. Pierce, B.C.: Types and Programming Languages. MIT Press, Cambridge (2002)

    Google Scholar 

  31. Full version of this paper, http://www.cs.le.ac.uk/people/lb148/fullpaper.html

  32. SAVARA JBoss Project webpage, http://www.jboss.org/savara

  33. Vallecillo, A., Vasconcelos, V.T., Ravara, A.: Typing the behavior of objects and components using session types. Fundamenta Informaticæ 73(4), 583–598 (2006)

    MATH  MathSciNet  Google Scholar 

  34. Xi, H., Pfenning, F.: Dependent types in practical programming. In: POPL, pp. 214–227. ACM, New York (1999)

    Google Scholar 

  35. Xu, D., Peyton Jones, S.: Static contract checking for Haskell. In: POPL, pp. 41–52. ACM, New York (2009)

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. University of Leicester,  

    Laura Bocchi & Emilio Tuosto

  2. Queen Mary, University of London,  

    Kohei Honda

  3. Imperial College London,  

    Nobuko Yoshida

Authors
  1. Laura Bocchi
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Kohei Honda
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Emilio Tuosto
    View author publications

    You can also search for this author in PubMed Google Scholar

  4. Nobuko Yoshida
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Laboratoire Spécification et Vérification (LSV), ENS de Cachan & CNRS, 94235, Cachan cedex, France

    Paul Gastin

  2. LIAFA, Université Paris Diderot, 75205, Paris cedex, France

    François Laroussinie

Rights and permissions

Reprints and permissions

Copyright information

© 2010 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Bocchi, L., Honda, K., Tuosto, E., Yoshida, N. (2010). A Theory of Design-by-Contract for Distributed Multiparty Interactions. In: Gastin, P., Laroussinie, F. (eds) CONCUR 2010 - Concurrency Theory. CONCUR 2010. Lecture Notes in Computer Science, vol 6269. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-15375-4_12

Download citation

  • DOI: https://doi.org/10.1007/978-3-642-15375-4_12

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-642-15374-7

  • Online ISBN: 978-3-642-15375-4

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation