Title :
Model checking of Control Interpreted Petri Nets
Author :
Grobelna, Iwona ; Adamski, Marian
Author_Institution :
Inst. of Comput. Eng. & Electron., Univ. of Zielona Gora, Gora, Poland
Abstract :
The paper presents an original approach to model checking of Control Interpreted Petri Nets. Petri Nets are currently used in the industry, but they are mostly verified only for structural properties. However, behavior properties are also of great importance. They can be verified using model checking technique. Model checking of specification allows to early detect subtle errors resulting from incorrect specification interpretation. Model description derived from Petri net is presented at RTL-level in such a way that it is easy to synthesize as reconfigurable logic controller or PLC as well as to formally verify for behavioral properties.
Keywords :
Petri nets; control engineering computing; formal specification; formal verification; programmable controllers; PLC; RTL-level; behavior property; control interpreted Petri nets; formal verification; incorrect specification interpretation; model checking technique; model description; reconfigurable logic controller; structural property; Formal verification; Industries; Integrated circuit modeling; Petri nets; Process control; Reconfigurable logic; Unified modeling language; Control Interpreted Petri Nets; formal verification; logic controller specification; model checking;
Conference_Titel :
Mixed Design of Integrated Circuits and Systems (MIXDES), 2011 Proceedings of the 18th International Conference
Conference_Location :
Gliwice
Print_ISBN :
978-1-4577-0304-1
