State space generation algorithm for gals systems modeled by IOPT Petri nets

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

7 Citations (Scopus)


This paper proposes an algorithm to generate the state space of Globally-Asynchronous-Locally-Synchronous (GALS) systems specified with a non-autonomous class of Petri nets. The Input-Output Place-Transition (IOPT) Petri net class is targeted to model automation and embedded systems. It extends the Place-Transition net class with non-autonomous features. To allow GALS systems specification with the IOPT Petri net class, Asynchronous-Channels are used to represent GALS components communication. As GALS systems tend to have large state spaces, a compilation strategy is used in order to improve generation performance. The presented algorithm is implemented in a C program through XSL transformations from the PNML file containing the IOPT net models of the GALS systems, which is then used to generate the intended state space and to identify a set of properties. After the state space analysis, the VHDL code of GALS components is automatically generated from the IOPT net specification, and implemented in FPGA based platforms.
Original languageUnknown
Title of host publicationAnnual Conference on IEEE Industrial Electronics Society
Publication statusPublished - 1 Jan 2011
EventIECON 2011 - 37th Annual Conference on IEEE Industrial Electronics Society -
Duration: 1 Jan 2011 → …


ConferenceIECON 2011 - 37th Annual Conference on IEEE Industrial Electronics Society
Period1/01/11 → …

Cite this