Skip to content

Formal Verification of Control System Properties with Theorem Proving

Research output: Contribution to conferencePoster

Original languageEnglish
DatePublished - 9 Jul 2014
Event2014 UKACC International Conference on Control - Loughborough, United Kingdom
Duration: 9 Jul 201411 Jul 2014

Conference

Conference2014 UKACC International Conference on Control
CountryUnited Kingdom
CityLoughborough
Period9/07/1411/07/14

Abstract

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.

Event

2014 UKACC International Conference on Control

Duration9 Jul 201411 Jul 2014
CityLoughborough
CountryUnited Kingdom
Degree of recognitionInternational event

Event: Conference

Documents

View research connections

Related faculties, schools or groups