Analysing storage resources on Synchronous Dataflows using Petri net verification techniques

Dataflow process networks have proved and demonstrated their adequacy in data-dominated systems, namely Synchronous Dataflows. Due to a multitude of domains, in where each realizes a model of computation, many different theoretical dataflow model approaches emerged. This paper presents a set of translating mechanisms allowing the mapping from Synchrounous Dataflows into Petri nets. Study on invariants focused on synchronous dataflows is presented, allowing one to make conclusion in Petri net domain to be applied in dataflow models to foresee the necessary amount of storage resources for each arc, as well as to expose the effective maximum number of tokens and the potential maximum number of tokens for each Synchronous Dataflow. This translation allows also, one to take benefit of the well known property verification capabilities of Petri, as well as, attain conclusions about the flow of data that are not possible using the Synchronous Dataflows, or that use dynamic programming to compute a schedule that minimizes the amount of data memory required from among the schedules, where the amount of storage resource for each arc is still unpredictable. An application example based on multistage implementation of a sample rate system will be used to illustrate the concept and effectiveness of the proposed approach. Our focus in this paper is addressed to the description of the translating mechanisms, model validation and at property verification in Petri net domain, namely invariant and reachability analysis.