Spec i f i cat ion and Ref inement o f F in i te Data f low Networks-- a Re la t iona l Approach*

Abstract. We specify the black box behavior of dataflow components by characterizing the relation between their input and their output histories. We distinguish between three main classes of such specifications, namely time independent specifications, weakly time dependent specifications and strongly time dependent specifications. Dataflow components are semantically modeled by sets of timed stream processing functions. Spec-ifications describe such sets by logical formulas. We emphasize the treat-ment of the well-known fair merge problem and the Brock/Ackermann anomaly. We give refinement rules which allow specifications to be de-composed modulo a feedback operator.