Browse Publications Technical Papers 2011-01-2558
2011-10-18

Towards Cooperation of Formal Methods for the Analysis of Critical Control Systems 2011-01-2558

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.

SAE MOBILUS

Subscribers can view annotate, and download all of SAE's content. Learn More »

Access SAE MOBILUS »

Members save up to 18% off list price.
Login to see discount.
We also recommend:
TECHNICAL PAPER

Validation of Control Software Specification Using Design Interests Extraction and Model Checking

2012-01-0960

View Details

TECHNICAL PAPER

Software-in-the-Loop Simulation Environment Realization using Matlab/Simulink

2006-01-1470

View Details

TECHNICAL PAPER

A User Configurable Powertrain Controller with Open Software Management

2007-01-1601

View Details

X