Formal Model–Driven Design of Distributed Algorithms

We examine the use of formal model–driven development for creation and improvement of distributed algorithms. We use the integrated modeling and verification tool UPPAAL as our supporting tool. Instead of the traditional design, code and test-cycles known from agile paradigms, we employ formal model, verification and correction-cycles. The success of this approach is demonstrated on a distributed agreement algorithm from 1996 by Chandra and Toueg. We improve the number of communication rounds needed in the best-case from n to 2 where n is the number of agents. We end the paper with a correctness argument for systems with n agents. Formal model–driven development thus seems to be a fruitful approach for development of distributed algorithms.