From Models to Implementations - Distributed Algorithms using Maude
Sam C Stephens · Illinois Digital Environment for Access to Learning and Scholarship (University of Illinois at Urbana-Champaign) · 2018
Maude is an equational and rewriting logic specification tool. It allows a unique and simple way of specifying concurrent programs and lends itself nicely to verification. This senior thesis focuses specifically on patterns for creating distributed algorithms in Maude, and after applying these patterns to several classical algorithms, it builds up to the consensus algorithm Raft, which has not previous been implemented. Maude has limited support for communication between processes on separate machines. This paper develops a “middleware” that enables a straightforward approach for transforming a model into an implementation, allowing correct-by-construction working implementations of distributed systems. The design and usage of this middleware will be examined, especially with the use of case studies. Ideally, this will allow easier development of future distributed systems in Maude, without having to worry about socket-level coding.