From Models to Implementations - Distributed Algorithms using Maude

Stephens, Sam C

Permalink

https://hdl.handle.net/2142/100071 Copy

Description

Title

From Models to Implementations - Distributed Algorithms using Maude

Author(s)

Stephens, Sam C

Issue Date

2018-05

Keyword(s)

• Maude
• Distributed System
• Consensus Algorithm
• Raft
• Model-checking

Abstract

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.

Type of Resource

text

Language

en

Permalink

http://hdl.handle.net/2142/100071

Owning Collections