Formal Verification of Control Modules in Cyber-Physical Systems

Area of Science:

• Computer Science
• Control Engineering
• Cyber-Physical Systems

Background:

• State-based control modules are critical components in cyber-physical systems.
• Ensuring the correctness and consistency of these modules is challenging.
• Existing methods may lack seamless integration between specification, verification, and implementation.

Purpose of the Study:

• To propose a novel formal verification method for state-based control modules in cyber-physical systems.
• To bridge the gap between high-level specifications and hardware implementation.
• To enable early detection of errors in system design.

Main Methods:

• Formal verification using model checking.
• Specification using UML state machine diagrams converted to a rule-based logical model.
• Automatic transformation of the logical model into nuXmv for verification and VHDL for FPGA implementation.
• Case study on a manufacturing automation system.

Main Results:

• A consistent framework for formal verification and hardware implementation.
• Demonstrated early error detection capabilities.
• Successful application to a manufacturing automation system case study.

Conclusions:

• The proposed method effectively verifies state-based control modules for cyber-physical systems.
• The approach ensures consistency between formal specifications and hardware prototypes.
• It facilitates early error detection, improving system reliability and development efficiency.