×

zbMATH — the first resource for mathematics

Modeling dynamic reconfigurations in Reo using high-level replacement systems. (English) Zbl 1211.68052
Summary: Reo is a channel-based coordination language, wherein circuit-like connectors model and implement interaction protocols in heterogeneous environments that coordinate components or services. Connectors are constructed from primitive channels and can be reconfigured dynamically. Reconfigurations can even execute within a pending I/O transaction. In this article, we formally model and analyze dynamic reconfigurations and show how running coordinators can be reconfigured without the cooperation of their engaged components.
We utilize the theory of high-level replacement systems to model rule-based reconfigurations of connectors. This allows us to perform a complex reconfiguration as an atomic step and analyze it using formal verification techniques. Specifically, we formalize the structure of connectors as typed hypergraphs and use critical pair and state space analyses for verification of dynamic reconfigurations. We provide a full implementation of our approach in a framework that includes tools for the definition, analysis, and execution of reconfigurations, and is integrated with two execution engines for Reo. Our framework, moreover, integrates with the graph transformation tools AGG and GROOVE for formal analysis, as well as the Eclipse platform and standard web service technologies.

MSC:
68N15 Theory of programming languages
68Q60 Specification and verification (program logics, model checking, etc.)
Software:
AGG; GROOVE; Reo
PDF BibTeX XML Cite
Full Text: DOI
References:
[1] D. Gelernter, N. Carriero, S. Chandran, S. Chang, Parallel programming in linda, in: International Conference on Parallel Processing, ICPP, 1985, pp. 255–263
[2] Arbab, F.: Reo: A channel-based coordination model for component composition, Mathematical structures in computer science 14, 329-366 (2004) · Zbl 1085.68552
[3] Baier, C.; Sirjani, M.; Arbab, F.; Rutten, J.: Modeling component connectors in reo by constraint automata, Science of computer programming 61, No. 2, 75-113 (2006) · Zbl 1105.68058
[4] Ehrig, H.; Ehrig, K.; Prange, U.; Taentzer, G.: Fundamentals of algebraic graph transformation, EATCS monographs in theoretical computer science, (2006) · Zbl 1095.68047
[5] Ehrig, H.; Ehrig, K.; Prange, U.; Taentzer, G.: Fundamental theory for typed attributed graphs and graph transformation based on adhesive HLR categories, Fundamenta informaticae 74, No. 1, 31-61 (2006) · Zbl 1106.68055
[6] Koehler, C.; Arbab, F.; De Vink, E.: Reconfiguring distributed reo connectors, Lecture notes in computer science 5486, 221-235 (2009)
[7] Koehler, C.; Costa, D.; Proenca, J.; Arbab, F.: Reconfiguration of reo connectors triggered by dataflow, Electronic communications of the EASST 10 (2008)
[8] Clarke, D.: A basic logic for reasoning about connector reconfiguration, Fundamenta informaticae 82, No. 4, 361-390 (2008) · Zbl 1147.68570
[9] Clarke, D.; Costa, D.; Arbab, F.: Connector colouring I: Synchronisation and context dependency, Science of computer programming 66, No. 3, 205-225 (2007) · Zbl 1121.68015
[10] Bonsangue, M.; Clarke, D.; Silva, A.: Automata for context-dependent connectors, Lecture notes in computer science 5521, 184-203 (2009)
[11] Taentzer, G.: AGG: A graph transformation environment for modeling and validation of software, Lecture notes in computer science 3062, 446-453 (2004)
[12] Rensink, A.: The GROOVE simulator: A tool for state space generation, Lecture notes in computer science 3062, 479-485 (2004)
[13] Rensink, A.: Explicit state model checking for graph grammars, Lecture notes in computer science 5065, 114-132 (2008) · Zbl 1143.68462
[14] Eclipse coordination tools, http://reo.project.cwi.nl
[15] ReoLive coordination web service, http://reo.project.cwi.nl/live
[16] Klüppelholz, S.; Baier, C.: Symbolic model checking for channel-based component connectors, Electronic notes in theoretical computer science 175, No. 2, 19-37 (2007)
[17] Plump, D.: Hypergraph rewriting: critical pairs and undecidability of confluence, Term graph rewriting: theory and practice, 201-213 (1993)
[18] Heckel, R.; Küster, J. M.; Taentzer, G.: Confluence of typed attributed graph transformation systems, , 161-176 (2002) · Zbl 1028.68031
[19] Clarke, E. M.; Emerson, E. A.; Sistla, A. P.: Automatic verification of finite-state concurrent systems using temporal logic specifications, ACM transactions on programming languages and systems, TOPLAS 8, No. 2, 244-263 (1986) · Zbl 0591.68027
[20] Baldan, P.; Corradini, A.; Ehrig, H.; Heckel, R.: Compositional semantics for open Petri nets based on deterministic processes, Mathematical structures in computer science 15, 1-35 (2005) · Zbl 1089.68068
[21] P. Baldan, A. Corradini, H. Ehrig, R. Heckel, B. König, Bisimilarity and behaviour-preserving reconfigurations of open petri nets, CoRR abs/0809.4115, 2008. doi:10.2168/LMCS-4(4:3)2008 · Zbl 1161.68034
[22] Van Der Aalst, W. M. P.: The application of Petri nets to workflow management, Journal of circuits, systems, and computers 8, No. 1, 21-66 (1998)
[23] Van Der Aalst, W. M. P.: Exterminating the dynamic change bug: A concrete approach to support workflow change, Information systems frontiers 3, No. 3, 297-317 (2001)
[24] Bruni, R.; Lafuente, A. L.; Montanari, U.; Tuosto, E.: Style-based architectural reconfigurations, Bulletin of the EATCS 94, 160-181 (2008) · Zbl 1169.68306
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. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.