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

fYear

2011

fDate

16-18 June 2011

Firstpage

621

Lastpage

626

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;

fLanguage

English

Publisher

ieee

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

Type

conf

Filename

6015998