Formal analysis of robustness at model and code level

Timothy Wang, Pierre Loïc Garoche, Pierre Roux, Romain Jobredeaux, Éric Féron

Research output: Chapter in Book/Report/Conference proceedingConference contribution

7 Scopus citations

Abstract

Robustness analyses play a major role in the synthesis and analysis of controllers. For control systems, robustness is a measure of the maximum tolerable model inaccuracies or perturbations that do not destabilize the system. Analyzing the robustness of a closed-loop system can be performed with multiple approaches: gain and phase margin computation for single-input single-output (SISO) linear systems, mu analysis, IQC computations, etc. However, none of these techniques consider the actual code in their analyses. The approach presented here relies on an invariant computation on the discrete system dynamics. Using semi-definite programming (SDP) solvers, a Lyapunov-based function is synthesized that captures the vector margins of the closedloop linear system considered. This numerical invariant expressed over the state variables of the system is compatible with code analysis and enables its validation on the code artifact. This automatic analysis extends verification techniques focused on controller implementation, addressing validation of robustness at model and code level. It has been implemented in a tool analyzing discrete SISO systems and generating over-Approximations of phase and gain margins. The analysis will be integrated in our toolchain for Simulink and Lustre models autocoding and formal analysis.
Original languageEnglish (US)
Title of host publicationHSCC 2016 - Proceedings of the 19th International Conference on Hybrid Systems: Computation and Control
PublisherAssociation for Computing Machinery, Incacmhelp@acm.org
Pages125-134
Number of pages10
ISBN (Print)9781450339551
DOIs
StatePublished - Apr 11 2016
Externally publishedYes

Fingerprint

Dive into the research topics of 'Formal analysis of robustness at model and code level'. Together they form a unique fingerprint.

Cite this