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

Taming Concurrency for Verification Using Multiparty Session Types

  • Conference paper
  • First Online:
Theoretical Aspects of Computing – ICTAC 2019 (ICTAC 2019)

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

Included in the following conference series:

Abstract

The additional complexity caused by concurrently communicating processes in distributed systems render the verification of such systems into a very hard problem. Multiparty session types were developed to govern communication and concurrency in distributed systems. As such, they provide an efficient verification method w. r. t. properties about communication and concurrency, like communication safety or progress. However, they do not support the analysis of properties that require the consideration of concrete runs or concrete values of variables. We sequentialise well-typed systems of processes guided by the structure of their global type to obtain interaction-free abstractions thereof. Without interaction, concurrency in the system is reduced to sequential and completely independent parallel compositions. In such abstractions, the verification of properties such as e. g. data-based termination that are not covered by multiparty session types, but rely on concrete runs or values of variables, becomes significantly more efficient.

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

References

  1. Bakst, A., Gleissenthall, K.V., Kıcı, R.G., Jhala, R.: Verifying distributed programs via canonical sequentialization. In: Proceedings of the ACM on Programming Languages 1(OOPSLA), 110:1–110:27 (2017). https://doi.org/10.1145/3133934

    Article  Google Scholar 

  2. Bejleri, A., Yoshida, N.: Synchronous multiparty session types. Electron. Notes Theor. Comput. Sci. 241, 3–33 (2009). https://doi.org/10.1016/j.entcs.2009.06.002

    Article  Google Scholar 

  3. Bettini, L., Coppo, M., D’Antoni, L., De Luca, M., Dezani-Ciancaglini, M., Yoshida, N.: Global progress in dynamically interleaved multiparty sessions. In: van Breugel, F., Chechik, M. (eds.) CONCUR 2008. LNCS, vol. 5201, pp. 418–433. Springer, Heidelberg (2008). https://doi.org/10.1007/978-3-540-85361-9_33

    Chapter  Google Scholar 

  4. Bocchi, L., Chen, T.-C., Demangeon, R., Honda, K., Yoshida, N.: Monitoring networks through multiparty session types. In: Beyer, D., Boreale, M. (eds.) FMOODS/FORTE -2013. LNCS, vol. 7892, pp. 50–65. Springer, Heidelberg (2013). https://doi.org/10.1007/978-3-642-38592-6_5

    Chapter  Google Scholar 

  5. Bocchi, L., Honda, K., Tuosto, E., Yoshida, N.: A theory of design-by-contract for distributed multiparty interactions. In: Gastin, P., Laroussinie, F. (eds.) CONCUR 2010. LNCS, vol. 6269, pp. 162–176. Springer, Heidelberg (2010). https://doi.org/10.1007/978-3-642-15375-4_12

    Chapter  MATH  Google Scholar 

  6. Caires, L., Pérez, J.A.: Multiparty session types within a canonical binary theory, and beyond. In: Albert, E., Lanese, I. (eds.) FORTE 2016. LNCS, vol. 9688, pp. 74–95. Springer, Cham (2016). https://doi.org/10.1007/978-3-319-39570-8_6

    Chapter  MATH  Google Scholar 

  7. Carbone, M., Montesi, F., Schürmann, C.: Choreographies, logically. Distrib. Comput. 31(1), 51–67 (2018). https://doi.org/10.1007/s00446-017-0295-1

    Article  MathSciNet  MATH  Google Scholar 

  8. Cavada, R., et al.: The nuXmv symbolic model checker. In: Biere, A., Bloem, R. (eds.) CAV 2014. LNCS, vol. 8559, pp. 334–342. Springer, Cham (2014). https://doi.org/10.1007/978-3-319-08867-9_22

    Chapter  Google Scholar 

  9. Chandy, K.M., Lamport, L.: Distributed snapshots: determining global states of distributed systems. ACM Trans. Comput. Syst. (TOCS) 3(1), 63–75 (1985). https://doi.org/10.1145/214451.214456

    Article  Google Scholar 

  10. Cruz-Filipe, L., Larsen, K.S., Montesi, F.: The paths to choreography extraction. In: Esparza, J., Murawski, A.S. (eds.) FoSSaCS 2017. LNCS, vol. 10203, pp. 424–440. Springer, Heidelberg (2017). https://doi.org/10.1007/978-3-662-54458-7_25

    Chapter  Google Scholar 

  11. Demangeon, R., Honda, K.: Nested protocols in session types. In: Koutny, M., Ulidowski, I. (eds.) CONCUR 2012. LNCS, vol. 7454, pp. 272–286. Springer, Heidelberg (2012). https://doi.org/10.1007/978-3-642-32940-1_20

    Chapter  Google Scholar 

  12. Glabbeek, R.J.: The linear time — branching time spectrum II. In: Best, E. (ed.) CONCUR 1993. LNCS, vol. 715, pp. 66–81. Springer, Heidelberg (1993). https://doi.org/10.1007/3-540-57208-2_6

    Chapter  Google Scholar 

  13. van Glabbeek, R.: The linear time - branching time spectrum i: the semantics of concrete, sequential processes. Handbook of Process Algebra, pp. 3–99 (2001)

    Google Scholar 

  14. Gorla, D.: Towards a unified approach to encodability and separation results for process calculi. Inf. Comput. 208(9), 1031–1053 (2010). https://doi.org/10.1016/j.ic.2010.05.002

    Article  MathSciNet  MATH  Google Scholar 

  15. Gorla, D., Nestmann, U.: Full abstraction for expressiveness: history, myths and facts. Math. Struct. Comput. Sci. 26(4), 639–654 (2014). https://doi.org/10.1017/S0960129514000279

    Article  MathSciNet  MATH  Google Scholar 

  16. Holzmann, G.J.: Design and Validation of Computer Protocols. Prentice Hall, Upper Saddle River (1991)

    Google Scholar 

  17. Holzmann, G.J.: The model checker SPIN. IEEE Trans. Software Eng. 23(5), 279–295 (1997). https://doi.org/10.1109/32.588521

    Article  Google Scholar 

  18. Honda, K., Mukhamedov, A., Brown, G., Chen, T.-C., Yoshida, N.: Scribbling interactions with a formal foundation. In: Natarajan, R., Ojo, A. (eds.) ICDCIT 2011. LNCS, vol. 6536, pp. 55–75. Springer, Heidelberg (2011). https://doi.org/10.1007/978-3-642-19056-8_4

    Chapter  Google Scholar 

  19. Honda, K., Yoshida, N., Carbone, M.: Multiparty Asynchronous Session Types. In: Proceedings of POPL, vol. 43, pp. 273–284. ACM (2008). https://doi.org/10.1145/1328438.1328472

  20. Honda, K., Yoshida, N., Carbone, M.: Multiparty asynchronous session types. J. ACM (JACM) 63(1) (2016). https://doi.org/10.1145/2827695

    Article  MathSciNet  Google Scholar 

  21. Milner, R., Parrow, J., Walker, D.: A calculus of mobile processes. Inf. Comput. 100(1), 1–77 (1992). https://doi.org/10.1016/0890-5401(92)90008-4

    Article  MathSciNet  MATH  Google Scholar 

  22. Montesi, F.: Choreographic Programming. Ph.D. thesis, IT University of Copenhagen (2013). http://www.fabriziomontesi.com/files/choreographic_programming.pdf

  23. Parrow, J., Sjödin, P.: Multiway synchronization verified with coupled simulation. In: Cleaveland, W.R. (ed.) CONCUR 1992. LNCS, vol. 630, pp. 518–533. Springer, Heidelberg (1992). https://doi.org/10.1007/BFb0084813

    Chapter  Google Scholar 

  24. Peled, D.: Ten years of partial order reduction. In: Hu, A.J., Vardi, M.Y. (eds.) CAV 1998. LNCS, vol. 1427, pp. 17–28. Springer, Heidelberg (1998). https://doi.org/10.1007/BFb0028727

    Chapter  Google Scholar 

  25. Peters, K., van Glabbeek, R.: Analysing and comparing encodability criteria. In: Proceedings of EXPRESS/SOS, EPTCS, vol. 190, pp. 46–60 (2015). https://doi.org/10.4204/EPTCS.190.4

    Article  MathSciNet  Google Scholar 

  26. Peters, K., Wagner, C., Nestmann, U.: taming concurrency for verification using multiparty session types (Technical Report). Technical report, TU Berlin/TU Darmstadt, https://arxiv.org (2019)

  27. Priami, C.: Enhanced Operational Semantics for Concurrency. Ph.D. thesis, Universita’ di Pisa-Genova-Udine, August 1996

    Google Scholar 

  28. Toninho, B., Yoshida, N.: Certifying data in multiparty session types. J. Logical Algebraic Methods Program. 90, 61–83 (2017). https://doi.org/10.1016/j.jlamp.2016.11.005

    Article  MathSciNet  MATH  Google Scholar 

  29. Wagner, C., Nestmann, U.: States in process calculi. In: Proceedings of EXPRESS/SOS, EPTCS, vol. 160, pp. 48–62 (2014). https://doi.org/10.4204/EPTCS.160.6

    Article  MathSciNet  Google Scholar 

  30. Yoshida, N., Deniélou, P.-M., Bejleri, A., Hu, R.: Parameterised multiparty session types. In: Ong, L. (ed.) FoSSaCS 2010. LNCS, vol. 6014, pp. 128–145. Springer, Heidelberg (2010). https://doi.org/10.1007/978-3-642-12032-9_10

    Chapter  Google Scholar 

  31. Yoshida, N., Hu, R., Neykova, R., Ng, N.: The scribble protocol language. In: Abadi, M., Lluch Lafuente, A. (eds.) TGC 2013. LNCS, vol. 8358, pp. 22–41. Springer, Cham (2014). https://doi.org/10.1007/978-3-319-05119-2_3

    Chapter  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. TU Berlin, Berlin, Germany

    Kirstin Peters, Christoph Wagner & Uwe Nestmann

  2. TU Darmstadt, Darmstadt, Germany

    Kirstin Peters

Authors
  1. Kirstin Peters
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Christoph Wagner
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Uwe Nestmann
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Kirstin Peters .

Editor information

Editors and Affiliations

  1. University of Sheffield, Sheffield, UK

    Robert Mark Hierons

  2. University of Bordeaux, Talence, France

    Mohamed Mosbah

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

Peters, K., Wagner, C., Nestmann, U. (2019). Taming Concurrency for Verification Using Multiparty Session Types. In: Hierons, R., Mosbah, M. (eds) Theoretical Aspects of Computing – ICTAC 2019. ICTAC 2019. Lecture Notes in Computer Science(), vol 11884. Springer, Cham. https://doi.org/10.1007/978-3-030-32505-3_12

Download citation

  • DOI: https://doi.org/10.1007/978-3-030-32505-3_12

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-030-32504-6

  • Online ISBN: 978-3-030-32505-3

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation