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.
|Title of host publication||Computer Aided Verification|
|Subtitle of host publication||29th International Conference, CAV 2017, Heidelberg, Germany, July 24-28, 2017, Proceedings, Part I|
|Editors||Rupak Majumdar, Viktor Kunčak|
|Publication status||Published - 13 Jul 2017|
|Event||32nd IEEE/ACM International Conference on Automated Software Engineering - University of Illinois at Urbana-Champaign, Illinois, USA, Urbana-Champaign, Illinois, United States|
Duration: 30 Oct 2017 → 3 Nov 2017
Conference number: 32
|Name||Lecture Notes in Computer Science|
|Conference||32nd IEEE/ACM International Conference on Automated Software Engineering|
|Abbreviated title||ASE 2017|
|Period||30/10/17 → 3/11/17|
- Programming Languages
FingerprintDive into the research topics of 'Automated Formal Synthesis of Digital Controllers for State-Space Physical Plants'. Together they form a unique fingerprint.
Dr Cristina David
- Department of Computer Science - Senior Lecturer