Reasoning about Reconfigurations of Distributed Systems

TL;DR

This paper introduces a formal calculus using resource logic to reason about reconfiguration programs in distributed systems, enabling local specifications and correctness proofs for dynamic structural changes.

Contribution

It presents a Hoare-style calculus with inductive predicates and havoc invariants for verifying reconfiguration in distributed systems, including real-world examples.

Findings

Proof calculus effectively verifies reconfiguration correctness.

Applicable to systems with unbounded components.

Demonstrated on self-adjustable tree architectures.

Abstract

This paper presents a Hoare-style calculus for formal reasoning about reconfiguration programs of distributed systems. Such programs create and delete components and/or interactions (connectors) while the system components change state according to their internal behaviour. Our proof calculus uses a resource logic, in the spirit of Separation Logic, to give local specifications of reconfiguration actions. Moreover, distributed systems with an unbounded number of components are described using inductively defined predicates. The correctness of reconfiguration programs relies on havoc invariants, that are assertions about the ongoing interactions in a part of the system that is not affected by the structural change caused by the reconfiguration. We present a proof system for such invariants in an assume/rely-guarantee style. We illustrate the feasibility of our approach by proving the correctness of real-life distributed systems with reconfigurable (self-adjustable) tree architectures.