Designing Distributed Services Using Refinement Mappings
Abstract
The thesis addresses the design of multiple-server implementations for services in distributed systems--a generalization of the replication management problem. A frequently used correctness criteria for replication management is that clients of a service not be able to distinguish a single- server implementation from one that involves multiple servers. Our approach formalizes this idea. It is based on viewing a single-server implementation is considered correct if it implements this single-server based specification. Program proof outlines can be viewed as specifications and, using refinement mappings, define what it means for one proof outline to implement another. The notion of a structural refinement, which formalizes the relationship between a program and the result of performing step-wise refinement, is defined. When one proof outline is a structural refinement of the other, simplified proof obligations can be used to show that one implements the other. The methodology for designing a multiple-server implementation of a service is presented. The methodology is based on structural refinement and on viewing proof outlines as specifications. A designer defines a refinement mapping to express the relationship between the state space of a given single-server implementation of a service and the state space of the desired multiple-server implementation. Using this refinement mapping, a provable correct multiple server implementation is derived from the single server one.
Document Details
- Document Type
- Technical Report
- Publication Date
- Sep 29, 1989
- Accession Number
- ADA213258
Entities
People
- Jacob I. Aizikowitz
Organizations
- Cornell University