Formal Specification of a Dynamically Configurable Distributed System

The Programmers\u27 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\u27 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 runtime 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 describd 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