Search Results

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.