The proposed formal treatment of dataflow diagrams such as those used by DeMarco, Jackson, Ross (in SADT), and others is based on an extension to Petri nets. The authors maintain that such a formal treatment makes it easier to develop automated aids that support the use of dataflow diagrams. They show how the formalism can be used to check three consistency properties when a dataflow diagram is decomposed: global consistency, structural consistency, and behavioral consistency. A decomposition is globally consistent if it is constructed through a nonrecursive decomposition, that is, it has no cycles. A decomposition is structurally consistent if it has the same internal and external data flows as the original diagram. A decomposition is behaviorally consistent if its dynamic properties, as indicated by the Petri net notions of tokens and firings, are those of the original diagram. In order to develop the formalism, the authors extend Petri nets to allow for oring as well as anding on both the input and output sides.

These results might be useful, but they did not strike me as particularly deep or nonobvious. The example that the authors provide of a behaviorally inconsistent decomposition is also structurally inconsistent, raising the question of just when a structurally consistent decomposition might be behaviorally inconsistent. (A structurally inconsistent decomposition is necessarily behaviorally inconsistent.) The authors do not cite any examples of their formalism being used in practice. Also, the paper was submitted in 1986 and published in 1989, and the bibliographic citations (other than those of the authors’ own works) are mostly from 1982 or earlier.