Thesis Topic Details

Topic ID:
3548
Title:
Leaderless Byzantine Paxos
Supervisor:
Kai Engelhardt
Research Area:
Distributed Systems, Algorithms
Associated Staff
Assessor:
Ron van der Meyden
Topic Details
Status:
Active
Type:
Research
Programs:
CS CE SE
Group Suitable:
No
Industrial:
No
Pre-requisites:
COMP3151
Description:
Agreement in distributed systems requires some form of synchrony. The potential for failures only aggravates the situation. Nevertheless, having distributed systems agree on anything is essential for making them work. Lamport's Paxos algorithms require a designated leader process. Lamport himself recognised this as a flaw and proposed a remedy in a 2-page abstract. This thesis is about verifying his claims. In more detail, one or more paxos algorithms need to modelled and relevant properties need to be expressed in some suitable formal language. Then, the actual verification can be undertaken in earnest.
Comments:
See for Lamport's sketch.
Past Student Reports
 
No Reports Available. Contact the supervisor for more information.

Check out all available reports in the CSE Thesis Report Library.

NOTE: only current CSE students can login to view and select reports to download.