Formal verification of control modules in cyber-physical systems

9Citations
Citations of this article
24Readers
Mendeley users who have this article in their library.

Abstract

The paper proposes a novel formal verification method for a state-based control module of a cyber-physical system. The initial specification in the form of user-friendly UML state machine diagrams is written as an abstract rule-based logical model. The logical model is then used both for formal verification using the model checking technique and for prototype implementation in FPGA devices. The model is automatically transformed into a verifiable model in nuXmv format and into synthesizable code in VHDL language, which ensures that the resulting models are consistent with each other. It also allows the early detection of any errors related to the specification. A case study of a manufacturing automation system is presented to illustrate the approach.

Cite

CITATION STYLE

APA

Grobelna, I. (2020). Formal verification of control modules in cyber-physical systems. Sensors (Switzerland), 20(18), 1–23. https://doi.org/10.3390/s20185154

Register to see more suggestions

Mendeley helps you to discover research relevant for your work.

Already have an account?

Save time finding and organizing research with Mendeley

Sign up for free