Cargando…

Automated formal synthesis of provably safe digital controllers for continuous plants

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-preci...

Descripción completa

Detalles Bibliográficos
Autores principales: Abate, Alessandro, Bessa, Iury, Cordeiro, Lucas, David, Cristina, Kesseli, Pascal, Kroening, Daniel, Polgreen, Elizabeth
Formato: Online Artículo Texto
Lenguaje:English
Publicado: Springer Berlin Heidelberg 2019
Materias:
Acceso en línea:https://www.ncbi.nlm.nih.gov/pmc/articles/PMC7056743/
https://www.ncbi.nlm.nih.gov/pubmed/32189718
http://dx.doi.org/10.1007/s00236-019-00359-1
_version_ 1783503530629267456
author Abate, Alessandro
Bessa, Iury
Cordeiro, Lucas
David, Cristina
Kesseli, Pascal
Kroening, Daniel
Polgreen, Elizabeth
author_facet Abate, Alessandro
Bessa, Iury
Cordeiro, Lucas
David, Cristina
Kesseli, Pascal
Kroening, Daniel
Polgreen, Elizabeth
author_sort Abate, Alessandro
collection PubMed
description 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.
format Online
Article
Text
id pubmed-7056743
institution National Center for Biotechnology Information
language English
publishDate 2019
publisher Springer Berlin Heidelberg
record_format MEDLINE/PubMed
spelling pubmed-70567432020-03-16 Automated formal synthesis of provably safe digital controllers for continuous plants Abate, Alessandro Bessa, Iury Cordeiro, Lucas David, Cristina Kesseli, Pascal Kroening, Daniel Polgreen, Elizabeth Acta Inform Original Article 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. Springer Berlin Heidelberg 2019-12-06 2020 /pmc/articles/PMC7056743/ /pubmed/32189718 http://dx.doi.org/10.1007/s00236-019-00359-1 Text en © The Author(s) 2019 Open AccessThis article is licensed under a Creative Commons Attribution 4.0 International License, which permits use, sharing, adaptation, distribution and reproduction in any medium or format, as long as you give appropriate credit to the original author(s) and the source, provide a link to the Creative Commons licence, and indicate if changes were made. The images or other third party material in this article are included in the article’s Creative Commons licence, unless indicated otherwise in a credit line to the material. If material is not included in the article’s Creative Commons licence and your intended use is not permitted by statutory regulation or exceeds the permitted use, you will need to obtain permission directly from the copyright holder. To view a copy of this licence, visit http://creativecommons.org/licenses/by/4.0/.
spellingShingle Original Article
Abate, Alessandro
Bessa, Iury
Cordeiro, Lucas
David, Cristina
Kesseli, Pascal
Kroening, Daniel
Polgreen, Elizabeth
Automated formal synthesis of provably safe digital controllers for continuous plants
title Automated formal synthesis of provably safe digital controllers for continuous plants
title_full Automated formal synthesis of provably safe digital controllers for continuous plants
title_fullStr Automated formal synthesis of provably safe digital controllers for continuous plants
title_full_unstemmed Automated formal synthesis of provably safe digital controllers for continuous plants
title_short Automated formal synthesis of provably safe digital controllers for continuous plants
title_sort automated formal synthesis of provably safe digital controllers for continuous plants
topic Original Article
url https://www.ncbi.nlm.nih.gov/pmc/articles/PMC7056743/
https://www.ncbi.nlm.nih.gov/pubmed/32189718
http://dx.doi.org/10.1007/s00236-019-00359-1
work_keys_str_mv AT abatealessandro automatedformalsynthesisofprovablysafedigitalcontrollersforcontinuousplants
AT bessaiury automatedformalsynthesisofprovablysafedigitalcontrollersforcontinuousplants
AT cordeirolucas automatedformalsynthesisofprovablysafedigitalcontrollersforcontinuousplants
AT davidcristina automatedformalsynthesisofprovablysafedigitalcontrollersforcontinuousplants
AT kesselipascal automatedformalsynthesisofprovablysafedigitalcontrollersforcontinuousplants
AT kroeningdaniel automatedformalsynthesisofprovablysafedigitalcontrollersforcontinuousplants
AT polgreenelizabeth automatedformalsynthesisofprovablysafedigitalcontrollersforcontinuousplants