Dataflow Model Property Verification Using Petri net Translation Techniques

Dataflow process networks lead to different theoretical model approaches and have demonstrated their adequacy in data-dominated intensive systems, namely Synchronous Dataflows. Since their appearance, dataflow models became too focused and specialized in their target applications. The paper presents a set of translating mechanisms allowing the mapping from dataflow models into Petri nets. This mapping allows taking advantage of Petri nets well-known properties verification capabilities and enriching dataflow models concerning scheduler information and resource allocation. This allows one to find out some hidden embedded features (model semantics and syntax) not normally addressed in dataflow analysis tools, which is briefly characterized. Dataflow model translation into Petri net domain give support to attain the required resource allocation under dataflow static scheduling list. 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 arc. An application example is used to illustrate the concept and effectiveness of the outlined approach.