Specification and refinement of finite dataflow networks — A relational approach

Manfred Broy; Ketil Stφlen

doi:10.1007/3-540-58468-4_169

Specification and refinement of finite dataflow networks — A relational approach

Manfred Broy, Ketil Stφlen

Informatics 4 - Chair of Software and Systems Engineering (2008 — 2022)

Technical University of Munich

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › peer-review

14 Scopus citations

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. 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.

Original language	English
Title of host publication	Formal Techniques in Real-Time and Fault-Tolerant Systems - 3rd International Symposium Organized Jointly with the Working Group Provably Correct Systems - ProCoS, Proceedings
Editors	Hans Langmaack, Willem-Paul de Roever, Jan Vytopil, Jan Vytopil
Publisher	Springer Verlag
Pages	247-267
Number of pages	21
ISBN (Print)	9783540584681
DOIs	https://doi.org/10.1007/3-540-58468-4_169
State	Published - 1994
Event	3rd International Symposium on Formal Techniques in Real Time and Fault Tolerance Organized Jointly with Working Group Provably Correct Systems, ProCoS 1994 - Lubeck, Germany Duration: 19 Sep 1994 → 23 Sep 1994

Publication series

Name	Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume	863 LNCS
ISSN (Print)	0302-9743
ISSN (Electronic)	1611-3349

Conference

Conference	3rd International Symposium on Formal Techniques in Real Time and Fault Tolerance Organized Jointly with Working Group Provably Correct Systems, ProCoS 1994
Country/Territory	Germany
City	Lubeck
Period	19/09/94 → 23/09/94

Access to Document

10.1007/3-540-58468-4_169

Cite this

Broy, M., & Stφlen, K. (1994). Specification and refinement of finite dataflow networks — A relational approach. In H. Langmaack, W.-P. de Roever, J. Vytopil, & J. Vytopil (Eds.), Formal Techniques in Real-Time and Fault-Tolerant Systems - 3rd International Symposium Organized Jointly with the Working Group Provably Correct Systems - ProCoS, Proceedings (pp. 247-267). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 863 LNCS). Springer Verlag. https://doi.org/10.1007/3-540-58468-4_169

Broy, Manfred ; Stφlen, Ketil. / Specification and refinement of finite dataflow networks — A relational approach. Formal Techniques in Real-Time and Fault-Tolerant Systems - 3rd International Symposium Organized Jointly with the Working Group Provably Correct Systems - ProCoS, Proceedings. editor / Hans Langmaack ; Willem-Paul de Roever ; Jan Vytopil ; Jan Vytopil. Springer Verlag, 1994. pp. 247-267 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)).

@inproceedings{7a01879cbbe24544a35369339d95d984,

title = "Specification and refinement of finite dataflow networks — A relational 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. 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.",

author = "Manfred Broy and Ketil Stφlen",

note = "Publisher Copyright: {\textcopyright} Springer-Verlag Berlin Heidelberg 1994.; 3rd International Symposium on Formal Techniques in Real Time and Fault Tolerance Organized Jointly with Working Group Provably Correct Systems, ProCoS 1994 ; Conference date: 19-09-1994 Through 23-09-1994",

year = "1994",

doi = "10.1007/3-540-58468-4_169",

language = "English",

isbn = "9783540584681",

series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",

publisher = "Springer Verlag",

pages = "247--267",

editor = "Hans Langmaack and {de Roever}, Willem-Paul and Jan Vytopil and Jan Vytopil",

booktitle = "Formal Techniques in Real-Time and Fault-Tolerant Systems - 3rd International Symposium Organized Jointly with the Working Group Provably Correct Systems - ProCoS, Proceedings",

}

Broy, M & Stφlen, K 1994, Specification and refinement of finite dataflow networks — A relational approach. in H Langmaack, W-P de Roever, J Vytopil & J Vytopil (eds), Formal Techniques in Real-Time and Fault-Tolerant Systems - 3rd International Symposium Organized Jointly with the Working Group Provably Correct Systems - ProCoS, Proceedings. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 863 LNCS, Springer Verlag, pp. 247-267, 3rd International Symposium on Formal Techniques in Real Time and Fault Tolerance Organized Jointly with Working Group Provably Correct Systems, ProCoS 1994, Lubeck, Germany, 19/09/94. https://doi.org/10.1007/3-540-58468-4_169

Specification and refinement of finite dataflow networks — A relational approach. / Broy, Manfred; Stφlen, Ketil.
Formal Techniques in Real-Time and Fault-Tolerant Systems - 3rd International Symposium Organized Jointly with the Working Group Provably Correct Systems - ProCoS, Proceedings. ed. / Hans Langmaack; Willem-Paul de Roever; Jan Vytopil; Jan Vytopil. Springer Verlag, 1994. p. 247-267 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 863 LNCS).

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › peer-review

TY - GEN

T1 - Specification and refinement of finite dataflow networks — A relational approach

AU - Broy, Manfred

AU - Stφlen, Ketil

N1 - Publisher Copyright: © Springer-Verlag Berlin Heidelberg 1994.

PY - 1994

Y1 - 1994

N2 - 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.

AB - 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.

UR - http://www.scopus.com/inward/record.url?scp=0042573622&partnerID=8YFLogxK

U2 - 10.1007/3-540-58468-4_169

DO - 10.1007/3-540-58468-4_169

M3 - Conference contribution

AN - SCOPUS:0042573622

SN - 9783540584681

T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

SP - 247

EP - 267

BT - Formal Techniques in Real-Time and Fault-Tolerant Systems - 3rd International Symposium Organized Jointly with the Working Group Provably Correct Systems - ProCoS, Proceedings

A2 - Langmaack, Hans

A2 - de Roever, Willem-Paul

A2 - Vytopil, Jan

PB - Springer Verlag

T2 - 3rd International Symposium on Formal Techniques in Real Time and Fault Tolerance Organized Jointly with Working Group Provably Correct Systems, ProCoS 1994

Y2 - 19 September 1994 through 23 September 1994

ER -

Broy M, Stφlen K. Specification and refinement of finite dataflow networks — A relational approach. In Langmaack H, de Roever WP, Vytopil J, Vytopil J, editors, Formal Techniques in Real-Time and Fault-Tolerant Systems - 3rd International Symposium Organized Jointly with the Working Group Provably Correct Systems - ProCoS, Proceedings. Springer Verlag. 1994. p. 247-267. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)). doi: 10.1007/3-540-58468-4_169

Specification and refinement of finite dataflow networks — A relational approach

Abstract

Publication series

Conference

Access to Document

Other files and links

Fingerprint

Cite this