TY - GEN
T1 - A scalable algebraic method to infer quadratic invariants of switched systems
AU - Allamigeon, Xavier
AU - Gaubert, Stéphane
AU - Goubault, Eric
AU - Putot, Sylvie
AU - Stott, Nikolas
N1 - Publisher Copyright:
© 2015 IEEE.
PY - 2015/11/4
Y1 - 2015/11/4
N2 - We present a new numerical abstract domain based on ellipsoids designed for the formal verification of switched linear systems. Unlike the existing approaches, this domain does not rely on a user-given template. We overcome the difficulty that ellipsoids do not have a lattice structure by exhibiting a canonical operator over-approximating the union. This operator is the only one which permits to perform analyses that are invariant with respect to a linear transformation of state variables. Moreover, we show that this operator can be computed efficiently using basic algebraic operations on positive semidefinite matrices. We finally develop a fast non-linear power-type algorithm, which allows one to determine sound quadratic invariants on switched systems in a tractable way, by solving fixed point problems over the space of ellipsoids. We test our approach on several benchmarks, and compare it with the standard techniques based on linear matrix inequalities, showing an important speedup on typical instances.
AB - We present a new numerical abstract domain based on ellipsoids designed for the formal verification of switched linear systems. Unlike the existing approaches, this domain does not rely on a user-given template. We overcome the difficulty that ellipsoids do not have a lattice structure by exhibiting a canonical operator over-approximating the union. This operator is the only one which permits to perform analyses that are invariant with respect to a linear transformation of state variables. Moreover, we show that this operator can be computed efficiently using basic algebraic operations on positive semidefinite matrices. We finally develop a fast non-linear power-type algorithm, which allows one to determine sound quadratic invariants on switched systems in a tractable way, by solving fixed point problems over the space of ellipsoids. We test our approach on several benchmarks, and compare it with the standard techniques based on linear matrix inequalities, showing an important speedup on typical instances.
KW - Static analysis
KW - abstract interpretation
KW - hybrid and switched linear systems
KW - invariant generation
KW - matrix information geometry
KW - stability
U2 - 10.1109/EMSOFT.2015.7318262
DO - 10.1109/EMSOFT.2015.7318262
M3 - Conference contribution
AN - SCOPUS:84962244324
T3 - 2015 Proceedings of the International Conference on Embedded Software, EMSOFT 2015
SP - 75
EP - 84
BT - 2015 Proceedings of the International Conference on Embedded Software, EMSOFT 2015
PB - Institute of Electrical and Electronics Engineers Inc.
T2 - 13th International Conference on Embedded Software, EMSOFT 2015
Y2 - 4 October 2015 through 9 October 2015
ER -