Decomposition, validation and documentation of control process specification in form of a Petri net

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...

Full description

Saved in:
Bibliographic Details
Main Authors: Grobelna, Iwona, Wisniewska, Monika, Wisniewski, Remigiusz, Grobelny, Michal, Mroz, Piotr
Format: Conference Proceeding
Language:English
Subjects:
Concurrent computing
decomposition
Field programmable gate arrays
Formal verification
hypergraph
interpreted Petri net
Model checking
Petri nets
Process control
UML activity diagram
Unified modeling language
Online Access:Request full text
Tags: Add Tag
No Tags, Be the first to tag this record!
Description
Summary: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.
ISSN:2158-2246
DOI:10.1109/HSI.2014.6860481