Formal Verification of Control System Properties with Theorem Proving

This paper presents the formal verification of high- level properties of control systems with theorem proving (through the Why3 tool). Properties that can be verified with this approach include stability, feedback gain, and robustness, among others. The systems are modelled in Simulink and we propose how to specify the properties of interest over the signals using Simulink blocks. A library of assertion blocks (logic expressions) to annotate the Simulink model, and currently in development, is presented. The functionality and specification of properties in the blocks of the Simulink models are automatically translated from Simulink to Why3 as ‘theories’ and verification goals, respectively, by our tool implemented in MATLAB. A library of theories in Why3 has been developed to facilitate the process of translation of the different Simulink blocks. The goals are automatically verified in Why3 with relevant theorem provers. A first-order discrete system is used to exemplify both, the translation process from Simulink to the Why3 formal logic language, and the verification of Lyapunov stability through added assertion blocks over signals in the model.