Verified Software

Authors

• Sergio Maffeis
• Philippa Gardner

Abstract

Abstract Peer-to-peer systems provide a simple and effective platform for data integration on the Internet, exchanging dynamic documents using Web services. Dynamic documents contain both data and references to external sources in the form of links, calls to Web services, or coordination scripts. XML standards and industrial platforms for Web services provide a technological basis for building such systems. Process algebras provide a formal framework for studying and understanding their formal properties. We have previously introduced Xdπ, a calculus for reasoning about dynamic Web data. It consists of locations, containing dynamic documents and π-like processes which communicate with each other, query and update these documents, and migrate to other peers to continue execution. Here, we study network equivalences for Xdπ and Core Xdπ, a reformulation of Xdπ which embeds the location structure in the processes. Using Core Xdπ, we study a process equivalence stipulating that two processes are equal if they have the same behaviour in equivalent networks. We also explore domain bisimilarity, which implies process equivalence and is easier to use in proofs. Our definition adapts a technique for reasoning about higher-order π-processes. In addition, it is sensitive to the set of locations present in the network, an approach we have not seen before. We use our process equivalence to study communication patterns used by servers in distributed query systems, and propose a new pattern involving mobile code.

Source Materials

• Authors' Preprint/Accepted Version
• Published Edition
• BibTeX Citation