Formal Specification and Implementation of Distributed Lazy Group Membership Protocol
摘要
In distributed systems, nodes typically collaborate to perform tasks. Many distributed systems adopt groups or clusters as architectural units to improve the management and coordination of nodes. The group membership protocol serves a crucial role in ensuring a consistent understanding of member status across all nodes in the group. Group membership protocols are essential in various distributed real-world systems, such as IoT sensor networks, smart agriculture, environmental monitoring, satellite communications, remote infrastructure monitoring, smart buildings, industrial automation, intelligent transportation systems, and medical monitoring systems. Group membership protocols are traditionally classified as heartbeat-based or gossip-based. Both protocol categories require frequent heartbeat or ping messages, facing challenges in energy efficiency, especially in systems with low failure rates and high energy consumption requirements. This paper introduces a novel group membership protocol with two main algorithms that eliminate the need for periodic ping or heartbeat messages. This protocol is designed for Symmetric P2P Systems using the actor model and ensures strong consistency. We provide formal specifications and verifications using TLA+ to ensure the correctness of our algorithms. The safety and liveness properties of the specifications are verified with the TLC model checker. In addition, the implementation of the protocol in the functional programming language is provided.