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

Journal of control, automation and electrical systems

article

Cavalcante, Thiago¹  Bessa, Iury¹  Filho, Eddie²  Cordeiro, Lucas³ 

[1] Federal University of Amazonas;TP Vision;University of Manchester

关键词: Formal verification;    Digital control systems;    Finite word length;    Controller fragility;   

DOI  :  10.1007/s40313-020-00575-y

学科分类：自动化工程

来源: Springer

【 摘 要 】

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.

【 授权许可】

CC BY