Transformational Design of an Asynchronous Distributor Component

The paper studies the systematic top-down design of an asynchronous distributor component that routes an incoming stream of messages to different output channels controlled by a stream of channel numbers. We refine the communication-oriented input/output behaviour into a state-based implementation exploiting two major transformations. The differentiation localizes the effect of single inputs with respect to previous input histories; the history abstraction extracts the component's state from the input histories. We present a uniform design for distributors of different outdegree using dependent types. Beyond the particular case study, we explicate generally applicable formal methods for the functional specification and systematic design of interactive components in asynchronous systems.