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

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.