Assurance of Distributed Algorithms and Systems: Runtime Checking of Safety and Liveness
This work addresses the challenge of ensuring correctness in distributed systems for developers and researchers, though it appears incremental as it builds upon existing languages and methods without claiming broad SOTA improvements.
The paper tackles the problem of verifying safety and liveness properties in distributed algorithms by introducing a framework that combines high-level pseudocode-like programming with executable specifications, using the DistAlgo language, and provides a complete example to demonstrate its applicability.
This paper presents a general framework and methods for complete programming and checking of distributed algorithms at a high-level, as in pseudocode languages, but precisely specified and directly executable, as in formal specification languages and practical programming languages, respectively. The checking framework, as well as the writing of distributed algorithms and specification of their safety and liveness properties, use DistAlgo, a high-level language for distributed algorithms. We give a complete executable specification of the checking framework, with a complete example algorithm and example safety and liveness properties.