×

zbMATH — the first resource for mathematics

Automated formal synthesis of provably safe digital controllers for continuous plants. (English) Zbl 1441.93171
Summary: 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.
MSC:
93C62 Digital control/observation systems
93B50 Synthesis problems
93C15 Control/observation systems governed by ordinary differential equations
93D20 Asymptotic stability in control theory
PDF BibTeX XML Cite
Full Text: DOI
References:
[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] 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) · Zbl 1369.93189
[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), 462-482 (2017), Cham: Springer, Cham
[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] Astrom, Kj; Murray, Rm, Feedback Systems: An Introduction for Scientists and Engineers (2008), Princeton: Princeton University Press, Princeton
[6] Åström, Kj; Hägglund, T., Advanced PID Control (2006), Research Triangle Park: ISA-The Instrumentation, Systems, and Automation Society, Research Triangle Park
[7] Åström, Kj; Wittenmark, B., Computer-Controlled Systems: Theory and Design (1997), Upper Saddle River: Prentice Hall, Upper Saddle River
[8] Belta, C.; Yordanov, B.; Gol, Ea, Formal Methods for Discrete-Time Dynamical Systems (2016), Cham: Springer, Cham
[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., 66, 3, 545-552 (2017) · Zbl 1364.93447
[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)
[11] Brönnimann, H.; Melquiond, G.; Pion, S., The design of the boost interval arithmetic library, Theor. Comput. Sci., 351, 1, 111-118 (2006) · Zbl 1086.65046
[12] Chaudhuri, S., Clochard, M., Solar-Lezama, A.: Bridging boolean and quantitative synthesis using smoothed proof search. In: POPL, pp. 207-220. ACM (2014) · Zbl 1284.68169
[13] Chen, Tc; Chang, Cy; Han, Kw, Reduction of transfer functions by the stability-equation method, J. Frankl. Inst., 308, 4, 389-404 (1979) · Zbl 0429.93027
[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), 168-176 (2004), Berlin: Springer, Berlin · Zbl 1126.68470
[15] Darulova, E., Kuncak, V., Majumdar, R., Saha, I.: Synthesis of fixed-point programs. In: EMSOFT, pp. 22:1-22:10. IEEE (2013)
[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., 20, 2, 95-126 (2016)
[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)
[18] Fadali, S.; Visioli, A., Digital Control Engineering: Analysis and Design (2009), Amsterdam: Elsevier, Amsterdam
[19] Fialho, Ij; Georgiou, Tt, On stability and performance of sampled-data systems subject to wordlength constraint, IEEE Trans. Autom. Control, 39, 12, 2476-2481 (1994) · Zbl 0825.93437
[20] Franklin, G.; Powell, D.; Emami-Naeini, A., Feedback Control of Dynamic Systems (2015), London: Pearson, London
[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, Boca Raton
[22] Horn, Ra; Johnson, C., Matrix Analysis (1990), Cambridge: Cambridge University Press, Cambridge
[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)
[24] Jha, S., Seshia, S.A.: SWATI: synthesizing wordlengths automatically using testing and induction. CoRR (2013). arxiv:1302.1920
[25] Jha, S., Seshia, S.A., Tiwari, A.: Synthesis of optimal switching logic for hybrid systems. In: EMSOFT, pp. 107-116. ACM (2011)
[26] Kokotovic, Pv; Allemong, Jj; Winkelman, Jr; Chow, Jh, Singular perturbation and iterative separation of time scales, Automatica, 16, 1, 23-33 (1980) · Zbl 0427.93007
[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), 298-309 (2003), Berlin: Springer, Berlin
[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, 389-391 (2014), Berlin: Springer, Berlin
[29] Liberzon, D., Hybrid feedback stabilization of systems with quantized signals, Automatica, 39, 9, 1543-1554 (2003) · Zbl 1030.93042
[30] Liu, J.; Ozay, N., Finite abstractions with robustness margins for temporal logic-based control synthesis, Nonlinear Anal. Hybrid Syst., 22, 1-15 (2016) · Zbl 1344.93046
[31] Luyben, W., External versus internal open-loop unstable processes, Ind. Eng. Chem. Res., 7, 3, 2713-2720 (1998)
[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), 566-569 (2010), Berlin: Springer, Berlin
[33] Middleton, Rh; Goodwin, Gc, Digital Control and Estimation: A Unified Approach (1990), Upper Saddle River: Prentice Hall, Upper Saddle River
[34] Moore, Re, Interval Analysis (1966), Englewood Cliffs: Prentice-Hall, Englewood Cliffs
[35] Oliveira, Va; Costa, Ef; Vargas, Jb, Digital implementation of a magnetic suspension control system for laboratory experiments, IEEE Trans. Educ., 42, 4, 315-322 (1999)
[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., 12, 1, 68-83 (2014)
[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), 662-679 (2016), Berlin: Springer, Berlin
[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) · Zbl 1032.93023
[39] Pramod, S.; Chidambaram, M., Closed loop identification of transfer function model for unstable bioreactors for tuning PID controllers, Bioprocess Eng., 22, 2, 185-188 (2000)
[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)
[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)
[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) · Zbl 1364.93504
[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)
[44] Spong, Mw, The swing up control problem for the Acrobot, IEEE Control Syst., 15, 1, 49-55 (1995)
[45] Tabuada, P., Verification and Control of Hybrid Systems: A Symbolic Approach (2009), New York: Springer, New York · Zbl 1195.93001
[46] Tadeo, F.; Lopez, Op; Alvarez, T., Control of neutralization processes by robust loop shaping, IEEE Trans. Control Syst. Technol., 8, 2, 236-246 (2000)
[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)
[48] Van Loan, C., Computing integrals involving the matrix exponential, IEEE Trans. Autom. Control, 23, 3, 395-404 (1978) · Zbl 0387.65013
[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) · Zbl 1364.93249
[50] Wu, J.; Li, G.; Chen, S.; Chu, J., Robust finite word length controller design, Automatica, 45, 12, 2850-2856 (2009) · Zbl 1192.93039
[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)
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.