Correctness by Construction and Style Preserving Reconfigurations of Distributed Systems.

In distributed systems and dynamic environments, software architectures may evolve. A crucial issue when conducting system evolutions is to maintain the system in a consistent and functional state. Based on formal proofs in design-time, correctness by construction has recently emerged to efficiently guarantee system coherency. This article proposes a new method for the construction and specification of correct by construction system reconfigurations. Such transformations are characterized by graph rewriting rules that necessarily preserve the coherency of a system. We firstly propose operators on graph transformations and show that they conserve their correctness. Given a system specified by a graph grammar, these operators then serve to construct and characterize a set of correct transformations. We show in particular that any correct configuration can be reached starting from any other one without inconsistent intermediate step, using these transformations only