language: en

Refining Interactions in a Distributed System

Neelam Soundarajan
Computer and Information Science The Ohio State University
2015 Neil Avenue Columbus, OH 43210 USA
e-mail: neelam@cis.ohio-state.edu

Re?ning Interactions in a Distributed System

Abstract: We identify a type of re?nement called interaction re?nement that is useful in designing distributed systems. In a step of interaction re?nement, a system designer re?nes a ?hi gh-level? interaction into a sequence of ?low-level? interactions. In doing this, the designer is not re?ning the internal structure of the processes; rather he1 is implementing a high-level interaction between two (or more) processes in terms of a sequence of low-level communications between them. We motivate the idea of interaction re?nement with simple examples and develop a preliminary formalism that can be used to establish correctness of systems developed using interaction re?nement. We apply the formalism to validate some communication protocols.

Keywords: Interaction re?nement, Communication traces, Speci?cation and veri?cation, Communication protocols.

1 Introduction and Motivation