Skip to main content
SpringerLink
Log in
Book cover

Programming Languages with Applications to Biology and Security pp 103–121Cite as

Compliance in Behavioural Contracts: A Brief Survey

  • Chapter
  • First Online:

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

Abstract

Behavioural contracts are formal specifications of interaction protocols between two or more distributed services. Despite the heterogeneous nature of the formalisms for behavioural contracts that have appeared in the literature, most of them feature a notion of compliance, which characterises when two or more contracts lead to correct interactions between services respecting them. We discuss and compare a selection of these notions in four different models of contracts: \(\tau \)-less CCS, session types, interface automata, and contract automata.

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   39.99
Price excludes VAT (USA)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD   54.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

References

  1. Acciai, L., Boreale, 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. 642–658. Springer, Heidelberg (2008)

    Chapter  Google Scholar 

  2. Acciai, L., Boreale, M., Zavattaro, G.: Behavioural contracts with request-response operations. In: Clarke, D., Agha, G. (eds.) COORDINATION 2010. LNCS, vol. 6116, pp. 16–30. Springer, Heidelberg (2010)

    Chapter  Google Scholar 

  3. Barbanera, F., de’Liguoro, U.: Two notions of sub-behaviour for session-based client/server systems. In: Proceedings of PPDP, pp. 155–164 (2010)

    Google Scholar 

  4. Barbanera, F., de’Liguoro, U.: Loosening the notions of compliance and sub-behaviour in client/server systems. In: Proceedings of ICE. EPTCS, vol. 166, pp. 94–110 (2014)

    Google Scholar 

  5. Barbanera, F., Dezani-Ciancaglini, M., Lanese, I., de’Liguoro, U.: Retractable contracts. In: Proceedings of PLACES. EPTCS (2015) (to appear)

    Google Scholar 

  6. Barbanera, F., van Bakel, S., de’Liguoro, U.: Orchestrated compliance for session-based client/server interactions. In: Proceedings of ICE. EPTCS (2015) (to appear)

    Google Scholar 

  7. Bartoletti, M., Cimoli, T., Murgia, M., Podda, A.S., Pompianu, L.: Compliance and subtyping in timed session types. In: Proceedings of FORTE, pp. 161–177 (2015)

    Google Scholar 

  8. Bartoletti, M., Cimoli, T., Pinna, G.M.: Lending Petri Nets and contracts. In: Arbab, F., Sirjani, M. (eds.) FSEN 2013. LNCS, vol. 8161, pp. 66–82. Springer, Heidelberg (2013)

    Chapter  Google Scholar 

  9. Bartoletti, M., Cimoli, T., Pinna, G.M.: Lending Petri nets. Science of Computer Programming (2015) (to appear)

    Google Scholar 

  10. Bartoletti, M., Cimoli, T., Pinna, G.M., Zunino, R.: Contracts as games on event structures. JLAMP (2015) (to appear)

    Google Scholar 

  11. Bartoletti, M., Cimoli, T., Zunino, R.: A theory of agreements and protection. In: Basin, D., Mitchell, J.C. (eds.) POST 2013 (ETAPS 2013). LNCS, vol. 7796, pp. 186–205. Springer, Heidelberg (2013)

    Chapter  Google Scholar 

  12. Bartoletti, M., Degano, P., Ferrari, G.L.: Types and effects for secure service orchestration, pp. 57–69. In: Proceedings of IEEE Computer Security Foundations Workshop (2006)

    Google Scholar 

  13. Bartoletti, M., Degano, P., Ferrari, G.L.: Planning and verifying service composition. J. Comput. Secur. 17(5), 799–837 (2009)

    Article  Google Scholar 

  14. Bartoletti, M., Degano, P., Ferrari, G.L., Zunino, R.: Semantics-based design for secure Web services. IEEE Trans. Software Eng. 34(1), 33–49 (2008)

    Article  Google Scholar 

  15. Bartoletti, M., Lange, J., Scalas, A., Zunino, R.: Choreographies in the wild. Science of Computer Programming (2015)

    Google Scholar 

  16. Bartoletti, M., Scalas, A., Tuosto, E., Zunino, R.: Honesty by typing. In: Boreale, M., Beyer, D. (eds.) FORTE 2013 and FMOODS 2013. LNCS, vol. 7892, pp. 305–320. Springer, Heidelberg (2013)

    Chapter  Google Scholar 

  17. Bartoletti, M., Scalas, A., Zunino, R.: A semantic deconstruction of session types. In: Baldan, P., Gorla, D. (eds.) CONCUR 2014. LNCS, vol. 8704, pp. 402–418. Springer, Heidelberg (2014)

    Google Scholar 

  18. Bartoletti, M., Tuosto, E., Zunino, R.: On the realizability of contracts in dishonest systems. In: Sirjani, M. (ed.) COORDINATION 2012. LNCS, vol. 7274, pp. 245–260. Springer, Heidelberg (2012)

    Chapter  Google Scholar 

  19. Basile, D., Degano, P., Ferrari, G.-L.: Automata for analysing service contracts. In: Maffei, M., Tuosto, E. (eds.) TGC 2014. LNCS, vol. 8902, pp. 34–50. Springer, Heidelberg (2014)

    Google Scholar 

  20. Basile, D., Degano, P., Ferrari, G.L., Tuosto, E.: From orchestration to choreography through contract automata. In: Proceedings of ICE, pp. 67–85 (2014)

    Google Scholar 

  21. Basu, S., Bultan, T., Ouederni, M.: Deciding choreography realizability. In: Proceedings of POPL, pp. 191–202 (2012)

    Google Scholar 

  22. Bernardi, G., Dardha, O., Gay, S.J., Kouzapas, D.: On duality relations for session types. In: Maffei, M., Tuosto, E. (eds.) TGC 2014. LNCS, vol. 8902, pp. 51–66. Springer, Heidelberg (2014)

    Google Scholar 

  23. Bernardi, G., Hennessy, M.: Compliance and testing preorders differ. In: Counsell, S., Núñez, M. (eds.) SEFM 2013. LNCS, vol. 8368, pp. 69–81. Springer, Heidelberg (2014)

    Chapter  Google Scholar 

  24. Bordeaux, L., Salaün, G., Berardi, D., Mecella, M.: When are two web services compatible? In: Shan, M.-C., Dayal, U., Hsu, M. (eds.) TES 2004. LNCS, vol. 3324, pp. 15–28. Springer, Heidelberg (2005)

    Chapter  Google Scholar 

  25. Brand, D., Zafiropulo, P.: On communicating finite-state machines. J. ACM 30(2), 323–342 (1983)

    Article  MathSciNet  MATH  Google Scholar 

  26. Bravetti, M., Zavattaro, G.: Contract based multi-party service composition. In: Arbab, F., Sirjani, M. (eds.) FSEN 2007. LNCS, vol. 4767, pp. 207–222. Springer, Heidelberg (2007)

    Chapter  Google Scholar 

  27. Bravetti, M., Zavattaro, G.: Contract compliance and choreography conformance in the presence of message queues. In: Proceedings of WS-FM, pp. 37–54 (2008)

    Google Scholar 

  28. Bravetti, M., Zavattaro, G.: A theory of contracts for strong service compliance. Math. Struct. Comput. Sci. 19(3), 601–638 (2009)

    Article  MathSciNet  MATH  Google Scholar 

  29. E. Brinksma, A. Rensink, and W. Vogler. Fair testing. In Proc. CONCUR, pages 313–327, 1995

    Google Scholar 

  30. Bugliesi, M., Macedonio, D., Pino, L., Rossi, S.: Compliance preorders for Web services. In: Proceedings of WS-FM, pp. 76–91 (2009)

    Google Scholar 

  31. Buscemi, M.G., Melgratti, H.C.: Contracts for abstract processes in service composition. In: Proceedings of FIT, pp. 9–27 (2010)

    Google Scholar 

  32. Carpineti, S., Castagna, G., Laneve, C., Padovani, L.: A formal account of contracts for Web services. In: Proceedings of WS-FM, pp. 148–162 (2006)

    Google Scholar 

  33. Castagna, G., Dezani-Ciancaglini, M., Giachino, E., Padovani, L.: Foundations of session types. In: Proceedings of PPDP (2009)

    Google Scholar 

  34. Castagna, G., Gesbert, N., Padovani, L.: A theory of contracts for Web services. ACM TOPLAS 31(5), 19:1–19:61 (2009)

    Article  MATH  Google Scholar 

  35. Cécé, G., Finkel, A.: Verification of programs with half-duplex communication. Inf. Comput. 202(2), 166–190 (2005)

    Article  MathSciNet  MATH  Google Scholar 

  36. Coppo, M., Dezani-Ciancaglini, M., Yoshida, N.: Asynchronous session types and progress for object oriented languages. In: Bonsangue, M.M., Johnsen, E.B. (eds.) FMOODS 2007. LNCS, vol. 4468, pp. 1–31. Springer, Heidelberg (2007)

    Chapter  Google Scholar 

  37. de Alfaro, L., Henzinger, T.A.: Interface automata. In: Proceedings of ACM SIGSOFT, pp. 109–120 (2001)

    Google Scholar 

  38. De Nicola, R., Hennessy, M.: Testing equivalences for processes. Theor. Comput. Sci. 34, 83–133 (1984)

    Article  MathSciNet  MATH  Google Scholar 

  39. De Nicola, R., Hennessy, M.: CCS without tau’s. In: Proceedings of TAPSOFT, pp. 138–152 (1987)

    Google Scholar 

  40. Deniélou, P.-M., Yoshida, N.: Multiparty session types meet communicating automata. In: Seidl, H. (ed.) Programming Languages and Systems. LNCS, vol. 7211, pp. 194–213. Springer, Heidelberg (2012)

    Chapter  Google Scholar 

  41. Deniélou, P.-M., Yoshida, N.: Multiparty compatibility in communicating automata: characterisation and synthesis of global session types. In: Fomin, F.V., Freivalds, R., Kwiatkowska, M., Peleg, D. (eds.) ICALP 2013, Part II. LNCS, vol. 7966, pp. 174–186. Springer, Heidelberg (2013)

    Google Scholar 

  42. Gay, S., Hole, M.: Subtyping for session types in the Pi calculus. Acta Inf. 42(2), 191–225 (2005)

    Article  MathSciNet  MATH  Google Scholar 

  43. Honda, K.: Types for dyadic interaction. In: Best, E. (ed.) CONCUR 1993. LNCS, vol. 715. Springer, Heidelberg (1993)

    Google Scholar 

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

    Chapter  Google Scholar 

  45. Honda, K., Yoshida, N., Carbone, M.: Multiparty asynchronous session types. In: Proceedings of POPL, pp. 273–284 (2008)

    Google Scholar 

  46. Hüttel, H. et al.: Foundations of behavioural types (2015). (Submitted) www.behavioural-types.eu/publications/WG1-State-of-the-Art.pdf

  47. Laneve, C., Laneve, C., Padovani, L., Padovani, L.: The Must preorder revisited. In: Caires, L., Caires, L., Vasconcelos, V.T., Vasconcelos, V.T. (eds.) CONCUR 2007. LNCS, vol. 4703, pp. 212–225. Springer, Heidelberg (2007)

    Chapter  Google Scholar 

  48. Laneve, C., Padovani, L.: The pairing of contracts and session types. In: Degano, P., De Nicola, R., Meseguer, J. (eds.) Concurrency, Graphs and Models. LNCS, vol. 5065, pp. 681–700. Springer, Heidelberg (2008)

    Chapter  Google Scholar 

  49. Laneve, C., Padovani, L.: An algebraic theory for Web service contracts. Formal Aspects of Computing, pp. 1–28 (2015)

    Google Scholar 

  50. Lange, J., Tuosto, E.: Synthesising Choreographies from local session types. In: Koutny, M., Ulidowski, I. (eds.) CONCUR 2012. LNCS, vol. 7454, pp. 225–239. Springer, Heidelberg (2012)

    Chapter  Google Scholar 

  51. Lange, J., Tuosto, E., Yoshida, N.: From communicating machines to graphical choreographies. In: Proceedings of POPL, pp. 221–232 (2015)

    Google Scholar 

  52. Milner, R.: Communication and concurrency. Prentice-Hall Inc. (1989)

    Google Scholar 

  53. Rensink, A., Vogler, W.: Fair testing. Inf. Comput. 205(2), 125–198 (2007)

    Article  MathSciNet  MATH  Google Scholar 

  54. nSangiorgi, D.: An introduction to bisimulation and coinduction. Cambridge University Press, Cambridge (2012)

    MATH  Google Scholar 

  55. Scalas, A.: A semantic deconstruction of session types. PhD thesis, University of Cagliari (2015)

    Google Scholar 

  56. van der Aalst, W.M.P., Lohmann, N., Massuthe, P., Stahl, C., Wolf, K.: Multiparty contracts: Agreeing and implementing interorganizational processes. Comput. J. 53(1), 90–106 (2010)

    Article  Google Scholar 

Download references

Acknowledgment

We warmly thank Emilio Tuosto and the anonymous reviewers for their insightful comments. This work has been partially supported by Aut. Reg. of Sardinia grants L.R.7/2007 CRP-17285 (TRICS) and P.I.A. 2010 (“Social Glue”), by MIUR PRIN 2010-11 project “Security Horizons”, and by EU COST Action IC1201 “Behavioural Types for Reliable Large-Scale Software Systems” (BETTY).

Author information

Authors and Affiliations

  1. Università Degli Studi di Cagliari, Cagliari, Italy

    Massimo Bartoletti & Tiziana Cimoli

  2. Università Degli Studi di Trento, Trento, Italy

    Roberto Zunino

Authors
  1. Massimo Bartoletti
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Tiziana Cimoli
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Roberto Zunino
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Massimo Bartoletti .

Editor information

Editors and Affiliations

  1. Dipartimento di Informatica, Università di Pisa, Pisa, Italy

    Chiara Bodei

  2. Dipartimento di Informatica, Università di Pisa, Pisa, Italy

    Gianluigi Ferrari

  3. Università degli Studi di Trento, Povo, Italy

    Corrado Priami

Rights and permissions

Reprints and permissions

Copyright information

© 2015 Springer International Publishing Switzerland

About this chapter

Cite this chapter

Bartoletti, M., Cimoli, T., Zunino, R. (2015). Compliance in Behavioural Contracts: A Brief Survey. In: Bodei, C., Ferrari, G., Priami, C. (eds) Programming Languages with Applications to Biology and Security. Lecture Notes in Computer Science(), vol 9465. Springer, Cham. https://doi.org/10.1007/978-3-319-25527-9_9

Download citation

  • DOI: https://doi.org/10.1007/978-3-319-25527-9_9

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-319-25526-2

  • Online ISBN: 978-3-319-25527-9

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation