Formal Design of a Parameterized Synchronization Component for Asynchronous Communication Streams

The paper presents the top-down design of a synchronization component refining the communication- oriented input/output behaviour into a state-based implementation. The component constrains the flow of messages on two parallel communication channels to stay within a specified tolerance. The formal derivation uses transformations which are of general importance for the design of interactive components. The differentiation of the stream function localizes the effect of a single input with respect to previous input histories. The history abstraction extracts the component´s state from the input histories. The design safely bridges different views of the synchronization component ranging from the stream based specification to the state based implementation.