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.
KeywordsFree Variable Feedback Operator Input Channel Output Stream Monotonicity Constraint
Unable to display preview. Download preview PDF.
- 1.Abadi, M., Lamport, L.: The Existence of Refinement Mappings. Tech. Report 29, Digital, Palo Alto, (1988)Google Scholar
- 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.Broy, M.: Towards a Design Methodology for Distributed Systems. Proc. Constructive Methods in Computing Science, Springer, (1989) 311–364Google Scholar
- 4.Broy, M.: Functional Specification of Time Sensitive Communicating Systems. Proc. Programming and Mathematical Method, Springer, (1992) 325–367Google Scholar
- 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.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.Keller, R. M.: Denotational Models for Parallel Programs with Indeterminate Operators. Proc. Formal Description of Programming Concepts, North-Holland, (1978) 337–366Google Scholar
- 8.Kleene, S. C.: Introduction to Metamathematics. (1952)Google Scholar
- 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.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