TY - GEN
T1 - SMT-Based Stability Verification of an Industrial Switched PI Control Systems
AU - Basagiannis, Stylianos
AU - Battista, Ludovico
AU - Becchi, Anna
AU - Cimatti, Alessandro
AU - Giantamidis, Georgios
AU - Mover, Sergio
AU - Tacchella, Alberto
AU - Tonetta, Stefano
AU - Tsachouridis, Vassilios
N1 - Publisher Copyright:
© 2023 IEEE.
PY - 2023/1/1
Y1 - 2023/1/1
N2 - The control of complex systems is typically designed describing the physical system with differential equations. The standard approach to their verification employs numerical analysis, which is suitable to prove stability properties, but is susceptible to numerical errors. On the other side, symbolic techniques give precise analysis results but typically do not scale to industrial size problems. In this paper, we consider the control design of an aircraft engine. The engine model is represented by a linear state space model of 18 internal state variables, 4 outputs, and 3 inputs. The control switches between two PI controllers, one for thrust control and another for low-pressure compressor spool speed control, based on the engine state and pilot commands. After reformulating the PI controllers in terms of differential equations, we obtain a hybrid system with 21 state variables and two modes, for which we want to prove with symbolic techniques the robustness of the stable states to perturbation. We achieved the verification with standard methods to synthesize quadratic Lyapunov functions and SMT techniques to synthesize neighborhoods of the stable states for which we have symbolic proof of stability.
AB - The control of complex systems is typically designed describing the physical system with differential equations. The standard approach to their verification employs numerical analysis, which is suitable to prove stability properties, but is susceptible to numerical errors. On the other side, symbolic techniques give precise analysis results but typically do not scale to industrial size problems. In this paper, we consider the control design of an aircraft engine. The engine model is represented by a linear state space model of 18 internal state variables, 4 outputs, and 3 inputs. The control switches between two PI controllers, one for thrust control and another for low-pressure compressor spool speed control, based on the engine state and pilot commands. After reformulating the PI controllers in terms of differential equations, we obtain a hybrid system with 21 state variables and two modes, for which we want to prove with symbolic techniques the robustness of the stable states to perturbation. We achieved the verification with standard methods to synthesize quadratic Lyapunov functions and SMT techniques to synthesize neighborhoods of the stable states for which we have symbolic proof of stability.
KW - Formal methods
KW - Hybrid systems
KW - Lyapunov functions
KW - SMT
KW - Stability
U2 - 10.1109/DSN-W58399.2023.00063
DO - 10.1109/DSN-W58399.2023.00063
M3 - Conference contribution
AN - SCOPUS:85169473624
T3 - Proceedings - 53rd Annual IEEE/IFIP International Conference on Dependable Systems and Networks Workshops Volume, DSN-W 2023
SP - 243
EP - 250
BT - Proceedings - 53rd Annual IEEE/IFIP International Conference on Dependable Systems and Networks Workshops Volume, DSN-W 2023
PB - Institute of Electrical and Electronics Engineers Inc.
T2 - 53rd Annual IEEE/IFIP International Conference on Dependable Systems and Networks Workshops Volume, DSN-W 2023
Y2 - 27 June 2023 through 30 June 2023
ER -