Skip to main content
Disciplines
Automotive Business IT + Informatics Construction + Real Estate Electrical Engineering + Electronics Energy + Sustainability Insurance + Risk Finance + Banking Management + Leadership Marketing + Sales Mechanical Engineering + Materials
Events
DE
EN
Books
Journals
Topic Page
Marketing
Start single access now
Access for companies
EXTENDED SEARCH
Log in
Top
Published in:
Safety Verification of Deep Neural Networks Read chapter Read first chapter

2017 | OriginalPaper | Chapter

Automated Formal Synthesis of Digital Controllers for State-Space Physical Plants

Authors : Alessandro Abate, Iury Bessa, Dario Cattaruzza, Lucas Cordeiro, Cristina David, Pascal Kesseli, Daniel Kroening, Elizabeth Polgreen

Published in: Computer Aided Verification

Publisher: Springer International Publishing

Log in

Activate our intelligent search to find suitable subject content or patents.

search-config
loading …

Abstract

We present a sound and automated approach to synthesize safe digital feedback controllers for physical plants represented as linear, time-invariant models. Models are given as dynamical equations with inputs, evolving over a continuous state space and accounting for errors due to the digitization of signals by the controller. Our counterexample guided inductive synthesis (CEGIS) approach has two phases: We synthesize a static feedback controller that stabilizes the system but that may not be safe for all initial conditions. Safety is then verified either via BMC or abstract acceleration; if the verification step fails, a counterexample is provided to the synthesis engine and the process iterates until a safe controller is obtained. We demonstrate the practical value of this approach by automatically synthesizing safe controllers for intricate physical plant models from the digital control literature.

Dont have a licence yet? Then find out more about our products and how to get one now:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

Mit Springer Professional "Wirtschaft+Technik" erhalten Sie Zugriff auf:

  • über 102.000 Bücher
  • über 537 Zeitschriften

aus folgenden Fachgebieten:

  • Automobil + Motoren
  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Elektrotechnik + Elektronik
  • Energie + Nachhaltigkeit
  • Finance + Banking
  • Management + Führung
  • Marketing + Vertrieb
  • Maschinenbau + Werkstoffe
  • Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

inform now

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

  • über 67.000 Bücher
  • über 390 Zeitschriften

aus folgenden Fachgebieten:

  • Automobil + Motoren
  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Elektrotechnik + Elektronik
  • Energie + Nachhaltigkeit
  • Maschinenbau + Werkstoffe




 

Jetzt Wissensvorsprung sichern!

inform now

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

  • über 67.000 Bücher
  • über 340 Zeitschriften

aus folgenden Fachgebieten:

  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Finance + Banking
  • Management + Führung
  • Marketing + Vertrieb
  • Versicherung + Risiko




Jetzt Wissensvorsprung sichern!

inform now
previous chapter DryVR: Data-Driven Verification and Compositional Reasoning for Automotive Systems
next chapter Classification and Coverage-Based Falsification for Embedded Control Systems
Appendix
Available only for authorised users
Footnotes
Literature
1.
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.
Anta, A., Majumdar, R., Saha, I., Tabuada, P.: Automatic verification of control system implementations. In: EMSOFT, pp. 9–18 (2010)
4.
Åström, K., Wittenmark, B.: Computer-Controlled Systems: Theory and Design. Prentice Hall Information and System Sciences Series. Prentice Hall, Upper Saddle River (1997)
5.
Bessa, I., Ismail, H., Palhares, R., Cordeiro, L., Filho, J.E.C.: Formal non-fragile stability verification of digital control systems with uncertainty. IEEE Trans. Comput. 66(3), 545–552 (2017)MathSciNetCrossRefMATH
6.
Brain, M., Tinelli, C., Rümmer, P., Wahl, T.: An automatable formal semantics for IEEE-754 floating-point arithmetic. In: ARITH, pp. 160–167. IEEE (2015)
7.
Cattaruzza, D., Abate, A., Schrammel, P., Kroening, D.: Unbounded-time analysis of guarded LTI systems with inputs by abstract acceleration. In: Blazy, S., Jensen, T. (eds.) SAS 2015. LNCS, vol. 9291, pp. 312–331. Springer, Heidelberg (2015). doi:10.​1007/​978-3-662-48288-9_​18 CrossRef
8.
David, C., Kroening, D., Lewis, M.: Using program synthesis for program analysis. In: Davis, M., Fehnker, A., McIver, A., Voronkov, A. (eds.) LPAR 2015. LNCS, vol. 9450, pp. 483–498. Springer, Heidelberg (2015). doi:10.​1007/​978-3-662-48899-7_​34 CrossRef
9.
de Bessa, I.V., Ismail, H., Cordeiro, L.C., Filho, J.E.C.: Verification of fixed-point digital controllers using direct and delta forms realizations. Des. Autom. Emb. Syst. 20(2), 95–126 (2016)CrossRef
10.
Duggirala, P.S., Viswanathan, M.: Analyzing real time linear control systems using software verification. In: IEEE Real-Time Systems Symposium, pp. 216–226, December 2015
11.
Fadali, S., Visioli, A.: Digital Control Engineering: Analysis and Design. Electronics & Electrical. Elsevier/Academic Press, Amsterdam/Cambridge (2009)
12.
Fialho, I.J., Georgiou, T.T.: On stability and performance of sampled-data systems subject to wordlength constraint. IEEE Trans. Autom. Control 39(12), 2476–2481 (1994)MathSciNetCrossRefMATH
13.
Franklin, G., Powell, D., Emami-Naeini, A.: Feedback Control of Dynamic Systems, 7th edn. Pearson, Upper Saddle River (2015)MATH
14.
15.
Horn, R.A., Johnson, C.: Matrix Analysis. Cambridge University Press, Cambridge (1990)
16.
Itzhaky, S., Gulwani, S., Immerman, N., Sagiv, M.: A simple inductive synthesis methodology and its applications. In: OOPSLA, pp. 36–46. ACM (2010)
17.
Kroening, D., Strichman, O.: Efficient computation of recurrence diameters. In: Zuck, L.D., Attie, P.C., Cortesi, A., Mukhopadhyay, S. (eds.) VMCAI 2003. LNCS, vol. 2575, pp. 298–309. Springer, Heidelberg (2003). doi:10.​1007/​3-540-36384-X_​24 CrossRef
18.
Li, G.: On pole and zero sensitivity of linear systems. IEEE Trans. Circuits Syst.-I: Fundam. Theory Appl. 44(7), 583–590 (1997)
19.
20.
Liu, J., Ozay, N.: Finite abstractions with robustness margins for temporal logic-based control synthesis. Nonlinear Anal.: Hybrid Syst. 22, 1–15 (2016)MathSciNetMATH
21.
Mazo, M., Davitian, A., Tabuada, P.: PESSOA: a tool for embedded controller synthesis. In: Touili, T., Cook, B., Jackson, P. (eds.) CAV 2010. LNCS, vol. 6174, pp. 566–569. Springer, Heidelberg (2010). doi:10.​1007/​978-3-642-14295-6_​49 CrossRef
22.
Moore, R.E.: Interval Analysis, vol. 4. Prentice-Hall, Englewood Cliffs (1966)
23.
Oliveira, V.A., Costa, E.F., Vargas, J.B.: Digital implementation of a magnetic suspension control system for laboratory experiments. IEEE Trans. Educ. 42(4), 315–322 (1999)CrossRef
24.
Oudjida, A.K., Chaillet, N., Liacha, A., Berrandjia, M.L., Hamerlain, M.: Design of high-speed and low-power finite-word-length PID controllers. Control Theory Technol. 12(1), 68–83 (2014)MathSciNetCrossRef
25.
Park, J., Pajic, M., Lee, I., Sokolsky, O.: Scalable verification of linear controller software. In: Chechik, M., Raskin, J.-F. (eds.) TACAS 2016. LNCS, vol. 9636, pp. 662–679. Springer, Heidelberg (2016). doi:10.​1007/​978-3-662-49674-9_​43 CrossRef
26.
Picasso, B., Bicchi, A.: Stabilization of LTI systems with quantized state - quantized input static feedback. In: Maler, O., Pnueli, A. (eds.) HSCC 2003. LNCS, vol. 2623, pp. 405–416. Springer, Heidelberg (2003). doi:10.​1007/​3-540-36580-X_​30 CrossRef
27.
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)
28.
Ravanbakhsh, H., Sankaranarayanan, S.: Robust controller synthesis of switched systems using counterexample guided framework. In: EMSOFT, pp. 8:1–8:10. ACM (2016)
29.
Roux, P., Jobredeaux, R., Garoche, P.: Closed loop analysis of control command software. In: HSCC, pp. 108–117. ACM (2015)
30.
Solar-Lezama, A., Tancau, L., Bodík, R., Seshia, S.A., Saraswat, V.A.: Combinatorial sketching for finite programs. In: ASPLOS, pp. 404–415. ACM (2006)
31.
Tan, R.H.G., Hoo, L.Y.H.: DC-DC converter modeling and simulation using state space approach. In: IEEE Conference on Energy Conversion, CENCON, pp. 42–47, October 2015
32.
Wang, T.E., Garoche, P., Roux, P., Jobredeaux, R., Feron, E.: Formal analysis of robustness at model and code level. In: HSCC, pp. 125–134. ACM (2016)
33.
34.
Zamani, M., Mazo, M., Abate, A.: Finite abstractions of networked control systems. In: IEEE CDC, pp. 95–100 (2014)
Metadata
Title
Automated Formal Synthesis of Digital Controllers for State-Space Physical Plants
Authors
Alessandro Abate
Iury Bessa
Dario Cattaruzza
Lucas Cordeiro
Cristina David
Pascal Kesseli
Daniel Kroening
Elizabeth Polgreen
Copyright Year
2017
Book
Computer Aided Verification

Print ISBN: 978-3-319-63386-2

Electronic ISBN: 978-3-319-63387-9

Copyright Year: 2017

DOI
https://doi.org/10.1007/978-3-319-63387-9_23

Premium Partner

    Image Credits