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. However, despite the existence of a few formal verification tools supporting these languages, few system builders actually rely on formal approaches to demonstrate safety properties of their software products.
Among the different formal proof techniques available for such models, the k-induction approach gives nice results but often needs external help in order to conclude non-trivial proofs and scale up.
Another method, abstract interpretation, is very efficient to discover properties over programs or models but is not well developed at model level to verify user specified properties.
The novelty of our framework is the tight cooperation between the k-induction engine and the abstract interpretation engine on the analysis of safety properties. The cooperation approach consists in using the abstract interpreter as an oracle in order to infer and inject numerical invariants in the k-induction analysis to prevent spurious falsifications of the induction scheme.
This new collaborative approach seems to be a valuable way to overcome identified drawbacks of each technique and ease the scalability of formal methods at model level.
