一句话：提出基于分离逻辑与归纳谓词的 Hoare 风格演算，用 havoc 不变式验证可重构分布式系统。
论文关注分布式系统中可重构程序的正确性推理。此类程序在组件按自身行为改变状态的同时，动态创建或删除组件及连接器。作者提出一种 Hoare 风格演算，借助类似分离逻辑的资源逻辑为重构动作给出局部规范，并用归纳定义谓词描述含无界数量组件的分布式系统。由于重构只影响部分结构，正确性还需处理未受影响的持续交互，作者引入 havoc 不变式，并以 assume/rely-guarantee 风格给出证明系统。最后，通过验证具有可重构（自调整）树架构的真实分布式系统，展示该方法的可行性。
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.
@article{paperbot1435,
title = {Reasoning about distributed reconfigurable systems},
author = {Emma Ahrens and Marius Bozga and Radu Iosif and Joost-Pieter Katoen},
journal = {Proceedings of the ACM on Programming Languages},
volume = {6},
number = {OOPSLA2},
year = {2022},
doi = {10.1145/3563293}
}