A Case Study in Specification and Verification in Spatial Logic: The Arrow Distributed Directory Protocol
The long term goal of this work is the development of high-level techniques and tools for semi automated proving of properties of distributed systems in spatial logic (Caires-Cardelli). In this setting, we have developed as a case study the specification and verification of a peer-2-peer distributed algorithm. <P>
The Arrow Distributed Directory Protocol of Demmer and Herlihy is a peer-2-peer distributed algorithm for directory lookup, such that the structure of the directory changes while the nodes transmit messages between them asking for a shared object. Our specification addresses both behavioural and structural aspects of the directory, for instance, to specify a node's behaviour, and the linked structure of the directory. Finally, we will also exemplify how the logic can be used to prove some safety properties essential for establishing the correctness of the protocol: the properties that the graph underlying the directory will never contain cycles, and that every path between two nodes is unique. <P>
This work is being developed in the context of the FET-Global Computing Profundis Project.
