Formal Specification of a Dynamically Configurable Distributed System

Ram Sethuraman

The Programmers' Playground} is a programming environment that supports end-user construction of distributed multimedia applications. The system implements a new programming model that is based, in part, upon ideas from the formal I/O automaton model of Lynch and Tuttle. Important features of The Programmers' Playground are a separation of communication and computation and graphical support for dynamic reconfiguration.

This paper provides a formal specification of the Playground programming model and run-time system in terms of the I/O automaton model on which it is based. Exploiting the compositionality properties of the I/O automaton model, the formal specification is described as a composition of several modules. A behavioral specification of each module is presented, followed by an I/O automaton that implements each specification. We present the specification in two stages, a centralized specification that captures the allowable behaviors, and then a detailed distributed implementation.

KEYWORDS: Dynamically configurable, distributed systems, I/O automata, formal specification

Technical report version is available as postscript (.ps) or compressed postscript (.ps.Z).

Washington University Department of Computer Science WUCS-95-17, November 1995.

Prepared by Ram Sethuraman (ram@cs.wustl.edu)

Washington University Department of Computer Science