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

Resumo

Resumo

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.

palavras-chave

Palavras-chave

formal verificationdigital control systemsstate feedback controlstep responsesettling timemaximum overshootfinite word length effectsbounded model checkingsatisfiability modulo theoriescontroller fragility

links

Links e arquivos