Technical Report Number
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 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.
Sethuraman, Ram and Goldman, Kenneth J., "Formal Specification of a Dynamically Configurable Distributed System" Report Number: WUCS-95-17 (1995). All Computer Science and Engineering Research.