Formal Specification of Pastry Overlay Structure using TLA+

Pastry is one of the structured peer-to-peer overlay networks, which provide a substrate for building distributed applications. They map object keys (identifier for a piece of distributed application, e.g. SUSE image for downloading) to overlay nodes (e.g., the computer connected to the Internet) and offers a lookup primitive to send a message to the node responsible for a key. Overlay nodes maintain some routing state (e.g. routing table and information of their neighbors) to route messages towards the nodes responsible for their destination keys [2].

In order to specify the algorithm and meanwhile to run a model checker to help us get correct and complete formal description of the systembehavior, we have to choose a suitable specification languages at the first place to start. TLA+[5] is a high-level specification language that has been used to specify and check the correctness of several hardware protocols and it is stated that it can also be used to specify and check concurrent algorithms and protocols for software systems [6].

In our approach, we've used TLA+ to specify Pastry routing algorithm formally and used the model checker TLC to check the specification with some artificially made-up extreme cases. Due to the laps between the description given in the publications we are aware of ([2], [3], [7], [1], [4]) and a formal specification, we have made some assumption. In this talk we are going to show our formal specification and we also want to point out some difficulties we met up with during specifying the system.