Automated Formal Synthesis of Provably Safe Digital Controllers for Continuous Plants

Research output: Contribution to journalArticle

  • External authors:
  • Alessandro Abate
  • Iury Bessa
  • Dario Cattaruzza
  • Cristina David
  • Pascal Kesseli
  • Daniel Kroening
  • Elizabeth Polgreen

Abstract

We present a sound and automated approach to synthesizing safe, digital controllers for physical plants represented as time-invariant models. Models are linear differential equations with inputs, evolving over a continuous state space. The synthesis precisely accounts for the effects of finite-precision arithmetic introduced by the controller. The approach uses counterexample-guided inductive synthesis (CEGIS): an inductive generalization phase produces a controller that is known to stabilize the model but that may not be safe for all initial conditions of the model. Safety is then verified via Bounded Model Checking: if the verification step fails, a counterexample is provided to the inductive generalization, and the process further iterates until a safe controller is obtained. We demonstrate the practical value of this approach by automatically synthesizing safe controllers for physical plant models from the digital control literature.

Bibliographical metadata

Original languageEnglish
JournalActa Informatica
Publication statusAccepted/In press - 18 Oct 2019