Stream-Based Modelling of an Interactive Priority Queue

We present different models of an interactive priority queue in the setting of stream processing functions. The models describe particular abstraction levels relevant for the stepwise design of an implementation. The external view characterizes the input/output behaviour, the transition view captures the single computation steps, the internal view concentrates on the update of the internal state, and the trace view records the sequence of events during a run. The different models are systematically derived from the external view following sound transformation rules. The case study exemplifies general methods for the modelling and refinement of interactive components.