This content is not included in
your SAE MOBILUS subscription, or you are not logged in.
Formal Verification for Model-Based Development
Technical Paper
2005-01-0781
ISSN: 0148-7191, e-ISSN: 2688-3627
Annotation ability available
Sector:
Language:
English
Abstract
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.
Recommended Content
Technical Paper | Software Certification for a Time-Triggered Operating System |
Technical Paper | Breakthrough Approach to Automotive Diagnostic Verification |
Technical Paper | Hardware and Software Development and Integration per SAE ARP4754A |
Citation
Bouali, A. and Dion, B., "Formal Verification for Model-Based Development," SAE Technical Paper 2005-01-0781, 2005, https://doi.org/10.4271/2005-01-0781.Also In
Occupant Safety, Safety-Critical Systems, and Crashworthiness
Number: SP-1923; Published: 2005-04-11
Number: SP-1923; Published: 2005-04-11
SAE 2005 Transactions Journal of Passenger Cars: Electronic and Electrical Systems
Number: V114-7; Published: 2006-02-01
Number: V114-7; Published: 2006-02-01
References
- IEC 61508 1998 Functional safety of electrical / electronic / programmable electronic safety-related systems
- Bernard Dion Correct-By-Construction Methods for the Development of Safety-Critical Applications SAE World Congress 2003, Paper Number 04AE-129
- Bouali Amar Coffer Darren Dajani-Brown Samar Formal Verification of an Avionics Sensor Voter Proc. of the international conference on Formal Techniques for Real-Time and Fault-Tolerant Systems (FTRTFT) Grenoble, France Sep. 2004
- Camus Jean-Louis Dion Bernard Efficient Development of Airborne Software with SCADE Suite Esterel Technologies 2003
- Pilarski François Cost effectiveness of formal methods in the development of avionics systems at Aerospatiale 17th Digital Avionics Conference Nov. 1st-5th 1998 Seattle, WA
- Sheeran Mary Singh Satnam Stålmarck Gunnar Checking safety properties using induction and a SAT-solver Proc. Formal Methods in Computer Aided Design (FMCAD 2000) Springer LNCS Nov. 2000
- Esterel Technologies http://www.esterel-technologies.com
- Prover Technology http://www.prover.com