Top

Published in:

2024 | OriginalPaper | Chapter

Overview on Constrained Multiparty Synchronisation in Team Automata

Author : José Proença

Published in: Formal Aspects of Component Software

Publisher: Springer Nature Switzerland

Activate our intelligent search to find suitable subject content or patents.

search-config

AI-assisted search

Off

Abstract

This paper provides an overview on recent work on Team Automata, whereby a network of automata interacts by synchronising actions from multiple senders and receivers. We further revisit this notion of synchronisation in other well known concurrency models, such as Reo, BIP, Choreography Automata, and Multiparty Session Types.

We address realisability of Team Automata, i.e., how to infer a network of interacting automata from a global specification, taking into account that this realisation should satisfy exactly the same properties as the global specification. In this analysis we propose a set of interesting directions of challenges and future work in the context of Team Automata or similar concurrency models.

Dont have a licence yet? Then find out more about our products and how to get one now:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

Mit Springer Professional "Wirtschaft+Technik" erhalten Sie Zugriff auf:

über 102.000 Bücher
über 537 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Finance + Banking
Management + Führung
Marketing + Vertrieb
Maschinenbau + Werkstoffe
Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

inform now

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 390 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Maschinenbau + Werkstoffe

Jetzt Wissensvorsprung sichern!

inform now

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 340 Zeitschriften

aus folgenden Fachgebieten:

Bauwesen + Immobilien
Business IT + Informatik
Finance + Banking
Management + Führung
Marketing + Vertrieb
Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

inform now

previous chapter Formal Aspects of Component Software

next chapter Embedding Formal Verification in Model-Driven Software Engineering with Slco: An Overview

Arbach, Y., Karcher, D.S., Peters, K., Nestmann, U.: Dynamic causality in event structures. Log. Methods Comput. Sci. 14(1) (2018). https://doi.org/10.23638/LMCS-14(1:17)2018

Baier, C., Sirjani, M., Arbab, F., Rutten, J.J.M.M.: Modeling component connectors in Reo by constraint automata. Sci. Comput. Program. 61(2), 75–113 (2006). https://doi.org/10.1016/j.scico.2005.10.008MathSciNetCrossRef

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_6CrossRef

Barbanera, F., Lanese, I., Tuosto, E.: Formal choreographic languages. In: ter Beek, M.H., Sirjani, M. (eds.) COORDINATION. LNCS, vol. 13271, pp. 121–139. Springer, Cham (2022). https://doi.org/10.1007/978-3-031-08143-9_8

ter Beek, M.H.: Team automata: a formal approach to the modeling of collaboration between system components. Ph.D. thesis, Leiden University (2003)

ter Beek, M.H., Carmona, J., Hennicker, R., Kleijn, J.: Communication requirements for team automata. In: Jacquet, J.-M., Massink, M. (eds.) COORDINATION 2017. LNCS, vol. 10319, pp. 256–277. Springer, Cham (2017). https://doi.org/10.1007/978-3-319-59746-1_14CrossRef

ter Beek, M.H., Carmona, J., Kleijn, J.: Conditions for compatibility of components. In: Margaria, T., Steffen, B. (eds.) ISoLA 2016. LNCS, vol. 9952, pp. 784–805. Springer, Cham (2016). https://doi.org/10.1007/978-3-319-47166-2_55CrossRef

ter Beek, M.H., Cledou, G., Hennicker, R., Proença, J.: Featured team automata. In: Huisman, M., Păsăreanu, C., Zhan, N. (eds.) FM 2021. LNCS, vol. 13047, pp. 483–502. Springer, Cham (2021). https://doi.org/10.1007/978-3-030-90870-6_26CrossRef

ter Beek, M.H., Ellis, C.A., Kleijn, J., Rozenberg, G.: Synchronizations in team automata for groupware systems. Comput. Sup. Coop. Work 12(1), 21–69 (2003). https://doi.org/10.1023/A:1022407907596CrossRef

10.

ter Beek, M.H., Gadducci, F., Janssens, D.: A calculus for team automata. ENTCS 195, 41–55 (2008). https://doi.org/10.1016/j.entcs.2007.08.022CrossRef

11.

ter Beek, M.H., Hennicker, R., Kleijn, J.: Compositionality of safe communication in systems of team automata. In: Pun, V.K.I., Stolz, V., Simao, A. (eds.) ICTAC 2020. LNCS, vol. 12545, pp. 200–220. Springer, Cham (2020). https://doi.org/10.1007/978-3-030-64276-1_11CrossRef

12.

ter Beek, M.H., Hennicker, R., Proença, J.: Realisability of global models of interaction. In: Ábrahám, E., Dubslaff, C., Tarifa, S.L.T. (eds.) Theoretical Aspects of Computing – ICTAC 2023. LNCS, vol. 14446, pp. 236–255. Springer, Cham (2023). https://doi.org/10.1007/978-3-031-47963-2_15

13.

ter Beek, M.H., Kleijn, J.: Team automata satisfying compositionality. In: Araki, K., Gnesi, S., Mandrioli, D. (eds.) FME 2003. LNCS, vol. 2805, pp. 381–400. Springer, Heidelberg (2003). https://doi.org/10.1007/978-3-540-45236-2_22CrossRef

14.

ter Beek, M.H., Kleijn, J.: Vector team automata. Theor. Comput. Sci. 429, 21–29 (2012). https://doi.org/10.1016/j.tcs.2011.12.020MathSciNetCrossRef

15.

ter Beek, M.H., Lenzini, G., Petrocchi, M.: Team automata for security: a survey. Electron. Notes Theor. Comput. Sci. 128(5), 105–119 (2005). https://doi.org/10.1016/j.entcs.2004.11.044CrossRef

16.

ter Beek, M.H., Cledou, G., Hennicker, R., Proença, J.: Can we communicate? Using dynamic logic to verify team automata. In: Chechik, M., Katoen, J.P., Leucker, M. (eds.) Proceedings of the 25th International Symposium on Formal Methods (FM 2023). LNCS, vol. 14000. Springer, Cham (2023). https://doi.org/10.1007/978-3-031-27481-7_9

17.

ter Beek, M.H., Lenzini, G., Petrocchi, M.: A team automaton scenario for the analysis of security properties of communication protocols. J. Autom. Lang. Comb. 11(4), 345–374 (2006). https://doi.org/10.25596/jalc-2006-345

18.

Behrmann, G., David, A., Larsen, K.G.: A tutorial on Uppaal. In: Bernardo, M., Corradini, F. (eds.) Formal Methods for the Design of Real-Time Systems, International School on Formal Methods for the Design of Computer, Communication and Software Systems, SFM-RT 2004, Bertinoro, Italy, 13–18 September 2004, Revised Lectures. LNCS, vol. 3185, pp. 200–236. Springer, Cham (2004). https://doi.org/10.1007/978-3-540-30080-9_7

19.

van Benthem, J., van Eijck, J., Stebletsova, V.: Modal logic, transition systems and processes. J. Log. Comput. 4(5), 811–855 (1994). https://doi.org/10.1093/logcom/4.5.811MathSciNetCrossRef

20.

Bliudze, S., Sifakis, J.: The algebra of connectors - structuring interaction in BIP. IEEE Trans. Comput. 57(10), 1315–1330 (2008). https://doi.org/10.1109/TC.2008.26MathSciNetCrossRef

21.

Bunte, O., et al.: The mCRL2 toolset for analysing concurrent systems. In: TACAS. LNCS, vol. 11428, pp. 21–39. Springer, Cham (2019). https://doi.org/10.1007/978-3-030-17465-1_2

22.

Carmona, J., Kleijn, J.: Compatibility in a multi-component environment. Theor. Comput. Sci. 484, 1–15 (2013). https://doi.org/10.1016/j.tcs.2013.03.006MathSciNetCrossRef

23.

de Alfaro, L., Henzinger, T.A.: Interface automata. In: ESEC/FSE, pp. 109–120. ACM (2001). https://doi.org/10.1145/503209.503226

24.

Dokter, K., Jongmans, S., Arbab, F., Bliudze, S.: Combine and conquer: relating BIP and Reo. J. Log. Algebraic Methods Program. 86(1), 134–156 (2017). https://doi.org/10.1016/j.jlamp.2016.09.008MathSciNetCrossRef

25.

al Duhaiby, O., Groote, J.F.: Active learning of decomposable systems. In: Bae, K., Bianculli, D., Gnesi, S., Plat, N. (eds.) FormaliSE@ICSE 2020: 8th International Conference on Formal Methods in Software Engineering, Seoul, Republic of Korea, 13 July 2020, pp. 1–10. ACM (2020). https://doi.org/10.1145/3372020.3391560

26.

Ellis, C.A.: Team automata for groupware systems. In: Proceedings of the 1st International ACM SIGGROUP Conference on Supporting Group Work (GROUP), pp. 415–424. ACM (1997). https://doi.org/10.1145/266838.267363

27.

Farhat, S., Bliudze, S., Duchien, L., Kouchnarenko, O.: Toward run-time coordination of reconfiguration requests in cloud computing systems. In: Jongmans, S., Lopes, A. (eds.) Coordination Models and Languages - 25th IFIP WG 6.1 International Conference, COORDINATION 2023, Held as Part of the 18th International Federated Conference on Distributed Computing Techniques, DisCoTec 2023, Lisbon, Portugal, 19–23 June 2023, Proceedings. LNCS, vol. 13908, pp. 271–291. Springer, Cham (2023). https://doi.org/10.1007/978-3-031-35361-1_15

28.

Ghilezan, S., Jaksic, S., Pantovic, J., Scalas, A., Yoshida, N.: Precise subtyping for synchronous multiparty sessions. J. Log. Algebraic Methods Program. 104, 127–173 (2019). https://doi.org/10.1016/j.jlamp.2018.12.002MathSciNetCrossRef

29.

Jongmans, S.T.Q., Arbab, F.: Overview of thirty semantic formalisms for Reo. Sci. Ann. Comput. Sci. 22(1), 201–251 (2012). https://doi.org/10.7561/SACS.2012.1.201MathSciNetCrossRef

30.

Kokash, N., Krause, C., de Vink, E.P.: Reo + mCRL2: a framework for model-checking dataflow in service compositions. Formal Aspects Comput. 24(2), 187–216 (2012). https://doi.org/10.1007/s00165-011-0191-6MathSciNetCrossRef

31.

Lynch, N.A., Tuttle, M.R.: An introduction to Input/Output automata. CWI Q. 2(3), 219–246 (1989). https://ir.cwi.nl/pub/18164

32.

Muschevici, R., Proença, J., Clarke, D.: Feature Nets: behavioural modelling of software product lines. Softw. Sys. Model. 15(4), 1181–1206 (2016). https://doi.org/10.1007/s10270-015-0475-zCrossRef

33.

Orlando, S., Pasquale, V.D., Barbanera, F., Lanese, I., Tuosto, E.: Corinne, a tool for choreography automata. In: Salaün, G., Wijs, A. (eds.) Formal Aspects of Component Software - 17th International Conference, FACS 2021, Virtual Event, 28–29 October 2021, Proceedings. LNCS, vol. 13077, pp. 82–92. Springer, Cham (2021). https://doi.org/10.1007/978-3-030-90636-8_5

34.

Proença, J., Clarke, D.: Typed connector families. In: Braga, C., Ölveczky, P.C. (eds.) Formal Aspects of Component Software - 12th International Conference, FACS 2015, Niterói, Brazil, 14–16 October 2015, Revised Selected Papers. LNCS, vol. 9539, pp. 294–311. Springer, Cham (2015). https://doi.org/10.1007/978-3-319-28934-2_16

35.

Proença, J., Madeira, A.: Taming hierarchical connectors. In: Hojjat, H., Massink, M. (eds.) Fundamentals of Software Engineering - 8th International Conference, FSEN 2019, Tehran, Iran, 1–3 May 2019, Revised Selected Papers. LNCS, vol. 11761, pp. 186–193. Springer, Cham (2019). https://doi.org/10.1007/978-3-030-31517-7_13

36.

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-1863MathSciNetCrossRef

Title: Overview on Constrained Multiparty Synchronisation in Team Automata
Author: José Proença
Publisher: Springer Nature Switzerland
Book: Formal Aspects of Component Software
Print ISBN: 978-3-031-52182-9

Electronic ISBN: 978-3-031-52183-6

Copyright Year: 2024
DOI: https://doi.org/10.1007/978-3-031-52183-6_10

Springer Professional

Abstract

Please log in to get access to your license.

Dont have a licence yet? Then find out more about our products and how to get one now:

Springer Professional "Wirtschaft+Technik"

Springer Professional "Technik"

Springer Professional "Wirtschaft"

Premium Partner