Campus Event Calendar

Event Entry

New for: D3

What and Who

Formal Specification of Pastry Overlay Structure using TLA+

Tianxiang Lu
International Max Planck Research School for Computer Science - IMPRS
IMPRS Research Seminar
AG 1, AG 3, AG 4, AG 5, SWS, RG1, MMCI  
Public Audience

Date, Time and Location

Thursday, 29 April 2010
60 Minutes
E1 4


Domain specific formal verification is currently widely used in hardware designs. In the software world, in particular the scale of network and distributed systems, asynchronism raises the challenge of using formal verification to prove the correctness of a design or find a bug from it. Our verification domain is the P2P routing protocol. We starts with the currently widely used P2P routing protocol Pastry as an Example.

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.


Jennifer Gerling
--email hidden
passcode not visible
logged in users only

Jennifer Gerling, 04/28/2010 09:53 -- Created document.