Reasoning about connector reconfiguration II: Basic reconfiguration logic

摘要

Software systems evolve over time. To facilitate this, the coordination language Reo offers operations to dynamically reconfigure the topology of component connectors. We present a semantics for Reo in the presence of reconfiguration, and a logic, and its model checking algorithm, for reasoning about connector behaviour in this setting.