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

fYear

2014

fDate

16-18 June 2014

Firstpage

232

Lastpage

237

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;

fLanguage

English

Publisher

ieee

Conference_Titel

Human System Interactions (HSI), 2014 7th International Conference on

Conference_Location

Costa da Caparica

Type

conf

DOI

10.1109/HSI.2014.6860481

Filename

6860481