A compositional model for layered distributed systems

Abstract

Composition and layering are important mechanisms for constructing modular descriptions of distributed systems. Composition is a symmetric operator that allows system components to communicate with each other across module boundaries. Layering is an asymmetric relationship that allows one system component to observe the state of another.

Both composition and layering are useful in formal models of distributed systems. For example, Lynch and Tuttle define a composition operator for the I/O automaton model that has associated compositionality properties guaranteeing, for example, that when an execution of a composition is projected on each of its components, the result is a set of executions of the components. Such compositionality properties are important for constructing modular correctness proofs for distributed algorithms. Chandy and Misra define a layering mechanism, called superposition, for the UNITY programming model. They define superposition as a program transformation that adds a layer on top of a program such that all properties of the original program are preserved, again supporting modular correctness proofs.

It would seem desirable to mix the notions of composition and layering in formal descriptions of complex distributed systems. However, UNITY provides a superposition operator, but its union operator for combining programs lacks compositionality properties. And the I/O automaton model provides compositionality properties, but offers no support for constructing the kinds of layered systems we have described. In this paper, the I/O automaton model of Lynch and Tuttle is extended to permit superposition of program modules. This results in a unified model that supports both composition and layering. We show that our superposition operator does not affect the set of executions of the underlying module, thus preserving all properties of that module. The extended model also includes a formal specification mechanism for layered systems that allows the set of correct behaviors of the higher layer to be expressed in terms of the states of the lower layer.

This research was conducted at the Massachusetts Institute of Technology Laboratory for Computer Science and was supported in part by the National Science Foundation under Grant CCR-86-11442, by the Office of Naval Research under Contract N00014-85-K-0168, by the Defense Advanced Research Projects Agency (DARPA) under Contract N00014-83-K-0125.