Formal Non-fragile Verification of Step Response Requirements for Digital State-Feedback Control Systems

T Cavalcante, I Bessa, E Filho, Lucas Cordeiro

Research output: Contribution to journalArticlepeer-review

Abstract

We describe and evaluate a novel approach to formally verify whether a digital control system meets specifications related to step-response parameters. In particular, we obtain a state feedback controller designed for a system represented by a state-space model. Then we analyze whether its required specifications regarding settling time and maximum overshoot are met, using both open- and closed-loop forms and considering finite word-length (FWL) effects for the latter. We developed our verification approaches inside DSVerifier, which is a verification tool that employs bounded (and unbounded) model checking based on satisfiability modulo theories. Thus, DSVerifier checks performance requirements of digital control systems considering fragility, such as round-off and numerical quantization errors. Our approaches were also evaluated over a set of standard control-system benchmarks extracted from the control literature. Experimental results show that DSVerifier can check settling-time and overshoot in control systems suffering from FWL effects, while other existing approaches routinely ignore those issues.
Original languageEnglish
JournalJournal of Control, Automation and Electrical Systems
Publication statusAccepted/In press - 27 Jan 2020

Fingerprint

Dive into the research topics of 'Formal Non-fragile Verification of Step Response Requirements for Digital State-Feedback Control Systems'. Together they form a unique fingerprint.

Cite this