Nothing Special   »   [go: up one dir, main page]
Skip to main content
Springer Nature Link
Log in

Relating Session Types and Behavioural Contracts: The Asynchronous Case

  • Conference paper
  • First Online:
Software Engineering and Formal Methods (SEFM 2019)

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

Included in the following conference series:

  • 1239 Accesses

Abstract

We discuss the relationship between session types and behavioural contracts under the assumption that processes communicate asynchronously. We show the existence of a fully abstract interpretation of session types into a fragment of contracts, that maps session subtyping into binary compliance-preserving contract refinement. In this way, the recent undecidability result for asynchronous session subtyping can be used to obtain an original undecidability result for asynchronous contract refinement.

Research partly supported by the H2020-MSCA-RISE project ID 778233 “Behavioural Application Program Interfaces (BEHAPI)”.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution

Subscribe and save

Springer+ Basic
$34.99 /Month
  • Get 10 units per month
  • Download Article/Chapter or eBook
  • 1 Unit = 1 Article or 1 Chapter
  • Cancel anytime
Subscribe now

Buy Now

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

Institutional subscriptions

Similar content being viewed by others

Notes

  1. 1.

    As for basic CCS [22] finite-stateness is an obvious consequence of the fact that the process algebra does not include static operators, like parallel or restriction.

  2. 2.

    The correspondence is as follows: the labeled transition systems of the indicated contracts and the corresponding automata in Fig. 1 are isomorphic.

  3. 3.

    As usual, we consider \(\,{::}\,\) right associative.

  4. 4.

    Differently from our definitions, in the channel-based approach of Gay and Hole [17] subtyping is covariant on branchings and contra-variant on selections.

  5. 5.

    Lange and Yoshida [20] independently proved that a slight variant of asynchronous subtyping, called orphan-message-free subtyping was undecidable.

References

  1. Ancona, D., et al.: Behavioral types in programming languages. Found. Trends Program. Lang. 3(2–3), 95–230 (2016)

    Article  Google Scholar 

  2. Baeten, J.C.M., Bravetti, M.: A ground-complete axiomatisation of finite-state processes in a generic process algebra. Math. Struct. Comput. Sci. 18(6), 1057–1089 (2008)

    Article  MathSciNet  Google Scholar 

  3. Bernardi, G.T., Hennessy, M.: Modelling session types using contracts. Math. Struct. Comput. Sci. 26(3), 510–560 (2016)

    Article  MathSciNet  Google Scholar 

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

    Article  MathSciNet  Google Scholar 

  5. Bravetti, M.: Reduction semantics in Markovian process algebra. J. Log. Algebr. Meth. Program. 96, 41–64 (2018)

    Article  MathSciNet  Google Scholar 

  6. Bravetti, M., Carbone, M., Lange, J., Yoshida, N., Zavattaro, G.: A sound algorithm for asynchronous session subtyping. In: Proceedings of 30th International Conference on Concurrency Theory, CONCUR 2019, Leibniz International Proceedings in Informatics. Schloss Dagstuhl (2019, to appear)

    Google Scholar 

  7. Bravetti, M., Carbone, M., Zavattaro, G.: Undecidability of asynchronous session subtyping. Inf. Comput. 256, 300–320 (2017)

    Article  MathSciNet  Google Scholar 

  8. Bravetti, M., Carbone, M., Zavattaro, G.: On the boundary between decidability and undecidability of asynchronous session subtyping. Theor. Comput. Sci. 722, 19–51 (2018)

    Article  MathSciNet  Google Scholar 

  9. Bravetti, M., Lanese, I., Zavattaro, G.: Contract-driven implementation of choreographies. In: Kaklamanis, C., Nielson, F. (eds.) TGC 2008. LNCS, vol. 5474, pp. 1–18. Springer, Heidelberg (2009). https://doi.org/10.1007/978-3-642-00945-7_1

    Chapter  Google Scholar 

  10. 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). https://doi.org/10.1007/978-3-540-75698-9_14

    Chapter  Google Scholar 

  11. Bravetti, M., Zavattaro, G.: Towards a unifying theory for choreography conformance and contract compliance. In: Lumpe, M., Vanderperren, W. (eds.) SC 2007. LNCS, vol. 4829, pp. 34–50. Springer, Heidelberg (2007). https://doi.org/10.1007/978-3-540-77351-1_4

    Chapter  MATH  Google Scholar 

  12. Bravetti, M., Zavattaro, G.: Contract compliance and choreography conformance in the presence of message queues. In: Bruni, R., Wolf, K. (eds.) WS-FM 2008. LNCS, vol. 5387, pp. 37–54. Springer, Heidelberg (2009). https://doi.org/10.1007/978-3-642-01364-5_3

    Chapter  Google Scholar 

  13. Bravetti, M., Zavattaro, G.: On the expressive power of process interruption and compensation. Math. Struct. Comput. Sci. 19(3), 565–599 (2009)

    Article  MathSciNet  Google Scholar 

  14. Castagna, G., Gesbert, N., Padovani, L.: A theory of contracts for web services. In: Proceedings of the 35th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2008, pp. 261–272. ACM (2008)

    Google Scholar 

  15. Chen, T., Dezani-Ciancaglini, M., Scalas, A., Yoshida, N.: On the preciseness of subtyping in session types. Log. Methods Comput. Sci. 13(2) (2017)

    Google Scholar 

  16. de Boer, F.S., Bravetti, M., Lee, M.D., Zavattaro, G.: A petri net based modeling of active objects and futures. Fundam. Inform. 159(3), 197–256 (2018)

    Article  MathSciNet  Google Scholar 

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

    Article  MathSciNet  Google Scholar 

  18. Hu, R., Yoshida, N.: Hybrid session verification through endpoint API generation. In: Stevens, P., Wąsowski, A. (eds.) FASE 2016. LNCS, vol. 9633, pp. 401–418. Springer, Heidelberg (2016). https://doi.org/10.1007/978-3-662-49665-7_24

    Chapter  Google Scholar 

  19. Laneve, C., Padovani, L.: The Must preorder revisited. In: Caires, L., Vasconcelos, V.T. (eds.) CONCUR 2007. LNCS, vol. 4703, pp. 212–225. Springer, Heidelberg (2007). https://doi.org/10.1007/978-3-540-74407-8_15

    Chapter  MATH  Google Scholar 

  20. Lange, J., Yoshida, N.: On the undecidability of asynchronous session subtyping. In: Esparza, J., Murawski, A.S. (eds.) FoSSaCS 2017. LNCS, vol. 10203, pp. 441–457. Springer, Heidelberg (2017). https://doi.org/10.1007/978-3-662-54458-7_26

    Chapter  MATH  Google Scholar 

  21. Lindley, S., Morris, J.G.: Embedding session types in Haskell. Haskell 2016, 133–145 (2016)

    Google Scholar 

  22. Milner, R.: Communication and Concurrency. Prentice Hall, Upper Saddle River (1989)

    MATH  Google Scholar 

  23. Milner, R., Parrow, J., Walker, D.: A calculus of mobile processes I/II. Inf. Comput. 100(1), 1–40 (1992)

    Article  MathSciNet  Google Scholar 

  24. Mostrous, D., Yoshida, N.: Session typing and asynchronous subtyping for the higher-order \(\pi \)-calculus. Inf. Comput. 241, 227–263 (2015)

    Article  MathSciNet  Google Scholar 

  25. Mostrous, D., Yoshida, N., Honda, K.: Global principal typing in partially commutative asynchronous sessions. In: Castagna, G. (ed.) ESOP 2009. LNCS, vol. 5502, pp. 316–332. Springer, Heidelberg (2009). https://doi.org/10.1007/978-3-642-00590-9_23

    Chapter  Google Scholar 

  26. Neykova, R., Hu, R., Yoshida, N., Abdeljallal, F.: A session type provider: compile-time API generation for distributed protocols with interaction refinements in F\(\sharp \). In: CC 2018. ACM (2018)

    Google Scholar 

  27. Orchard, D.A., Yoshida, N.: Effects as sessions, sessions as effects. POPL 2016, 568–581 (2016)

    MATH  Google Scholar 

  28. Padovani, L.: A simple library implementation of binary sessions. J. Funct. Program. 27, e4 (2017)

    Article  MathSciNet  Google Scholar 

  29. Scalas, A., Yoshida, N.: Lightweight session programming in scala. In: ECOOP 2016, pp. 21:1–21:28 (2016)

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Department of Computer Science and Engineering & Focus Team, Inria, University of Bologna, Bologna, Italy

    Mario Bravetti & Gianluigi Zavattaro

Authors
  1. Mario Bravetti
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Gianluigi Zavattaro
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Mario Bravetti .

Editor information

Editors and Affiliations

  1. University of Oslo, Oslo, Norway

    Peter Csaba Ölveczky

  2. University of Grenoble Alpes, Montbonnot, France

    Gwen Salaün

Rights and permissions

Reprints and permissions

Copyright information

© 2019 Springer Nature Switzerland AG

About this paper

Check for updates. Verify currency and authenticity via CrossMark

Cite this paper

Bravetti, M., Zavattaro, G. (2019). Relating Session Types and Behavioural Contracts: The Asynchronous Case. In: Ölveczky, P., Salaün, G. (eds) Software Engineering and Formal Methods. SEFM 2019. Lecture Notes in Computer Science(), vol 11724. Springer, Cham. https://doi.org/10.1007/978-3-030-30446-1_2

Download citation

  • DOI: https://doi.org/10.1007/978-3-030-30446-1_2

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-030-30445-4

  • Online ISBN: 978-3-030-30446-1

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation