Browse Publications Technical Papers 2005-01-0781

Formal Verification for Model-Based Development 2005-01-0781

Formal verification is increasingly used for checking and proving the correctness of digital systems. In this paper, we present formal verification as a cost-effective technique for the verification and validation of model-based safety-critical embedded systems.
We start by explaining how formal verification can be easily integrated in a model-based development methodology for critical embedded software. In the methodology examined, the development methods are based upon a formal and deterministic language representation and a correct-by-construction automatic code generation. In this methodology, formal verification proves that what you execute conforms to safety requirements, and what you execute is exactly what you embed. We show the impacts and benefits of using formal verification in software development that must be compliant with the IEC 61508 standards, especially for SIL 3 and SIL 4 software development. We conclude by detailing specific formal verification techniques and tools available today for use in a state-of-the-art model-based development environment. We focus on the verification of safety requirements, involving control-logic aspects as well as data computation aspects of embedded software. We explain how to relate this model-checking activity with the objectives of the software life cycle process described in the IEC 61508 standards.
Figures on the use of the SCADE product and its Design Verifier module on several realistic safety-related automotive applications illustrate the presentation.


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


Members save up to 17% off list price.
Login to see discount.
Special Offer: Download multiple Technical Papers each year? TechSelect is a cost-effective subscription option to select and download 12-100 full-text Technical Papers per year. Find more information here.
We also recommend:

Software Certification for a Time-Triggered Operating System


View Details


Breakthrough Approach to Automotive Diagnostic Verification


View Details


Test Strategy for Linux based Platforms using Open Source Tools


View Details