Repository logo
 

Automated Formal Synthesis of Digital Controllers for State-Space Physical Plants

Accepted version
Peer-reviewed

Type

Conference Object

Change log

Authors

Abate, Alessandro 
Bessa, Yuri 
Cattaruzza, Dario 
Cordeiro, Lucas 
David, Cristina 

Abstract

We present a sound and automated approach to synthesize safe digital feedback controllers for physical plants represented as linear, time-invariant models. Models are given as dynamical equations with inputs, evolving over a continuous state space and accounting for errors due to the digitization of signals by the controller. Our counterexample guided inductive synthesis (CEGIS) approach has two phases: We synthesize a static feedback controller that stabilizes the system but that may not be safe for all initial conditions. Safety is then verified either via BMC or abstract acceleration; if the verification step fails, a counterexample is provided to the synthesis engine and the process iterates until a safe controller is obtained. We demonstrate the practical value of this approach by automatically synthesizing safe controllers for intricate physical plant models from the digital control literature.

Description

Keywords

46 Information and Computing Sciences

Journal Title

CAV 2017: Computer Aided Verification

Conference Name

CAV 2017: International Conference on Computer Aided Verification

Journal ISSN

0302-9743
1611-3349

Volume Title

Publisher

Springer

Rights

All rights reserved