This content is not included in your SAE MOBILUS subscription, or you are not logged in.
Formal Methods for the Analysis of Critical Control Systems Models: Combining Non-Linear and Linear Analyses
ISSN: 1946-3855, e-ISSN: 1946-3901
Published September 17, 2013 by SAE International in United States
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.
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.