Formal Design of a Slow-Down Component for Almost Synchronous Streams

The paper presents the systematic top-down design of a slown-down component that spreads an incoming stream of almost synchronous messages such that each two proper messages in the output stream are separated by at least one pause. We refine the communication-oriented input/output behaviour to a state-based implementation exploiting three important transformations. In the first design step, we approximate the component’s infinite behaviour by an input/ output synchronous finite behaviour. In the second design step, we differentiate the finite behaviour to localize the effect of single inputs with respect to previous input histories. In the third design step, we extract the component’s state from the input histories by a state abstraction function. Throughout the paper, we explicate a formal method how to implement a specified input/output behaviour by a state transition machine.