DocumentCode :
2235202
Title :
State space generation for Petri nets-based GALS systems
Author :
Moutinho, Filipe ; Gomes, L.
Author_Institution :
Fac. de Cienc. e Tecnol., Univ. Nova de Lisboa, Lisbon, Portugal
fYear :
2012
fDate :
19-21 March 2012
Firstpage :
620
Lastpage :
625
Abstract :
This paper presents a tool that automatically generates state spaces of Globally-Asynchronous Locally-Synchronous (GALS) systems modeled through a non-autonomous Petri net class. The underlying class is the Input-Output Place-Transition Petri net (IOPT-nets) class extended with asynchronous channels and time domains. IOPT-nets benefits from an existing tool chain framework, which supports the development of automation and embedded systems, from the specification to implementation (through automatic code generation) in hardware and software platforms. The tool presented in this paper extends the existing tool chain framework, to support the verification of GALS systems. With the generated state space is possible to check the properties of each component of the GALS system and their interactions, allowing the verification of behavioral proprieties of the entire GALS system. The Petri net model of the GALS system is represented in PNML format and translated into a C program, assuring a good execution performance of the tool, even when handling large models (due to the compilation approach). The tool creates and saves the associated state space in an hierarchical XML file, which can be used to support its visualization and proprieties analysis through queries.
Keywords :
C language; Petri nets; XML; data analysis; data visualisation; embedded systems; formal verification; program compilers; query processing; C program; GALS system verification; PNML format; Petri nets-based GALS system; XML file; asynchronous channel; automatic code generation; automation system; compilation approach; embedded systems; formal specification; globally-asynchronous locally-synchronous; input-output place-transition Petri net; nonautonomous Petri net class; proprieties analysis; query; software platform; state-space generation; time domian; tool chain framework; visualization analysis; Bismuth; Fires; XML;
fLanguage :
English
Publisher :
ieee
Conference_Titel :
Industrial Technology (ICIT), 2012 IEEE International Conference on
Conference_Location :
Athens
Print_ISBN :
978-1-4673-0340-8
Type :
conf
DOI :
10.1109/ICIT.2012.6210007
Filename :
6210007
Link To Document :
بازگشت