Specification and Refinement of Finite Dataflow Networks - a Relational Approach

. 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. Specifications describe such sets by logical formulas. We emphasize the treatment of the well-known fair merge problem and the Brock/Ackermann anomaly. We give refinement rules which allow specifications to be decomposed modulo a feedback operator. 1 Introduction Dataflow components can be specified by formulas with a free variable ranging over domains of so-called stream processing functions [7], [5]. Both time independent and time dependent components can be described this way. In the latter case, the functions are timed in the sense that the input/output streams may have oc..