Formal Methods for the Analysis of Critical Control Systems Models: Combining Non-Linear and Linear Analyses

• Published in: SAE International Journal of Aerospace 2013-09, Vol.6 (1), p.150-160, Article 2013-01-2109
• Main Authors: Champion, Adrien, Delmas, Rémi, Dierkes, Michael, Garoche, Pierre-loic, Jobredeaux, Romain, Roux, Pierre
• Format: Article
• Language: English
• Subjects: Control systems; Formal method; Proportional integral derivative
• ISSN: 1946-3855; 1946-3901; 1946-3901
• DOI: 10.4271/2013-01-2109

Critical control systems are often built as a combination of a control core with safety mechanisms allowing to recover from failures. For example a PID controller used with triplicated inputs. Typically those systems would be designed at the model level in a synchronous language like Lustre or Simulink, and their code automatically generated from those models. In previous SAE symposium, we addressed the formal analysis of such systems - focusing on the safety parts - using a combination of formal techniques, ie. k-induction and abstract interpretation. The approach developed here extends the analysis of the system to the control core. We present a new analysis framework combining the analysis of open-loop stable controller with those safety constructs. We introduce the basic analysis approaches: abstract interpretation synthesizing quadratic invariants and backward analysis based on quantifier elimination. Then we apply it on a simple but representative example that no other available state-of-the-art technique is able to analyze. This contribution is another step towards early use of formal methods for critical embedded software such as the ones of the aerospace industry.