WSEAS Transactions on Systems and Control
Print ISSN: 1991-8763, E-ISSN: 2224-2856
Volume 18, 2023
Formal Verification of Dynamical Control Systems (Addressing Integral Windup Phenomena Using Model-Checking)
Authors: , ,
Abstract: This paper investigates the utilization of model-checking as a potent method for verifying system designs, emphasizing its early error detection capabilities, reducing failures, increasing safety, and saving costs. The study explores the application of the UPPAAL tool and model-checking techniques within control systems. A case study in the paper concentrates on formally verifying Proportional Integral Derivative (PID) controllers, emphasizing integral windup issues. A model is constructed in UPPAAL for a control system that includes the system dynamics and the actuator limitations. The model’s accuracy is validated against the MATLAB/Simulink® model. Formal requirements addressing integral windup are formulated, and a practical model-checking example using UPPAAL illustrates its utility in control system verification.
Search Articles
Keywords: Model-based Verification, Formal Verification, Model-checking, UPPAAL, Safety-critical Systems, Control Systems Verification, Integral Windup, PID Controller
Pages: 393-400
DOI: 10.37394/23203.2023.18.41