Modelling and Analyzing a Peer-to-peer Protocol
Chord is a distributed hash lookup primitive for building scalable and robust peer-to-peer systems. We have developed a small and compact Alloy model of the key elements of a Chord network. The analysis exposed some subtle issues in the specification of key intervals, which led to a bug in the code (written, unfortunately, before the analysis was performed). We are able to verify the correctness of the lookup routines with the updated specifications and are currently looking into checking other invariants mentioned in the Chord paper.
Members
- Daniel Jackson
- Hoe Teck Wee