Modeling dynamic reconfigurations in Reo using high-level replacement systems

Krause, C., Maraikar, Z., Lazovik, A. & Arbab, F., 1-Jan-2011, In : Science of computer programming. 76, 1, p. 23-36 14 p.

Research output: Contribution to journalArticleAcademicpeer-review

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. (C) 2009 Elsevier B.V. All rights reserved.

Original languageEnglish
Pages (from-to)23-36
Number of pages14
JournalScience of computer programming
Issue number1
Publication statusPublished - 1-Jan-2011


  • Dynamic reconfiguration, Graph transformation, Coordination, PETRI NETS, CONNECTORS, AUTOMATA, LOGIC

ID: 5213768