Title :
Decomposition, validation and documentation of control process specification in form of a Petri net
Author :
Grobelna, Iwona ; Wisniewska, Monika ; Wisniewski, Rafael ; Grobelny, Michal ; Mroz, Piotr
Author_Institution :
Univ. of Zielona Gora, Zielona Gora, Poland
Abstract :
The article focuses on some aspects regarding logic controller design. Control process is formally specified using interpreted Petri nets. It is then formally verified against behavioral properties using model checking technique and temporal logic. Formal specification can also be documented as UML activity diagram. One can then benefit from advantages of both specification techniques - Petri nets with a wide range of mathematical support and user-friendly UML activity diagrams. An interpreted Petri net can also be decomposed into state machine components (SMCs), each of them to be implemented in a separate module of FPGA device.
Keywords :
Petri nets; Unified Modeling Language; field programmable gate arrays; finite state machines; formal specification; formal verification; programmable controllers; temporal logic; FPGA device; Petri net; SMC; UML activity diagram; behavioral properties; control process specification; documentation; formal specification; formal verification; logic controller design; model checking technique; state machine components; temporal logic; user-friendly UML activity diagrams; Concurrent computing; Field programmable gate arrays; Formal verification; Model checking; Petri nets; Process control; Unified modeling language; UML activity diagram; decomposition; hypergraph; interpreted Petri net; model checking;
Conference_Titel :
Human System Interactions (HSI), 2014 7th International Conference on
Conference_Location :
Costa da Caparica
DOI :
10.1109/HSI.2014.6860481
