CoChat
Sign Up
Cited by 10

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·2020·Acta Informatica
DOI 10.1007/s00236-019-00359-1PMC PMC7056743
Open this paper in CoChat — free account

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.

The claims and statistics of this paper haven’t been checked yet.

Run the check — free, no account needed. It reads the open-access text and checks the sources it cites.

A few free checks a day · papers already verified open instantly · results are public

Integrity signals

Registry

Crossref · 10.1007/s00236-019-00359-1

Cites

Statistics

Claims the paper makes

The claims and statistics of this paper haven’t been checked yet.

Run the check — free, no account needed. It reads the open-access text and checks the sources it cites.

A few free checks a day · papers already verified open instantly · results are public

Claims other papers make about this one

Each is checked against this paper’s own text: does it say what the citing paper says it does?

  • Correct-by-construction program synthesis is an approach to software development that aims to produce programs guaranteed to be correct with respect to their specifications from the outset, rather than relying on traditional testing and debugging methods to identify and fix errors after the fact.

    “This is an approach to software development that aims to produce programs that are guaranteed to be correct with respect to their specifications from the outset, rather than relying on traditional testing and debugging methods to identify and fix errors after the fact.”

    From Towards Guaranteed Safe AI: A Framework for Ensuring Robust and Reliable AI Systems (2024) · cites this paper as Abate et al., 2020

Self-check

Percentages, sums and reported differences re-computed from the paper’s own numbers.

The self-check needs the paper’s full text.

Cites

No references could be resolved yet.

Research works printed but not linked: 49

  1. [1]Abate, A., Bessa, I., Cattaruzza, D., Chaves, L., Cordeiro, L.C., David, C., Kesseli, P., Kroening, D., Polgreen, E.: DSSynth: an automated digital controller synthesis tool for physical plants. In: International Conference on Automated Software Engineering (ASE), pp. 919–924. IEEE Computer Society (2017)
  2. [2]Abate, A., Bessa, I., Cattaruzza, D., Cordeiro, L.C., David, C., Kesseli, P., Kroening, D.: Sound and automated synthesis of digital stabilizing controllers for continuous plants. In: Hybrid Systems: Computation and Control (HSCC), pp. 197–206. ACM (2017)
  3. [3]Abate A Bessa I Cattaruzza D Cordeiro LC David C Kesseli P Kroening D Polgreen E Majumdar R Kunčak V Automated formal synthesis of digital controllers for state-space physical plants Computer Aided Verification (CAV) 2017 Cham Springer 462 482
  4. [4]Anta, A., Majumdar, R., Saha, I., Tabuada, P.: Automatic verification of control system implementations. In: International Conference on Embedded Software (EMSOFT), pp. 9–18. ACM (2010)
  5. [5]Astrom KJ Murray RM Feedback Systems: An Introduction for Scientists and Engineers 2008 Princeton Princeton University Press
  6. [7]Åström KJ Wittenmark B Computer-Controlled Systems: Theory and Design 1997 Upper Saddle River Prentice Hall
  7. [8]Belta C Yordanov B Gol EA Formal Methods for Discrete-Time Dynamical Systems 2016 Cham Springer
  8. [9]Bessa I Ismail H Palhares R Cordeiro LC Filho JEC Formal non-fragile stability verification of digital control systems with uncertainty IEEE Trans. Comput. 2017 66 3 545 552 10.1109/TC.2016.2601328 · DOI
  9. [10]Brain, M., Tinelli, C., Rümmer, P., Wahl, T.: An automatable formal semantics for IEEE-754 floating-point arithmetic. In: Symposium on Computer Arithmetic (ARITH), pp. 160–167. IEEE (2015)
  10. [11]Brönnimann H Melquiond G Pion S The design of the boost interval arithmetic library Theor. Comput. Sci. 2006 351 1 111 118 10.1016/j.tcs.2005.09.062 · DOI
  11. [12]Chaudhuri, S., Clochard, M., Solar-Lezama, A.: Bridging boolean and quantitative synthesis using smoothed proof search. In: POPL, pp. 207–220. ACM (2014)
  12. [13]Chen TC Chang CY Han KW Reduction of transfer functions by the stability-equation method J. Frankl. Inst. 1979 308 4 389 404 10.1016/0016-0032(79)90066-8 · DOI
  13. [14]Clarke EM Kroening D Lerda F Jensen K Podelski A A tool for checking ANSI-C programs Tools and Algorithms for the Construction and Analysis of Systems (TACAS) 2004 Berlin Springer 168 176
  14. [15]Darulova, E., Kuncak, V., Majumdar, R., Saha, I.: Synthesis of fixed-point programs. In: EMSOFT, pp. 22:1–22:10. IEEE (2013)
  15. [16]de Bessa IV Ismail H Cordeiro LC Filho JEC Verification of fixed-point digital controllers using direct and delta forms realizations Des. Autom. Embed. Syst. 2016 20 2 95 126 10.1007/s10617-016-9173-5 · DOI
  16. [17]Duggirala, P.S., Viswanathan, M.: Analyzing real time linear control systems using software verification. In: IEEE Real-Time Systems Symposium (RTSS), pp. 216–226 (2015)
  17. [18]Fadali S Visioli A Digital Control Engineering: Analysis and Design 2009 Amsterdam Elsevier
  18. [19]Fialho IJ Georgiou TT On stability and performance of sampled-data systems subject to wordlength constraint IEEE Trans. Autom. Control 1994 39 12 2476 2481 10.1109/9.362844 · DOI
  19. [20]Franklin G Powell D Emami-Naeini A Feedback Control of Dynamic Systems 2015 7 London Pearson
  20. [21]Gajic Z Lim M-T Skataric D Wu-Chung S Kecman V Optimal Control: Weakly Coupled Systems and Applications 2008 Boca Raton CRC Press
  21. [22]Horn RA Johnson C Matrix Analysis 1990 Cambridge Cambridge University Press
  22. [23]Jha, S., Gulwani, S., Seshia, S.A., Tiwari, A.: Oracle-guided component-based program synthesis. In: International Conference on Software Engineering (ICSE), vol. 1, pp. 215–224. ACM (2010)
  23. [24]Jha, S., Seshia, S.A.: SWATI: synthesizing wordlengths automatically using testing and induction. CoRR (2013). arxiv:1302.1920 · arXiv
  24. [25]Jha, S., Seshia, S.A., Tiwari, A.: Synthesis of optimal switching logic for hybrid systems. In: EMSOFT, pp. 107–116. ACM (2011)
  25. [26]Kokotovic PV Allemong JJ Winkelman JR Chow JH Singular perturbation and iterative separation of time scales Automatica 1980 16 1 23 33 10.1016/0005-1098(80)90083-7 · DOI
  26. [27]Kroening D Strichman O Zuck LD Attie PC Cortesi A Mukhopadhyay S Efficient computation of recurrence diameters Verification, Model Checking, and Abstract Interpretation (VMCAI) 2003 Berlin Springer 298 309
  27. [28]Kroening D Tautschnig M Ábrahám E Havelund K CBMC–C bounded model checker–(competition contribution) Tools and Algorithms for the Construction and Analysis of Systems 2014 Berlin Springer 389 391
  28. [29]Liberzon D Hybrid feedback stabilization of systems with quantized signals Automatica 2003 39 9 1543 1554 10.1016/S0005-1098(03)00151-1 · DOI · Paper page
  29. [30]Liu J Ozay N Finite abstractions with robustness margins for temporal logic-based control synthesis Nonlinear Anal. Hybrid Syst. 2016 22 1 15 10.1016/j.nahs.2016.02.002 · DOI
  30. [31]Luyben W External versus internal open-loop unstable processes Ind. Eng. Chem. Res. 1998 7 3 2713 2720 10.1021/ie9800400 · DOI
  31. [32]Mazo M Jr Davitian A Tabuada P Touili T Cook B Jackson P PESSOA: a tool for embedded controller synthesis Computer Aided Verification (CAV) 2010 Berlin Springer 566 569
  32. [33]Middleton RH Goodwin GC Digital Control and Estimation: A Unified Approach 1990 Upper Saddle River Prentice Hall
  33. [35]Oliveira VA Costa EF Vargas JB Digital implementation of a magnetic suspension control system for laboratory experiments IEEE Trans. Educ. 1999 42 4 315 322 10.1109/13.804538 · DOI
  34. [36]Oudjida AK Chaillet N Liacha A Berrandjia ML Hamerlain M Design of high-speed and low-power finite-word-length PID controllers Control Theory Technol. 2014 12 1 68 83 10.1007/s11768-014-2131-5 · DOI
  35. [37]Park J Pajic M Lee I Sokolsky O Scalable verification of linear controller software Tools and Algorithms for the Construction and Analysis of Systems (TACAS) 2016 Berlin Springer 662 679
  36. [38]Picasso, B., Bicchi, A.: Stabilization of LTI systems with quantized state-quantized input static feedback. In: International Workshop on Hybrid Systems: Computation and Control, pp. 405–416. Springer (2003)
  37. [39]Pramod S Chidambaram M Closed loop identification of transfer function model for unstable bioreactors for tuning PID controllers Bioprocess Eng. 2000 22 2 185 188 10.1007/s004499900077 · DOI
  38. [40]Ravanbakhsh, H., Sankaranarayanan, S.: Counter-example guided synthesis of control Lyapunov functions for switched systems. In: Conference on Decision and Control (CDC), pp. 4232–4239 (2015)
  39. [41]Ravanbakhsh, H., Sankaranarayanan, S.: Robust controller synthesis of switched systems using counterexample guided framework. In: International Conference on Embedded Software (EMSOFT), pp. 8:1–8:10. ACM (2016)
  40. [42]Roux, P., Jobredeaux, R., Garoche, P.-L.: Closed loop analysis of control command software. In: International Conference on Hybrid Systems: Computation and Control (HSCC), pp. 108–117. ACM (2015)
  41. [43]Solar-Lezama, A., Tancau, L., Bodík, R., Seshia, S.A, Saraswat, V.A.: Combinatorial sketching for finite programs. In: International Conference on Architectural Support for Programming Languages and Operating Systems (ASPLOS), pp. 404–415. ACM (2006)
  42. [44]Spong MW The swing up control problem for the Acrobot IEEE Control Syst. 1995 15 1 49 55 10.1109/37.341864 · DOI
  43. [45]Tabuada P Verification and Control of Hybrid Systems: A Symbolic Approach 2009 New York Springer
  44. [46]Tadeo F Lopez OP Alvarez T Control of neutralization processes by robust loop shaping IEEE Trans. Control Syst. Technol. 2000 8 2 236 246 10.1109/87.826795 · DOI
  45. [47]Tan, R.H.G., Hoo, L.Y.H.: DC–DC converter modeling and simulation using state space approach. In: Conference on Energy Conversion (CENCON), pp. 42–47. IEEE (2015)
  46. [48]Van Loan C Computing integrals involving the matrix exponential IEEE Trans. Autom. Control 1978 23 3 395 404 10.1109/TAC.1978.1101743 · DOI
  47. [49]Wang, T.E., Garoche, P.-L., Roux, P., Jobredeaux, R., Feron, E.: Formal analysis of robustness at model and code level. In: International Conference on Hybrid Systems: Computation and Control (HSCC), pp. 125–134. ACM (2016)
  48. [50]Wu J Li G Chen S Chu J Robust finite word length controller design Automatica 2009 45 12 2850 2856 10.1016/j.automatica.2009.09.001 · DOI
  49. [51]Zamani, M., Mazo, M., Abate, A.: Finite abstractions of networked control systems. In: Conference on Decision and Control (CDC), pp. 95–100. IEEE (2014)

Cited by

Sorted by citations

Authors
Abate, A., Bessa, I., Cordeiro, L., David, C., Kesseli, P., Kroening, D., & Polgreen, E.
ORCID
Venue
Acta Informatica
Publisher
Springer Science and Business Media LLC
Published
2019-12-06
Volume
57
Issue
1-2
Pages
223-244
ISSN
  • 0001-5903
  • 1432-0525
DOI
10.1007/s00236-019-00359-1
PMC
PMC7056743
Cited by
10
References
0
Language
en
Licence
Funders
  • Engineering and Physical Sciences Research Council (EP/J012564/1)
  • European Research Council (280053)
  • H2020 Future and Emerging Technologies (280053)

About these checks

Registry, retraction, Cites and statistics results are computed, not judged, with one exception: a printed reference that no index lists is read once by a model before it counts as a citation error. Claims are extracted by a model and kept only when their quote appears verbatim in the text; each cited source is then checked, with a model’s help, for whether it says what the claim relies on. Those verdicts can be wrong — read the claim’s quote and the cited source before relying on one.

Statistics and arithmetic are recomputed, not judged.

Confidence bands are shown only for fields calibrated on our annotated test set. None is calibrated yet, so no band is shown.

What counts as a claim ›How we measure confidence ›How we check this ›

Are you an author, or do you see a problem with this page? Request a review