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

Corinne, a Tool for Choreography Automata

  • Conference paper
  • First Online:
Formal Aspects of Component Software (FACS 2021)

Part of the book series: Lecture Notes in Computer Science ((LNPSE,volume 13077))

Included in the following conference series:

Abstract

Choreography automata are a model of choreographies envisaging high-level views of the behaviour of communicating systems as finite-state automata. The behaviour of each participant of a choreography can be obtained via a projection operation from a choreography automaton. The system of participants obtained by projection is well-behaved if the choreography automaton satisfies some well-formedness conditions. We present Corinne, a tool allowing one to render, compute projections of and compose choreography automata, as well as to check well-formedness conditions.

Research partly supported by the EU H2020 RISE programme under the Marie Skłodowska-Curie grant agreement No 778233, by the MIUR project PRIN 2017FTXR7S “IT-MaTTerS" (Methods and Tools for Trustworthy Smart Systems), and by the Progetto di Ateneo Pia.Ce.Ri - UNICT. The third and fourth authors have also been partially supported by INdAM as members of GNCS (Gruppo Nazionale per il Calcolo Scientifico). The authors thank the reviewers for their interesting comments and suggestions, which helped us to improve the paper. The third author wishes to thank also Mariangiola Dezani-Ciancaglini for her support.

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

    In [4] also minimisation is performed, but this is not needed for the correctness of the constructions, and it is not currently performed by

  2. 2.

    Determinisation required for projection is computed using the classical subset construction for FSAs with \(\epsilon \)-transitions.

References

  1. Barbanera, F., de’Liguoro, U., Hennicker, R.: Global types for open systems. In: Bartoletti, M., Knight, S. (eds.) ICE, EPTCS, vol. 279, pp. 4–20 (2018)

    Google Scholar 

  2. Barbanera, F., de’Liguoro, U., Hennicker, R.: Connecting open systems of communicating finite state machines. J. Logic Algebr. Methods Program. 109 (2019). https://doi.org/10.1016/j.jlamp.2019.07.004. Extended version of [1]

  3. Barbanera, F., Dezani-Ciancaglini, M., Lanese, I., Tuosto, E.: Composition and decomposition of multiparty sessions. J. Logic Algebr. Methods Program. 119, 100620 (2021)

    Google Scholar 

  4. Barbanera, F., Lanese, I., Tuosto, E.: Choreography automata. In: Bliudze, S., Bocchi, L. (eds.) COORDINATION 2020. LNCS, vol. 12134, pp. 86–106. Springer, Cham (2020). https://doi.org/10.1007/978-3-030-50029-0_6

    Chapter  Google Scholar 

  5. Barbanera, F., Lanese, I., Tuosto, E.: Composition of choreography automata. Technical reports 2107.06727, Arxiv, July 2021. http://arxiv.org/abs/2107.06727

  6. Basile, D., ter Beek, M.H., Pugliese, R.: Synthesis of orchestrations and choreographies: bridging the gap between supervisory control and coordination of services. Logic. Methods Comput. Sci. 16(2) (2020)

    Google Scholar 

  7. Basile, D., Degano, P., Ferrari, G.-L., Tuosto, E.: Playing with our CAT and communication-centric applications. In: Albert, E., Lanese, I. (eds.) FORTE 2016. LNCS, vol. 9688, pp. 62–73. Springer, Cham (2016). https://doi.org/10.1007/978-3-319-39570-8_5

    Chapter  Google Scholar 

  8. Basile, D., Degano, P., Ferrari, G., Tuosto, E.: Relating two automata-based models of orchestration and choreography. J. Logic Algebr. Methods Program. 85(3), 425–446 (2016)

    Article  MathSciNet  Google Scholar 

  9. Basile, D., ter Beek, M.H.: A clean and efficient implementation of choreography synthesis for behavioural contracts. In: Damiani, F., Dardha, O. (eds.) COORDINATION 2021. LNCS, vol. 12717, pp. 225–238. Springer, Cham (2021). https://doi.org/10.1007/978-3-030-78142-2_14

    Chapter  Google Scholar 

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

    Article  MathSciNet  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. Carbone, M., Honda, K., Yoshida, N.: Structured communication-centred programming for web services. In: De Nicola, R. (ed.) ESOP 2007. LNCS, vol. 4421, pp. 2–17. Springer, Heidelberg (2007). https://doi.org/10.1007/978-3-540-71316-6_2

    Chapter  MATH  Google Scholar 

  13. Carbone, M., Montesi, F.: Deadlock-freedom-by-design: multiparty asynchronous global programming. In: POPL, pp. 263–274 (2013). https://doi.org/10.1145/2429069.2429101

  14. Corinne github repository. https://github.com/lanese/corinne-3

  15. Coto, A., Guanciale, R., Lange, J., Tuosto, E.: ChorGram: tool support for choreographic development (2015). https://bitbucket.org/emlio_tuosto/chorgram/wiki/Home

  16. Coto, A., Guanciale, R., Tuosto, E.: An abstract framework for choreographic testing. In: Lange, J., Mavridou, A., Safina, L., Scalas, A. (eds.) Proceedings 13th Interaction and Concurrency Experience, ICE 2020, Online, 19 June 2020. EPTCS, vol. 324, pp. 43–60 (2020)

    Google Scholar 

  17. Coto, A., Guanciale, R., Tuosto, E.: Choreographic development of message-passing applications. In: Bliudze, S., Bocchi, L. (eds.) COORDINATION 2020. LNCS, vol. 12134, pp. 20–36. Springer, Cham (2020). https://doi.org/10.1007/978-3-030-50029-0_2

    Chapter  Google Scholar 

  18. Coto, A., Guanciale, R., Tuosto, E.: An abstract framework for choreographic testing. J. Logic Algebraic Methods Program. 123, 100712 (2021). Extended version of [16]

    Google Scholar 

  19. Cruz-Filipe, L., Montesi, F.: Procedural choreographic programming. In: Bouajjani, A., Silva, A. (eds.) FORTE 2017. LNCS, vol. 10321, pp. 92–107. Springer, Cham (2017). https://doi.org/10.1007/978-3-319-60225-7_7

    Chapter  Google Scholar 

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

  21. Dezani-Ciancaglini, M., Ghilezan, S., Jaksic, S., Pantovic, J., Yoshida, N.: Precise subtyping for synchronous multiparty sessions. In: Gay, S., Alglave, J. (eds.) Proceedings Eighth International Workshop on Programming Language Approaches to Concurrency- and Communication-cEntric Software, PLACES 2015, London, UK, 18th April 2015. EPTCS, vol. 203, pp. 29–43 (2015). https://doi.org/10.4204/EPTCS.203.3

  22. Domitilla github repository. https://github.com/dedo94/Domitilla

  23. The DOT Language. https://graphviz.org/doc/info/lang.html

  24. Fu, X., Bultan, T., Su, J.: Conversation protocols: a formalism for specification and verification of reactive electronic services. Theoret. Comput. Sci. 328(1–2), 19–37 (2004). https://doi.org/10.1016/.tcs.2004.07.004

  25. Graphviz 0.16 - Simple Python interface for Graphviz. https://pypi.org/project/graphviz/

  26. Honda, K., Yoshida, N., Carbone, M.: Multiparty asynchronous session types. In: Necula, G.C., Wadler, P. (eds.) POPL, pp. 273–284. ACM Press (2008)

    Google Scholar 

  27. Hüttel, H., et al.: Foundations of session types and behavioural contracts. ACM Comput. Surv. 49(1), 3:1–3:36 (2016)

    Google Scholar 

  28. Kavantzas, N., Burdett, D., Ritzinger, G., Fletcher, T., Lafon, Y., Barreto, C.: Web services choreography description language version 1.0. Technical report, W3C (2005). http://www.w3.org/TR/ws-cdl-10/

  29. Lange, J., Tuosto, E., Yoshida, N.: A tool for choreography-based analysis of message-passing software. In: Gay, S., Ravara, A. (eds.) Behavioural Types: From Theory to Tools, chap. 6, pp. 125–146. Automation, Control and Robotics, River (2017)

    Google Scholar 

  30. Ng, N., Yoshida, N., Honda, K.: Multiparty session c: safe parallel programming with message optimisation. In: Furia, C.A., Nanz, S. (eds.) TOOLS 2012. LNCS, vol. 7304, pp. 202–218. Springer, Heidelberg (2012). https://doi.org/10.1007/978-3-642-30561-0_15

    Chapter  Google Scholar 

  31. OMG: Business Process Model and Notation (BPMN), Version 2.0, January 2011. https://www.omg.org/spec/BPMN

  32. Parr, T.: Antlr. https://www.antlr.org/index.html

  33. Severi, P., Dezani-Ciancaglini, M.: Observational equivalence for multiparty sessions. Fundam. Informaticae 170(1–3), 267–305 (2019). https://doi.org/10.3233/FI-2019-1863

  34. TKinter - Python interface to Tcl/Tk. https://docs.python.org/3/library/tkinter.html

  35. Tuosto, E., Guanciale, R.: Semantics of global view of choreographies. J. Logic Algebr. Methods Program. 95, 17–40 (2018)

    Article  MathSciNet  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. University of Bologna, Bologna, Italy

    Simone Orlando & Vairo Di Pasquale

  2. Department of Mathematics and Computer Science, University of Catania, Catania, Italy

    Franco Barbanera

  3. Focus Team, University of Bologna/INRIA, Bologna, Italy

    Ivan Lanese

  4. Gran Sasso Science Institute, L’Aquila, Italy

    Emilio Tuosto

Authors
  1. Simone Orlando
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Vairo Di Pasquale
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Franco Barbanera
    View author publications

    You can also search for this author in PubMed Google Scholar

  4. Ivan Lanese
    View author publications

    You can also search for this author in PubMed Google Scholar

  5. Emilio Tuosto
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Grenoble Alpes University, Saint-Martin-d'Hères, France

    Gwen Salaün

  2. Eindhoven University of Technology, Eindhoven, The Netherlands

    Anton Wijs

Rights and permissions

Reprints and permissions

Copyright information

© 2021 Springer Nature Switzerland AG

About this paper

Check for updates. Verify currency and authenticity via CrossMark

Cite this paper

Orlando, S., Pasquale, V.D., Barbanera, F., Lanese, I., Tuosto, E. (2021). Corinne, a Tool for Choreography Automata. In: Salaün, G., Wijs, A. (eds) Formal Aspects of Component Software. FACS 2021. Lecture Notes in Computer Science(), vol 13077. Springer, Cham. https://doi.org/10.1007/978-3-030-90636-8_5

Download citation

  • DOI: https://doi.org/10.1007/978-3-030-90636-8_5

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-030-90635-1

  • Online ISBN: 978-3-030-90636-8

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation