Automated formal synthesis of provably safe digital controllers for continuous plants
Authors
Publication Date
2019-12-06Journal Title
Acta Informatica
ISSN
0001-5903
Publisher
Springer Berlin Heidelberg
Volume
57
Issue
1-2
Pages
223-244
Language
en
Type
Article
This Version
VoR
Metadata
Show full item recordCitation
Abate, A., Bessa, I., Cordeiro, L., David, C., Kesseli, P., Kroening, D., & Polgreen, E. (2019). Automated formal synthesis of provably safe digital controllers for continuous plants. Acta Informatica, 57 (1-2), 223-244. https://doi.org/10.1007/s00236-019-00359-1
Abstract
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: 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.
Keywords
Original Article
Sponsorship
Engineering and Physical Sciences Research Council (EP/J012564/1)
European Research Council (280053)
H2020 Future and Emerging Technologies (280053)
Identifiers
s00236-019-00359-1, 359
External DOI: https://doi.org/10.1007/s00236-019-00359-1
This record's URL: https://www.repository.cam.ac.uk/handle/1810/314802
Rights
Attribution 4.0 International (CC BY 4.0)
Licence URL: https://creativecommons.org/licenses/by/4.0/
Statistics
Total file downloads (since January 2020). For more information on metrics see the
IRUS guide.