Reasoning about distributed reconfigurable systems

Proceedings of the ACM on Programming Languages, vol. 6, pp. 145–174

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.

Authors 4

1. Emma Ahrens Aachen

   RWTH Aachen University

   Affiliation as printed

   RWTH Aachen University, Aachen, Germany

2. Marius Dorel Bozga

   Institut polytechnique de Grenoble · Centre National de la Recherche Scientifique · Verimag · Université Grenoble Alpes

   Affiliation as printed

   Université Grenoble Alpes, France / CNRS, France / Grenoble INP, France / VERIMAG, France

3. Radu Iosif

   Institut polytechnique de Grenoble · Centre National de la Recherche Scientifique · Verimag · Université Grenoble Alpes

   Affiliation as printed

   Université Grenoble Alpes, France / CNRS, France / Grenoble INP, France / VERIMAG, France

4. Joost-Pieter Katoen Aachen

   RWTH Aachen University

   Affiliation as printed

   RWTH Aachen University, Aachen, Germany