Petri net verification techniques on Synchronous Dataflow models

Dataflow process networks lead to different theoretical model approaches and have demonstrated their adequacy in data-dominated intensive systems, namely Synchronous Dataflow. The paper presents a set of translating mechanisms allowing the mapping from dataflow models (Synchrounous Dataflows) into Petri nets. Study on invariants focused on misbehaving dataflow, in which there is no static scheduling are delved to find out more hidden embedded features not normally addressed in dataflow analysis tools. This scheme allows one to make conclusion in Petri net domain to be applied in dataflow models to foresee the necessary amount of storage resources for each are, as well as to unveil the effective maximum number of tokens and the potential maximum number of tokens for each Synchronous Dataflow. Dataflow model translation into Petri net domain will give support to attain the required resource allocation under a reduced (minor) dataflow where a static scheduling list still exists. An application example will be used to illustrate the concept and effectiveness of the outlined approach. Our focus in this paper is centered in the description, model validation and at property verification in Petri net domain, namely Invariant and reachability analysis.