关于Floodsub协议正确性的形式化化

Floodsub是一种简单、稳健且流行的点对点发布/订阅(pubsub)协议，节点可以随意离开或加入网络，订阅或取消订阅主题，并将新接收的消息转发给所有邻居(除发送者或起源节点之外)。为证明Floodsub的正确性，我们提出了其规范:Broadcastsub，在其中省略了网络连接和邻居订阅等实现细节。要证明Floodsub确实实现了Broadcastsub，就需要证明两个系统具有相关的无限计算。我们通过对状态及其后继进行局部推理来证明这一点，使用良根仿射(Well-Founded Simulation, WFS)。本文重点介绍了使用WFS证明Floodsub是Broadcastsub仿射细化的机械化证明。据我们所知，这是首个针对真实世界pubsub协议的机械化仿射细化验证。