Specification and refinement of finite dataflow networks — a relational approach

  • Manfred Broy
  • Ketil StØlen
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 863)


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.


Free Variable Feedback Operator Input Channel Output Stream Monotonicity Constraint 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    Abadi, M., Lamport, L.: The Existence of Refinement Mappings. Tech. Report 29, Digital, Palo Alto, (1988)Google Scholar
  2. 2.
    Brock, J. D., Ackermann, W. B.: Scenarios: A Model of Non-determinate Computation. Proc. Formalization of Programming Concepts, LNCS 107, (1981) 252–259Google Scholar
  3. 3.
    Broy, M.: Towards a Design Methodology for Distributed Systems. Proc. Constructive Methods in Computing Science, Springer, (1989) 311–364Google Scholar
  4. 4.
    Broy, M.: Functional Specification of Time Sensitive Communicating Systems. Proc. Programming and Mathematical Method, Springer, (1992) 325–367Google Scholar
  5. 5.
    Broy, M., Dederichs, F., Dendorfer, C., Fuchs, M., Gritzner, T. F., Weber, R.: The Design of Distributed Systems — An Introduction to Focus. Tech. Report SFB 342/2/92 A, TU München (1992)Google Scholar
  6. 6.
    Broy, M., StØlen, K.: Specification and Refinement of Finite Dataflow Networks — a Relational Approach. Tech. Report SFB 342/7/94 A, TU München (1994)Google Scholar
  7. 7.
    Keller, R. M.: Denotational Models for Parallel Programs with Indeterminate Operators. Proc. Formal Description of Programming Concepts, North-Holland, (1978) 337–366Google Scholar
  8. 8.
    Kleene, S. C.: Introduction to Metamathematics. (1952)Google Scholar
  9. 9.
    Park, D.: The “Fairness” Problem and Nondeterministic Computing Networks. Proc. 4th Foundations of Computer Science, Mathematical Centre Tracts 159, Mathematisch Centrum Amsterdam, (1983) 133–161Google Scholar
  10. 10.
    StØlen, K., Dederichs, F., Weber, R.: Assumption/Commitment Rules for Networks of Asynchronously Communicating Agents. Tech. Report SFB 342/2/93 A, TU München (1993)Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 1994

Authors and Affiliations

  • Manfred Broy
    • 1
  • Ketil StØlen
    • 1
  1. 1.Institut für InformatikTU MünchenMünchenGermany

Personalised recommendations