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 of a service as a specification of that service. A multiple-server implementation is considered correct if it implements this single-server based specification.
We show how 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 the one implements the other.
Finally, a 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 provably correct multiple-server implementation is derived from the single server one. Different refinement mappings as well as different single-server based specifications result in different implementations. Examples illustrate the concepts and the methodology.
Cited By
- Felder M, Ghezzi C and Pezzè M Analyzing refinements of state based specifications Proceedings of the 1993 ACM SIGSOFT international symposium on Software testing and analysis, (28-39)
- Felder M, Ghezzi C and Pezzè M (1993). Analyzing refinements of state based specifications, ACM SIGSOFT Software Engineering Notes, 18:3, (28-39), Online publication date: 1-Jul-1993.
- Marzullo K and Wood M (1991). Making real-time reactive systems reliable, ACM SIGOPS Operating Systems Review, 25:1, (45-48), Online publication date: 2-Jan-1991.
- Marzullo K and Wood M Making real-time reactive systems reliable Proceedings of the 4th workshop on ACM SIGOPS European workshop, (1-4)
Index Terms
- Designing distributed services using refinement mappings
Recommendations
Designing Distributed Services with SDL
An approach to developing distributed services by automatically generating Java implementations from designs expressed using the specification and description language, SDL, is described below.Using a specification exemplar for a distributed meeting ...
Correct Architecture Refinement
Special issue on software architectureA method is presented for the stepwise refinement of an abstract architecture into a relatively correct lower level architecture that is intended to implement it. A refinement step involves the application of a predefined refinement pattern that ...