Formal Methods for the Analysis of Critical Control Systems Models: Combining Non-Linear and Linear Analyses 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.
Citation: Champion, A., Delmas, R., Dierkes, M., Garoche, P. et al., "Formal Methods for the Analysis of Critical Control Systems Models: Combining Non-Linear and Linear Analyses," SAE Int. J. Aerosp. 6(1):150-160, 2013, https://doi.org/10.4271/2013-01-2109. Download Citation
Adrien Champion, Rémi Delmas, Michael Dierkes, Pierre-loic Garoche, Romain Jobredeaux, Pierre Roux
Rockwell Collins France, ONERA, Georgia Tech Univ and Univ of Toulouse
SAE 2013 AeroTech Congress & Exhibition
SAE International Journal of Aerospace-V122-1, SAE International Journal of Aerospace-V122-1EJ