Transformational design of an interactive component straddling communication streams
Issue title: Selected papers from the International Conference on Computer Science, Software Engineering, Information Technology, e-Business, and Applications, 2004
Affiliations: Institute of Software Technology and Programming Languages, University of Lübeck, Ratzeburger Allee 160, D-23538 Lübeck, Germany. E-mail: dosch@isp.uni-luebeck.de
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: Interactive component, input/output behaviour, stream function, state transition machine, history abstraction, control state, data state, functional modeling, specification, transformation
