Formal Verification of Control System Properties with Theorem Proving

Dejanira Araiza Illan, Kerstin I Eder, Arthur G Richards

Research output: Contribution to conferenceConference Posterpeer-review


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.
Original languageEnglish
Publication statusPublished - 9 Jul 2014
Event2014 UKACC International Conference on Control - Loughborough, United Kingdom
Duration: 9 Jul 201411 Jul 2014


Conference2014 UKACC International Conference on Control
CountryUnited Kingdom

Fingerprint Dive into the research topics of 'Formal Verification of Control System Properties with Theorem Proving'. Together they form a unique fingerprint.

Cite this