Abstract
The paper presents the transformational design of a transmission component that straddles an incoming stream of messages such that each two proper messages in the output stream are separated by a specified number of pauses. We refine the communication-oriented input/output behaviour to a state-based implementation exploiting two major transformations. The first transformation refines the component's infinite behaviour to a finite behaviour by imposing a fixed input/output ratio. The second transformation implements the component's finite behaviour by a state transition machine. Here we extract the component's control state and data state from the input history by a history abstraction function. Throughout the paper, we explicate formal methods for the spefication and refinement of interactive components in the setting of stream functions. Altogether, we present a general methodology how to implement a specified infinite input/output behaviour of an interactive component by a state transition machine in a correctness preserving way.
Keywords
Get full access to this article
View all access options for this article.