A Basic Logic for Reasoning about Connector Reconfiguration

Issue title: Behavior of Composed Concurrent Systems: Logic and Reasoning

Article type: Research Article

Authors: Clarke, Dave

Affiliations: CWI, Kruislaan 413, NL-1098 SJ Amsterdam, The Netherlands. E-mail: dave@cwi.nl

Abstract: Software systems evolve over time. From a component-based software engineering perspective, this means that either the components of the system need to change, or, if components are connected using a coordination layer, then the way in which they are connected needs to change, or both. In some situations, changes must be performed without stopping the running system. This not only introduces a serious technological challenge, it also makes reasoning about the evolving system difficult. One approach to this problem is to use component connectors to plug components together. Reconfiguration of a system can then be reduced to reconfiguring the component connector, as changing component implementations can be implemented by changing which components the connector connects together. The coordination language Reo offers operations to dynamically reconfigure the topology of component connectors, but until now, no means for reasoning about reconfiguration in Reo has been developed. This issue is addressed in this paper. To enable reasoning about connector behaviour, and hence behaviour of the composed system, we present a semantics of Reo in the presence of reconfiguration, and a logic together with its model checking algorithm.

Keywords: Dynamic Reconfiguration, Coordination, Component Connectors, Reo

Journal: Fundamenta Informaticae, vol. 82, no. 4, pp. 361-390, 2008