nach oben

Erschienen in:

2020 | OriginalPaper | Buchkapitel

Compositionality of Safe Communication in Systems of Team Automata

verfasst von : Maurice H. ter Beek, Rolf Hennicker, Jetty Kleijn

Erschienen in: Theoretical Aspects of Computing – ICTAC 2020

Verlag: Springer International Publishing

Einloggen

Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.

search-config

KI-gestützte Suche

Aus

Abstract

We study guarantees for safe communication in systems of systems composed of reactive components that communicate through synchronised execution of common actions. Systems are modelled as (extended) team automata, in which, in principle, any number of component automata can participate in the execution of a communicating action, either as a sender or as a receiver. We extend team automata with synchronisation type specifications, which determine specific synchronisation policies fine-tuned for particular application domains. On the other hand, synchronisation type specifications generate communication requirements for receptiveness and responsiveness. We propose a new, liberal version of requirement satisfaction which allows teams to execute arbitrary intermediate actions before being ready for the required communication, which is important in practice. Then we turn to the composition of systems and show that composition behaves well with respect to synchronisation type specifications. As a central result, we investigate criteria that ensure the preservation of local communication properties when (extended) team automata are composed. This is particularly challenging in the context of weak requirement satisfaction.

Sie haben noch keine Lizenz? Dann Informieren Sie sich jetzt über unsere Produkte:

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!

Jetzt informieren

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!

Jetzt informieren

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!

Jetzt informieren

Vorheriges Kapitel Formal Verification of Parallel Stream Compaction and Summed-Area Table Algorithms

Nächstes Kapitel Analysis of Bayesian Networks via Prob-Solvable Loops

In general, and in the classical team automata approach, a component automaton can also have a distinguished set of internal actions. Since internal actions are not really relevant for the scope of this paper, we omit them for the sake of simplicity.

If component automata were equipped with internal actions, then a syntactic composability constraint would have to be applied to \({\mathcal {S}}\) requiring that each internal action of a component automaton is unique to that component automaton.

We use a conjunction here since outputs are autonomously decided by components.

Otherwise the component has already a receptiveness requirement for an output.

We use a disjunction here since inputs rely on external choice.

Thus, (1) involves only responsiveness requirements concerning interface actions.

Attie, P., Baranov, E., Bliudze, S., Jaber, M., Sifakis, J.: A general framework for architecture composability. Formal Aspects Comput. 28(2), 207–231 (2015). https://doi.org/10.1007/s00165-015-0349-8MathSciNetCrossRefMATH

Bartoletti, M., Cimoli, T., Zunino, R.: Compliance in behavioural contracts: a brief survey. In: Bodei, C., Ferrari, G.-L., Priami, C. (eds.) Programming Languages with Applications to Biology and Security. LNCS, vol. 9465, pp. 103–121. Springer, Cham (2015). https://doi.org/10.1007/978-3-319-25527-9_9CrossRef

Basile, D., ter Beek, M.H., Legay, A.: Timed service contract automata. Innov. Syst. Softw. Eng. 16(2), 199–214 (2019). https://doi.org/10.1007/s11334-019-00353-3CrossRef

Basile, D., Degano, P., Ferrari, G.L.: Automata for specifying and orchestrating service contracts. Log. Methods Comput. Sci. 12(4:6), 1–51 (2016). https://doi.org/10.2168/LMCS-12(4:6)2016

Bauer, S.S., Mayer, P., Schroeder, A., Hennicker, R.: On weak modal compatibility, refinement, and the MIO workbench. In: Esparza, J., Majumdar, R. (eds.) TACAS 2010. LNCS, vol. 6015, pp. 175–189. Springer, Heidelberg (2010). https://doi.org/10.1007/978-3-642-12002-2_15CrossRefMATH

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: the case of masters and slaves. 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., Ellis, C.A., Kleijn, J., Rozenberg, G.: Synchronizations in team automata for groupware systems. Comput. Supp. Coop. Work 12(1), 21–69 (2003). https://doi.org/10.1023/A:1022407907596CrossRef

ter Beek, M.H., Hennicker, R., Kleijn, J.: Compositionality of safe communication in systems of team automata. Technical report, Zenodo, September 2020. https://doi.org/10.5281/zenodo.4050293

10.

ter Beek, M.H., Hennicker, R., Kleijn, J.: Team Automata@Work: on safe communication. In: Bliudze, S., Bocchi, L. (eds.) COORDINATION 2020. LNCS, vol. 12134, pp. 77–85. Springer, Cham (2020). https://doi.org/10.1007/978-3-030-50029-0_5CrossRef

11.

ter Beek, M.H., Kleijn, J.: Associativity of infinite synchronized shuffles and team automata. Fundam. Inform. 91(3–4), 437–461 (2009). https://doi.org/10.3233/FI-2009-0051MathSciNetCrossRefMATH

12.

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). https://doi.org/10.1007/978-3-540-31811-8_2CrossRef

13.

Brand, D., Zafiropulo, P.: On communicating finite-state machines. J. ACM 30(2), 323–342 (1983). https://doi.org/10.1145/322374.322380MathSciNetCrossRefMATH

14.

Brim, L., Cerná, I., Vareková, P., Zimmerova, B.: Component-interaction automata as a verification-oriented component-based system specification. ACM Softw. Eng. Notes 31(2) (2006). https://doi.org/10.1145/1118537.1123063

15.

Carmona, J., Cortadella, J.: Input/output compatibility of reactive systems. In: Aagaard, M.D., O’Leary, J.W. (eds.) FMCAD 2002. LNCS, vol. 2517, pp. 360–377. Springer, Heidelberg (2002). https://doi.org/10.1007/3-540-36126-X_22CrossRef

16.

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.006MathSciNetCrossRefMATH

17.

Carrez, C., Fantechi, A., Najm, E.: Behavioural contracts for a sound assembly of components. In: König, H., Heiner, M., Wolisz, A. (eds.) FORTE 2003. LNCS, vol. 2767, pp. 111–126. Springer, Heidelberg (2003). https://doi.org/10.1007/978-3-540-39979-7_8CrossRefMATH

18.

Castagna, G., Gesbert, N., Padovani, L.: A theory of contracts for web services. ACM Trans. Program. Lang. Syst. 31(5), 19:1–19:61 (2009). https://doi.org/10.1145/1538917.1538920

19.

David, A., Larsen, K.G., Legay, A., Nyman, U., Wąsowski, A.: Timed I/O automata: a complete specification theory for real-time systems. In: Proceedings of the 13th International Conference on Hybrid Systems: Computation and Control, HSCC 2010, pp. 91–100. ACM (2010). https://doi.org/10.1145/1755952.1755967

20.

de Alfaro, L., Henzinger, T.A.: Interface automata. In: Proceedings of the 8th European Software Engineering Conference Held Jointly with 9th ACM SIGSOFT International Symposium on Foundations of Software Engineering, ESEC/FSE 2001, pp. 109–120. ACM (2001). https://doi.org/10.1145/503209.503226

21.

de Alfaro, L., Henzinger, T.A.: Interface-based design. In: Broy, M., Grünbauer, J., Harel, D., Hoare, T. (eds.) Engineering Theories of Software Intensive Systems. NSS, vol. 195, pp. 83–104. Springer, Dordrecht (2005). https://doi.org/10.1007/1-4020-3532-2_3CrossRef

22.

Durán, F., Ouederni, M., Salaün, G.: A generic framework for \(n\)-protocol compatibility checking. Sci. Comput. Program. 77(7–8), 870–886 (2012). https://doi.org/10.1016/j.scico.2011.03.009CrossRefMATH

23.

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

24.

Engels, G., Groenewegen, L.: Towards team-automata-driven object-oriented collaborative work. In: Brauer, W., Ehrig, H., Karhumäki, J., Salomaa, A. (eds.) Formal and Natural Computing. LNCS, vol. 2300, pp. 257–276. Springer, Heidelberg (2002). https://doi.org/10.1007/3-540-45711-9_15CrossRef

25.

Hennicker, R., Bidoit, M.: Compatibility properties of synchronously and asynchronously communicating components. Log. Methods Comput. Sci. 14(1), 1–31 (2018). https://doi.org/10.23638/LMCS-14(1:1)2018

26.

Hennicker, R., Knapp, A.: Moving from interface theories to assembly theories. Acta Inf. 52(2–3), 235–268 (2015). https://doi.org/10.1007/s00236-015-0220-7

27.

Larsen, K.G., Nyman, U., Wąsowski, A.: Modal I/O automata for interface and product line theories. In: De Nicola, R. (ed.) ESOP 2007. LNCS, vol. 4421, pp. 64–79. Springer, Heidelberg (2007). https://doi.org/10.1007/978-3-540-71316-6_6CrossRefMATH

28.

Lüttgen, G., Vogler, W., Fendrich, S.: Richer interface automata with optimistic and pessimistic compatibility. Acta Inf. 52(4-5), 305–336 (2015). https://doi.org/10.1007/s00236-014-0211-0

29.

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

30.

Mavridou, A., Baranov, E., Bliudze, S., Sifakis, J.: Architecture diagrams: a graphical language for architecture style specification. EPTCS 223, 83–97 (2016). https://doi.org/10.4204/eptcs.223.6

31.

Winskel, G.: Synchronization trees. Theor. Comput. Sci. 34(1), 33–82 (1984). https://doi.org/10.1016/0304-3975(84)90112-9MathSciNetCrossRefMATH

Titel: Compositionality of Safe Communication in Systems of Team Automata
verfasst von: Maurice H. ter Beek
Rolf Hennicker
Jetty Kleijn
Verlag: Springer International Publishing
Buch: Theoretical Aspects of Computing – ICTAC 2020
Print ISBN: 978-3-030-64275-4

Electronic ISBN: 978-3-030-64276-1

Copyright-Jahr: 2020
DOI: https://doi.org/10.1007/978-3-030-64276-1_11

Springer Professional

Abstract

Bitte loggen Sie sich ein, um Zugang zu Ihrer Lizenz zu erhalten.

Sie haben noch keine Lizenz? Dann Informieren Sie sich jetzt über unsere Produkte:

Springer Professional "Wirtschaft+Technik"

Springer Professional "Technik"

Springer Professional "Wirtschaft"

Premium Partner