Abstract
Among the various critical systems that are worth to be formally analyzed, a wide set consists of controllers for dynamical systems. Those programs typically execute an infinite loop in which simple computations update internal states and produce commands to update the system state. Those systems are yet hardly analyzable by available static analysis method, since, even if performing mainly linear computations, the computation of a safe set of reachable states often requires quadratic invariants.
In this paper we consider the general setting of a piecewise affine program; that is a program performing different affine updates on the system depending on some conditions. This typically encompasses linear controllers with saturations or controllers with different behaviors and performances activated on some safety conditions.
Our analysis is inspired by works performed a decade ago by Johansson et al, and Morari et al, in the control community. We adapted their method focused on the analysis of stability in continuous-time or discretetime settings to fit the static analysis paradigm and the computation of invariants, that is over-approximation of reachable sets using piecewise quadratic Lyapunov functions.
This work has been partially supported by an RTRA/STAE BRIEFCASE project grant, the ANR projects INS-2012-007 CAFEIN, and ASTRID VORACE.
Access provided by Autonomous University of Puebla. Download to read the full chapter text
Chapter PDF
Similar content being viewed by others
Keywords
References
Allamigeon, X.: Static analysis of memory manipulations by abstract interpretation — Algorithmics of tropical polyhedra, and application to abstract interpretation. PhD thesis, École Polytechnique, Palaiseau, France (November 2009)
Blondel, V., Bournez, O., Koiran, P., Papadimitriou, C., Tsitsiklis, J.: Deciding stability and mortality of piecewise affine dynamical systems. Theoretical Computer Science A 1–2(255), 687–696 (2001)
Bertrane, J., Cousot, P., Cousot, R., Feret, J., Mauborgne, L., Miné, A., Rival, X.: Static analysis by abstract interpretation of embedded critical software. ACM SIGSOFT Software Engineering Notes 36(1), 1–8 (2011)
Biswas, P., Grieder, P., Löfberg, J., Morari, M.: A Survey on Stability Analysis of Discrete-Time Piecewise Affine Systems. In: IFAC World Congress, Prague, Czech Republic (July 2005)
Cousot, P., Cousot, R.: Abstract interpretation: A unified lattice model for static analysis of programs by construction or approximation of fixpoints. In: Conference Record of the Fourth Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, Los Angeles, California, pp. 238–252. ACM Press, New York (1977)
Cousot, P., Halbwachs, N.: Automatic discovery of linear restraints among variables of a program. In: Aho, A., Zilles, S., Szymanski, T. (eds.) POPL, pp. 84–96. ACM Press (1978)
Colón, M.A., Sankaranarayanan, S.: Generalizing the template polyhedral domain. In: Barthe, G. (ed.) ESOP 2011. LNCS, vol. 6602, pp. 176–195. Springer, Heidelberg (2011)
Colón, M.A., Sankaranarayanan, S., Sipma, H.B.: Linear invariant generation using non-linear constraint solving. In: Hunt Jr., W.A., Somenzi, F. (eds.) CAV 2003. LNCS, vol. 2725, pp. 420–432. Springer, Heidelberg (2003)
Feret, J.: Static analysis of digital filters. In: Schmidt, D. (ed.) ESOP 2004. LNCS, vol. 2986, pp. 33–48. Springer, Heidelberg (2004)
Filé, G., Ranzato, F.: Improving abstract interpretations by systematic lifting to the powerset. In: Logic Programming, Proc. of the 1994 International Symposium, Ithaca, New York, USA, November 13-17, pp. 655–669 (1994)
Ghorbal, K., Goubault, E., Putot, S.: The zonotope abstract domain taylor1+. In: Bouajjani, A., Maler, O. (eds.) CAV 2009. LNCS, vol. 5643, pp. 627–633. Springer, Heidelberg (2009)
Gawlitza, T., Seidl, H., Adjé, A., Gaubert, S., Goubault, E.: Abstract interpretation meets convex optimization. J. Symb. Comput. 47(12), 1416–1446 (2012)
Ikramov, K.D., Savel’eva, N.V.: Conditionally definite matrices. Journal of Mathematical Sciences 98(1), 1–50 (2000)
Johansson, M.: On modeling, analysis and design of piecewise linear control systems. In: Proc. of the 2003 International Symposium on Circuits and Systems, ISCAS 2003, vol. 3, pp. III–646–III–649 (May 2003)
Mignone, D., Ferrari-Trecate, G., Morari, M.: Stability and stabilization of piecewise affine and hybrid systems: An lmi approach. In: Proc. of the 39th IEEE Conference on Decision and Control, vol. 1, pp. 504–509 (2000)
Miné, A.: A new numerical abstract domain based on difference-bound matrices. In: Danvy, O., Filinski, A. (eds.) PADO-II 2001. LNCS, vol. 2053, pp. 155–172. Springer, Heidelberg (2001)
Miné, A.: The octagon abstract domain. Higher-Order and Symbolic Computation 19(1), 31–100 (2006)
Martin, D.H., Jacobson, D.H.: Copositive matrices and definiteness of quadratic forms subject to homogeneous linear inequality constraints. Linear Algebra and its Applications 35(0), 227–258 (1981)
Motzkin, T.S.: Two consequences of the transposition theorem on linear inequalities. Econometrica 19(2), 184–185 (1951)
Roux, P., Garoche, P.-L.: Integrating policy iterations in abstract interpreters. In: Van Hung, D., Ogawa, M. (eds.) ATVA 2013. LNCS, vol. 8172, pp. 240–254. Springer, Heidelberg (2013)
Rantzer, A., Johansson, M.: Piecewise linear quadratic optimal control. IEEE Transactions on Automatic Control 45(4), 629–637 (2000)
Roux, P., Jobredeaux, R., Garoche, P.-L., Feron, E.: A generic ellipsoid abstract domain for linear time invariant systems. In: Dang, T., Mitchell, I. (eds.) HSCC, pp. 105–114. ACM (2012)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2015 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Adjé, A., Garoche, PL. (2015). Automatic Synthesis of Piecewise Linear Quadratic Invariants for Programs. In: D’Souza, D., Lal, A., Larsen, K.G. (eds) Verification, Model Checking, and Abstract Interpretation. VMCAI 2015. Lecture Notes in Computer Science, vol 8931. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-662-46081-8_6
Download citation
DOI: https://doi.org/10.1007/978-3-662-46081-8_6
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-662-46080-1
Online ISBN: 978-3-662-46081-8
eBook Packages: Computer ScienceComputer Science (R0)