Abate Alessandro, Bessa Iury, Cordeiro Lucas, David Cristina, Kesseli Pascal, Kroening Daniel, Polgreen Elizabeth
2Department of Computer Science, University of Oxford, Oxford, UK.
3Department of Electricity, Federal University of Amazonas, Manaus, Brazil.
Acta Inform. 2020;57(1):223-244. doi: 10.1007/s00236-019-00359-1. Epub 2019 Dec 6.
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.
我们提出了一种合理且自动化的方法，用于为表示为时不变模型的物理工厂合成安全的数字控制器。模型是带有输入的线性微分方程，在连续状态空间中演化。该合成精确地考虑了由控制器引入的有限精度算术的影响。该方法使用反例引导的归纳合成：归纳泛化阶段生成一个已知能稳定模型但可能对模型的所有初始条件都不安全的控制器。然后通过有界模型检查来验证安全性：如果验证步骤失败，则向归纳泛化提供一个反例，并且该过程进一步迭代，直到获得一个安全的控制器。我们通过从数字控制文献中自动为物理工厂模型合成安全控制器来证明这种方法的实际价值。
