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.

Critical systems are subject to drastic certification constraints (DO178-B for avionic systems, SIL-4 for railway systems, ISO26262 for the automotive domain), which require system providers to produce strong evidence for the correctness, reliability, or performance of their systems. Today, the early use of formal modeling and verification methods is recognized as favorable by the industry. Formal methods, which started to appear in the 60's, have now reached a maturity level allowing them to be used in an industrial context. The approach of control system modeling as proposed by the MathWorks with MATLAB Simulink, by Esterel Technologies with the SCADE language or by the academic community with the Lustre language, is extensively used for reactive systems design and often allows the automatic generation of the embedded code.