Assurance of Distributed Algorithms and Systems: Runtime Checking of Safety and Liveness

TL;DR

This paper introduces a comprehensive framework for specifying, implementing, and verifying distributed algorithms' safety and liveness properties using DistAlgo, combining high-level expressiveness with formal precision and executability.

Contribution

It provides a novel, executable specification framework for distributed algorithms that integrates high-level programming with formal safety and liveness property checking.

Findings

Complete executable specification of the checking framework

Example algorithm demonstrating safety and liveness properties

Integration of high-level language with formal verification

Abstract

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.