Document Type

Technical Report

Publication Date

1991-07-01

Filename

WUCS-91-43.pdf

DOI:

10.7936/K7BV7DZ4

Technical Report Number

WUCS-91-43

Abstract

Composition, superposition, and encapsulation are important techniques that work well together for designing large distributed software systems. Composition is a symmetric operator that allows system components to communicate with each other across module boundaries. Superposition is an asymmetric relationship that allows one system component to observe the state of another. Encapsulation is the ability to define the reason about the behavior of a module in terms of a well-defined boundary between that module and its environment, while hiding the internal operations of that module. In this paper, the I/O automation model of Lynch and Tuttle is extended to permit superposition of program modules. This results in a unified model that supports composition, superposition, and encapsulation. The extended model includes a formal specification mechanism for layered systems that allows the sets of correct behaviors of each layer to be expressed in terms of the states of the layers below it. To illustrate the ideas, we use the extended model to specify the global snapshot problem and prove the correctness of the global snapshot algorithm of Chandy and Lamport.

Comments

Permanent URL: http://dx.doi.org/10.7936/K7BV7DZ4

Download

Share

COinS