Petri Net Verification Techniques on Synchronous Dataflow Models

Research output: Chapter in Book/Report/Conference proceedingConference contributionpeer-review

6 Citations (Scopus)


Dataflow process networks lead to different theoretical model approaches and have demonstrated their adequacy in data-dominated intensive systems, namely Synchronous Dataflows. 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 arc, 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.
Original languageUnknown
Title of host publicationAnnual Conference of the IEEE Industrial Electronics Society
Pages3792 - 3797
Publication statusPublished - 1 Jan 2011
EventIECON’2011 - The 37th Annual Conference of the IEEE Industrial Electronics Society -
Duration: 1 Jan 2011 → …


ConferenceIECON’2011 - The 37th Annual Conference of the IEEE Industrial Electronics Society
Period1/01/11 → …

Cite this