Published in Volume XXII, Issue 1, 2012, pages 201 - 251, doi: 10.7561/SACS.2012.1.201
Authors: S.-S. T.Q. Jongmans, F. Arbab
Abstract
Over the past decades, coordination languages have emerged for the specification and implementation of interaction protocols for communicating software components. This class of languages includes Reo, a platform for compositional construction of connectors. In recent years, many formalisms for describing the behavior of Reo connectors have emerged. In this paper, we give an overview of all these classes of semantic models. Furthermore, we investigate the expressiveness of two more prominent classes, constraint automata and coloring models, in detail.
Full Text (PDF)References
[1] Bernhard Aichernig, Farhad Arbab, Lacramioara Astefanoaei, Frank de Boer, Sun Meng, and Jan Rutten. Fault-Based Test Case Generation for Component Connectors. In Proceedings of TASE 2009, pages 147-154, 2009. http://dx.doi.org/10.1109/TASE.2009.14
[2] Rajeev Alur and David Dill. A theory of timed automata. TCS, 126(2):183-235, 1994. http://dx.doi.org/10.1016/0304-3975(94)90010-8
[3] Farhad Arbab. Coordination of Mobile Components. ENTCS, 54(1):1-16, 2001. http://dx.doi.org/10.1016/S1571-0661(04)00231-2
[4] Farhad Arbab. Abstract Behavior Types: A Foundation Model for Components and their Composition. In Frank de Boer, Marcello Bonsangue, Susanne Graf, and Willem-Paul de Roever, editors, Formal Methods for Components and Objects, volume 2852 of LNCS, pages 33-70. Springer, 2003. http://dx.doi.org/10.1007/978-3-540-39656-7_2
[5] Farhad Arbab. Reo: a channel-based coordination model for component composition. MSCS, 14(3):329-366, 2004. http://dx.doi.org/10.1017/S0960129504004153
[6] Farhad Arbab. Abstract Behavior Types: a foundation model for components and their composition. Sci. Comput. Program., 55(1-3):3-52, 2005. http://dx.doi.org/10.1016/j.scico.2004.05.010
[7] Farhad Arbab. Coordination for Component Composition. ENTCS, 160(1):15-40, 2006. http://dx.doi.org/10.1016/j.entcs.2006.05.013
[8] Farhad Arbab, Christel Baier, Frank de Boer, and Jan Rutten. Models and Temporal Logics for Timed Component Connectors. In Proceedings of SEFM 2004, pages 198-207, 2004. http://dx.doi.org/10.1109/SEFM.2004.10016
[9] Farhad Arbab, Christel Baier, Frank de Boer, and Jan Rutten. Models and temporal logical specifications for timed component connectors. SoSyM, 6(1):59-82, 2007. http://dx.doi.org/10.1007/s10270-006-0009-9
[10] Farhad Arbab, Christel Baier, Jan Rutten, and Marjan Sirjani. Modeling Component Connectors in Reo by Constraint Automata (Extended Abstract). ENTCS, 97(1):25-46, 2004. http://dx.doi.org/10.1016/j.entcs.2004.04.028
[11] Farhad Arbab, Roberto Bruni, Dave Clarke, Ivan Lanese, and Ugo Montanari. Tiles for Reo. In Andrea Corradini and Ugo Montanari, editors, Recent Trends in Algebraic Development Techniques, volume 5486 of LNCS, pages 37-55. Springer, 2009. http://dx.doi.org/10.1007/978-3-642-03429-9_4
[12] Farhad Arbab, Tom Chothia, Sun Meng, and Young-Joo Moon. Component Connectors with QoS Guarantees. In Amy Murphy and Jan Vitek, editors, Coordination Models and Languages, volume 4467 of LNCS, pages 286-304. Springer, 2007. http://dx.doi.org/10.1007/978-3-540-72794-1_16
[13] Farhad Arbab, Tom Chothia, Rob van der Mei, Sun Meng, Young-Joo Moon, and Chretien Verhoef. From Coordination to Stochastic Models of QoS. In John Field and Vasco Vasconcelos, editors, Coordination Models and Languages, volume 5521 of LNCS, pages 268-287. Springer, 2009. http://dx.doi.org/10.1007/978-3-642-02053-7_14
[14] Farhad Arbab and Jan Rutten. A Coinductive Calculus of Component Connectors. In Martin Wirsing, Dirk Pattinson, and Rolf Hennicker, editors, Recent Trends in Algebraic Development Techniques, volume 2755 of LNCS, pages 34-55. Springer, 2003. http://dx.doi.org/10.1007/978-3-540-40020-2_2
[15] Christel Baier. Probabilistic Models for Reo Connector Circuits. JUCS, 11(10):1718-1748, 2005. http://dx.doi.org/10.3217/jucs-011-10-1718
[16] Christel Baier, Tobias Blechmann, Joachim Klein, Sascha Kluppelholz, and Wolfgang Leister. Design and Verification of Systems with Exogenous Coordination Using Vereofy. In Tiziana Margaria and Bernhard Steffen, editors, Leveraging Applications of Formal Methods, Verification, and Validation, volume 6416 of LNCS, pages 97-111. Springer, 2010. http://dx.doi.org/10.1007/978-3-642-16561-0_15
[17] Christel Baier, Marjan Sirjani, Farhad Arbab, and Jan Rutten. Modeling component connectors in Reo by constraint automata. Sci. Comput. Program., 61(2):75-113, 2006. http://dx.doi.org/10.1016/j.scico.2005.10.008
[18] Christel Baier and Verena Wolf. Stochastic Reasoning About Channel-Based Component Connectors. In Paolo Ciancarini and Herbert Wiklicky, editors, Coordination Models and Languages, volume 4038 of LNCS, pages 1-15. Springer, 2006. http://dx.doi.org/10.1007/11767954_1
[19] Jan Bergstra and Jan Willem Klop. Process algebra for synchronous communication. IC, 60(1-3):109-137, 1984. http://dx.doi.org/10.1016/S0019-9958(84)80025-X
[20] Marcello Bonsangue, Dave Clarke, and Alexandra Silva. A model of context-dependent component connectors. Accepted for publication in Sci. Comput. Program. http://dx.doi.org/10.1016/j.scico.2011.01.006
[21] Marcello Bonsangue, Dave Clarke, and Alexandra Silva. Automata for Context-Dependent Connectors. In John Field and Vasco Vasconcelos, editors, Coordination Models and Languages, volume 5521 of LNCS, pages 184-203. Springer, 2009. http://dx.doi.org/10.1007/978-3-642-02053-7_10
[22] Roberto Bruni, Ivan Lanese, and Ugo Montanari. A basic algebra of stateless connectors. TCS, 366(1-2):95-120, 2006. http://dx.doi.org/10.1016/j.tcs.2006.07.005
[23] Roberto Bruni and Ugo Montanari. Zero-Safe Nets: Comparing the Collective and Individual Token Approaches. IC, 156(1-2):46-89, 2000. http://dx.doi.org/10.1006/inco.1999.2819
[24] Tom Chothia and Jetty Kleijn. Q-Automata: Modelling the Resource Usage of Concurrent Components. ENTCS, 175(2):153-167, 2007. http://dx.doi.org/10.1016/j.entcs.2007.03.009
[25] Dave Clarke. Reasoning About Connector Reconfiguration II: Basic Reconfiguration Logic. ENTCS, 159(1):61-77, 2006. http://dx.doi.org/10.1016/j.entcs.2005.12.062
[26] Dave Clarke. A Basic Logic for Reasoning about Connector Reconfiguration. Fundam. Inform., 82(4):361-390, 2008.
[27] Dave Clarke. Coordination: Reo, Nets, and Logic. In Frank de Boer, Marcello Bonsangue, Susanne Graf, and Willem-Paul de Roever, editors, Formal Methods for Components and Objects, volume 5382 of LNCS, pages 226-256. Springer, 2008. http://dx.doi.org/10.1007/978-3-540-92188-2_10
[28] Dave Clarke, David Costa, and Farhad Arbab. Connector Colouring I: Synchronisation and Context Dependency. ENTCS, 154(1):101-119, 2006. http://dx.doi.org/10.1016/j.entcs.2005.12.035
[29] Dave Clarke, David Costa, and Farhad Arbab. Connector colouring I: Synchronisation and context dependency. Sci. Comput. Program., 66(3):205-225, 2007. http://dx.doi.org/10.1016/j.scico.2007.01.009
[30] Dave Clarke and Jose Proenca. Coordination via Interaction Constraints I: Local Logic. EPTCS, 12(1):17-39, 2009. http://dx.doi.org/10.4204/EPTCS.12.2
[31] Dave Clarke, Jose Proenca, Alexander Lazovik, and Farhad Arbab. Deconstructing Reo. ENTCS, 229(2):43-58, 2009. http://dx.doi.org/10.1016/j.entcs.2009.06.028
[32] Dave Clarke, Jose Proenca, Alexander Lazovik, and Farhad Arbab. Channel-based coordination via constraint satisfaction. Sci. Comput. Program., 76(8):681-710, 2011. http://dx.doi.org/10.1016/j.scico.2010.05.004
[33] David Costa. Formal Models for Component Connectors. PhD thesis, Free University Amsterdam, 2010.
[34] Fabio Gadducci and Ugo Monanari. The tile model. In Gordon Plotkin, Colin Stirling, and Mads Tofte, editors, Proof, language, and interaction: essays in honour of Robin Milner, Foundations of Computing, pages 133-166. The MIT Press, 2000.
[35] Jan Friso Groote, Jeroen Keiren, Aad Mathijssen, Bas Ploeger, Frank Stappers, Carst Tankink, Yaroslav Usenko, Muck van Weerdenburg, WiegerWesselink, Tim Willemse, and Jeroen van der Wulp. The mCRL2 toolset. In Proceedings of WASDeTT 2008, 2008.
[36] Theo Haerder and Andreas Reuter. Principles of Transaction-Oriented Database Recovery. ACM CSUR, 15(4):287-317, 1983. http://dx.doi.org/10.1145/289.291
[37] Tony Hoare and He Jifeng. Unifying Theories of Programming. Prentice Hall, 1998.
[38] Mohammad Izadi and Marcello Bonsangue. Recasting Constraint Automata into Buchi Automata. In John Fitzgerald, Anne Haxthausen, and Husnu Yenigun, editors, Theoretical Aspects of Computing|ICTAC 2008, volume 5160 of LNCS, pages 156-170. Springer, 2008. http://dx.doi.org/10.1007/978-3-540-85762-4_11
[39] Mohammad Izadi, Marcello Bonsangue, and Dave Clarke. Modeling Component Connectors: Synchronisation and Context-Dependency. In Proceedings of SEFM 2008, pages 303-312, 2008. http://dx.doi.org/10.1109/SEFM.2008.24
[40] Mohammad Izadi, Marcello Bonsangue, and Dave Clarke. Buchi automata for modeling component connectors. Software and Systems Modeling, 10(2):183-200, 2011. http://dx.doi.org/10.1007/s10270-010-0152-1
[41] Sung-Shik Jongmans and Farhad Arbab. Correlating Semantic Models of Reo Connectors: Connector Coloring and Constraint Automata. EPTCS, 59(1):84-103, 2011. http://dx.doi.org/10.4204/EPTCS.59.8
[42] Sung-Shik Jongmans, Christian Krause, and Farhad Arbab. Encoding Context-Sensitivity in Reo into Non-Context-Sensitive Semantic Models. In Wolfgang de Meuter and Gruia-Catalin Roman, editors, Coordination Models and Languages, volume 6721 of LNCS, pages 31-48. Springer, 2011. http://dx.doi.org/10.1007/978-3-642-21464-6_3
[43] Ramtin Khosravi, Marjan Sirjani, Nesa Asoudeh, Shaghayegh Sahebi, and Hamed Iravanchi. Modeling and Analysis of Reo Connectors Using Alloy. In Doug Lea and Gianluigi Zavattaro, editors, Coordination Models and Languages, volume 5052 of LNCS, pages 169-183. Springer, 2008. http://dx.doi.org/10.1007/978-3-540-68265-3_11
[44] Sascha Kluppelholz and Christel Baier. Symbolic Model Checking for Channel-based Component Connectors. ENTCS, 175(2):19-37, 2007. http://dx.doi.org/10.1016/j.entcs.2007.03.003
[45] Christian Koehler and Dave Clarke. Decomposing Port Automata. In Proceedings of SAC 2009, pages 1369-1373, 2009. http://dx.doi.org/10.1145/1529282.1529587
[46] Natallia Kokash, Behnaz Changizi, and Farhad Arbab. A Semantic Model for Service Composition with Coordination Time Delays. In Jin Song Dong and Huibiao Zhu, editors, Formal Methods and Software Engineering, volume 6447 of LNCS, pages 106-121. Springer, 2010. http://dx.doi.org/10.1007/978-3-642-16901-4_9
[47] Natallia Kokash, Christian Krause, and Erik de Vink. Data-Aware Design and Verification of Service Compositions with Reo and mCRL2. In Proceedings of SAC 2010, pages 2406-2413, 2010. http://dx.doi.org/10.1145/1774088.1774590
[48] Natallia Kokash, Christian Krause, and Erik de Vink. Time and Data-Aware Analysis of Graphical Service Models in Reo. In Proceedings of SEFM 2010, pages 125-134, 2010. http://dx.doi.org/10.1109/SEFM.2010.26
[49] Natallia Kokash, Christian Krause, and Erik de Vink. Verification of Context-Dependent Channel-Based Service Models. In Frank de Boer, Marcello Bonsangue, Stefan Hallerstede, and Michael Leuschel, editors, Formal Methods for Components and Objects, volume 6286 of LNCS, pages 21-40. Springer, 2010. http://dx.doi.org/10.1007/978-3-642-17071-3_2
[50] Christian Krause. Integrated Structure and Semantics for Reo Connectors and Petri Nets. EPTCS, 12(1):57-69, 2009. http://dx.doi.org/10.4204/EPTCS.12.4
[51] Sun Meng and Farhad Arbab. On Resource-Sensitive Timed Component Connectors. In Marcello Bonsangue and Einar Broch Johnsen, editors, Formal Methods for Open Object-Based Distributed Systems, volume 4468 of LNCS, pages 301-316. Springer, 2007. http://dx.doi.org/10.1007/978-3-540-72952-5_19
[52] Sun Meng and Farhad Arbab. Connectors as Designs. ENTCS, 255(1):119-135, 2009. http://dx.doi.org/10.1016/j.entcs.2009.10.028
[53] Sun Meng and Farhad Arbab. QoS-Driven Service Selection and Composition Using Quantitative Constraint Automata. Fundam. Inform., 95(1):103-128, 2009. http://dx.doi.org/10.1109/SOSE.2010.51
[54] Sun Meng and Farhad Arbab. A Model for Web Service Coordination in Long-Running Transactions. In Proceedings of SOSE 2010, pages 121-128, 2010. http://dx.doi.org/10.1109/SOSE.2010.51
[55] Sun Meng, Farhad Arbab, Bernhard Aichernig, Lacramioara Astefanoaei, Frank de Boer, and Jan Rutten. Connectors as designs: Modeling, refinement and test case generation. Accepted for publication in Sci. Comput. Program. http://dx.doi.org/10.1016/j.scico.2011.04.002
[56] Young-Joo Moon, Alexandra Silva, Christian Krause, and Farhad Arbab. A compositional model to reason about end-to-end QoS in Stochastic Reo connectors. Accepted for publication in Sci. Comput. Program. http://dx.doi.org/10.1016/j.scico.2011.11.007
[57] Young-Joo Moon, Alexandra Silva, Christian Krause, and Farhad Arbab. A Compositional Semantics for Stochastic Reo Connectors. EPTCS, 30(1):93-107, 2010. http://dx.doi.org/10.4204/EPTCS.30.7
[58] Mohammed-Reza Mousavi, Marjan Sirjani, and Farhad Arbab. Formal Semantics and Analysis of Component Connectors in Reo. ENTCS, 154(1):83-99, 2006. http://dx.doi.org/10.1016/j.entcs.2005.12.034
[59] Gordon Plotkin. A Structural Approach to Operational Semantics. J. Log. Algebr. Program., 60-61:17-139, 2004. http://dx.doi.org/10.1016/j.jlap.2004.05.001
[60] Bahman Pourvatan, Marjan Sirjani, Hossein Hojjat, and Farhad Arbab. Automated Analysis of Reo Circuits using Symbolic Execution. ENTCS, 255(1):137-158, 2009. http://dx.doi.org/10.1016/j.entcs.2009.10.029
[61] Jose Proenca. Synchronous Coordination of Distributed Components. PhD thesis, Universiteit Leiden, 2011.
[62] Jan Rutten. Component Connectors. In Prakash Panangaden and Franck van Breugel, editors, Mathematical Techniques for Analyzing Concurrent and Probabilistic Systems, volume 23 of CRM, pages 73-87. AMS, 2004.
[63] Wolfgang Thomas. Automata on Infinite Objects. In Jan van Leeuwen, editor, Formal Models and Semantics, volume B of HTCS, pages 133-191. The MIT Press, 1990.
Bibtex
@article{sacscuza:q.2013ootsffr,
title={Overview of Thirty Semantic Formalisms for Reo},
author={S.-S. T.Q. Jongmans and F. Arbab},
journal={Scientific Annals of Computer Science},
volume={22},
number={1},
organization={``A.I. Cuza'' University, Iasi, Romania},
year={2013},
pages={201 -- 251},
doi={10.7561/SACS.2012.1.201},
publisher={``A.I. Cuza'' University Press}
}