×

Combine and conquer: relating BIP and Reo. (English) Zbl 1353.68201

Summary: Coordination languages simplify design and development of concurrent systems. Particularly, exogenous coordination languages, like BIP and Reo, enable system designers to express the interactions among components in a system explicitly. A formal relation between exogenous coordination languages comprises the basis for a solid comparison and consolidation of their fundamental concepts. In this paper we establish a formal relation between BI(P) (i.e., BIP without the priority layer) and Reo, by defining transformations between their semantic models. We show that these transformations preserve all properties expressible in a common semantics. We use these transformations to define data-sensitive BIP architectures and their composition.

MSC:

68Q85 Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.)

Software:

mCRL2; Reo

References:

[1] Basu, A.; Bozga, M.; Sifakis, J., Modeling heterogeneous real-time components in BIP, (Proc. of SEFM (2006), ACM), 3-12
[2] Bliudze, S.; Sifakis, J., The algebra of connectors: structuring interaction in BIP, (Proc. of EMSOFT (2007), ACM), 11-20
[3] Arbab, F., Reo: a channel-based coordination model for component composition, Math. Struct. Comput. Sci., 14, 3, 329-366 (2004) · Zbl 1085.68552
[4] Arbab, F., Puff, the magic protocol, (Talcott Festschrift. Talcott Festschrift, Lecture Notes in Comput. Sci., vol. 7000 (2011), Springer), 169-206
[5] Papadopoulos, G. A.; Arbab, F., Configuration and dynamic reconfiguration of components using the coordination paradigm, Future Gener. Comput. Syst., 17, 8, 1023-1038 (2001) · Zbl 1032.68053
[6] BIP toolset (Apr 2016)
[7] Reo toolset (Apr 2016)
[8] Jongmans, S.-S. T.Q.; Arbab, F., Overview of thirty semantic formalisms for Reo, Sci. Ann. Comput. Sci., 22, 1, 201-251 (2012) · Zbl 1424.68105
[9] Attie, P.; Baranov, E.; Bliudze, S.; Jaber, M.; Sifakis, J., A general framework for architecture composability, (Proc. of SEFM. Proc. of SEFM, Lecture Notes in Comput. Sci., vol. 8702 (2014), Springer), 128-143
[10] Bliudze, S.; Sifakis, J.; Bozga, M.; Jaber, M., Architecture internalisation in BIP, (Proc. of CBSE (2014), ACM), 169-178
[11] Clarke, D.; Costa, D.; Arbab, F., Connector colouring I: synchronization and context dependency, Sci. Comput. Program., 66, 3, 205-225 (2007) · Zbl 1121.68015
[12] Jongmans, S.-S. T.Q.; Krause, C.; Arbab, F., Encoding context-sensitivity in Reo into non-context-sensitive semantic models, (Proc. of COORDINATION. Proc. of COORDINATION, Lecture Notes in Comput. Sci. (2011), Springer: Springer Berlin, Heidelberg), 31-48
[13] Dokter, K.; Jongmans, S.-S. T.Q.; Arbab, F.; Bliudze, S., Relating BIP and Reo, (Proc. of ICE. Proc. of ICE, Electron. Proc. Theor. Comput. Sci. (2015)), 3-20 · Zbl 1433.68093
[14] Baier, C.; Sirjani, M.; Arbab, F.; Rutten, J., Modeling component connectors in Reo by constraint automata, Sci. Comput. Program., 61, 2, 75-113 (2006) · Zbl 1105.68058
[15] Koehler, C.; Clarke, D., Decomposing port automata, (Proc. of SAC (2009), ACM), 1369-1373
[16] Baier, C.; Klein, J.; Klüppelholz, S., Synthesis of Reo connectors for strategies and controllers, Fundam. Inform., 130, 1, 1-20 (2014) · Zbl 1286.68067
[17] Milner, R., Communication and Concurrency, vol. 84 (1989), Prentice-Hall, Inc. · Zbl 0683.68008
[18] Gadducci, F.; Montanari, U., The tile model, (Proof, Language and Interaction (2000), The MIT Press), 133-166
[19] Arbab, F.; Bruni, R.; Clarke, D.; Lanese, I.; Montanari, U., Tiles for Reo, (Proc. of WADT. Proc. of WADT, Lecture Notes in Comput. Sci., vol. 5486 (2009), Springer: Springer Berlin, Heidelberg), 37-55 · Zbl 1253.68090
[20] Bruni, R.; Melgratti, H.; Montanari, U., Connector algebras, Petri Nets, and BIP, (Proc. of PSI. Proc. of PSI, Lecture Notes in Comput. Sci., vol. 7162 (2011), Springer), 19-38 · Zbl 1336.68006
[21] Krause, C., Integrated structure and semantics for Reo connectors and Petri nets, (Proc. of ICE. Proc. of ICE, Electron. Proc. Theor. Comput. Sci. (2009)), 57-69 · Zbl 1454.68077
[22] Papadopoulos, G. A.; Arbab, F., Coordination models and languages, Adv. Comput., 46, 329-400 (1998)
[23] Proença, J.; Clarke, D., Coordination models Orc and Reo compared, Electron. Notes Theor. Comput. Sci., 194, 4, 57-76 (2008) · Zbl 1277.68201
[24] Chkouri, M. Y.; Robert, A.; Bozga, M.; Sifakis, J., Translating AADL into BIP - application to the verification of real-time systems, (Proc. of MODELS. Proc. of MODELS, Lecture Notes in Comput. Sci., vol. 5421 (2009), Springer), 5-19
[25] Talcott, C.; Sirjani, M.; Ren, S., Comparing three coordination models: Reo, ARC, and PBRD, Sci. Comput. Program., 76, 1, 3-22 (2011) · Zbl 1211.68056
[26] Valiant, L. G., A bridging model for parallel computation, Commun. ACM, 33, 8, 103-111 (1990)
[27] Barros, T.; Ameur-Boulifa, R.; Cansado, A.; Henrio, L.; Madelaine, E., Behavioural models for distributed fractal components, Ann. Télécommun., 64, 1-2, 25-43 (2009)
[28] Winskel, G.; Nielsen, M., Models for concurrency, (Handbook of Logic in Computer Science, vol. 4 (1995), Oxford University Press), 1-148 · Zbl 0876.68001
[29] Bergstra, J. A.; Klop, J. W., Algebra of communicating processes with abstraction, Theor. Comput. Sci., 37, 77-121 (1985) · Zbl 0579.68016
[30] Kokash, N.; Krause, C.; de Vink, E. P., Reo + mcrl2: a framework for model-checking dataflow in service compositions, Form. Asp. Comput., 24, 2, 187-216 (2012) · Zbl 1259.68129
[31] Cranen, S.; Groote, J. F.; Keiren, J. J.A.; Stappers, F. P.M.; de Vink, E. P.; Wesselink, W.; Willemse, T. A.C., An overview of the mcrl2 toolset and its recent advances, (Proc. of TACAS. Proc. of TACAS, Lecture Notes in Comput. Sci. (2013), Springer), 199-213 · Zbl 1381.68198
[32] Jongmans, S.-S. T.Q., Automata-theoretic protocol programming (2016), Leiden University, Ph.D. thesis
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.