This content is not included in
your SAE MOBILUS subscription, or you are not logged in.
Formal Verification Method for Safety Diagnosis Software
Technical Paper
2015-01-0279
ISSN: 0148-7191, e-ISSN: 2688-3627
Annotation ability available
Sector:
Language:
English
Abstract
Functions and sizes of electronic control and software systems in automotives are being increased to achieve better controllability and reduce fuel consumption. A higher safety level is also demanded, so functional-safety standards are increasingly being introduced to in-vehicle systems.
In safety critical systems, failure must be diagnosed and a system transited to a safe state when hardware failure occurs. Therefore, the failure diagnosis part of the basic software that takes charge of signal inputs and outputs processing must be verified for high accountability and explanations to a third party. To diagnose failure, the hardware and software that originally operate independently need to cooperate in principle. Hardware and software cooperating systems are not straight-forward to verify, because the combinations of conditions are too numerous for testing.
The formal verification technology is effective, because it enables exhaustive verification of a vast quantity of test cases including unexpected states, such as a failed state. However, modeling methodology has not been established for timing related uncertainty between hardware failure and software.
Our proposed method is to model a combination of the concurrent executions of both hardware and software operations under uncertain delay. We chose a C-language based model checker, which is formal verification software. We developed the uncertain delay injection mechanism and random hardware failure injection mechanism on the model checker software. Delay injection made it possible to model a concurrent hardware and software cooperating system with jitter and failure injection, which enables fail-safe behavior to be verified.
Recommended Content
Authors
Citation
Narisawa, F., Matsubara, M., Nishi, M., and Ebina, T., "Formal Verification Method for Safety Diagnosis Software," SAE Technical Paper 2015-01-0279, 2015, https://doi.org/10.4271/2015-01-0279.Also In
References
- Clarke Edmund , Kroening Daniel , and Lerda Flavio A tool for checking ansi-c programs Tools and Algorithms for the Construction and Analysis of Systems 168 176 Springer 2004
- Cordeiro Lucas and Fischer Bernd Verifying multi-threaded software using smt-based context-bounded model checking Proceedings of the 33rd International Conference on Software Engineering, ICSE '11 331 340 New York, NY, USA 2011 ACM
- Sinz Carsten , Falke Stephan , and Merz Florian A Precise Memory Model for Low-Level Bounded model Checking Proceeding Proceedings of the 5th international conference on Systems software verification SSV'10 7 7
- Cordeiro L. . Fischer B. , and Marques-Silva J. SMT-based bounded model checking for embedded ANSI-C software Porceedings of ASE 2009 2009 302 314
- Clarke E. , Grumberg O. , and Peled D. Model Checking The MIT Press January 2000
- Chabrol Damien , Roux Didier , David Vincent , Jan Mathieu , Hmid Moha Ait , Oudin Patrice , and Zeppa Gilles Time- and angle-triggered real-time kernel Proceedings of the Conference on Design, Automation and Test in Europe DATE '13 1060 1062
- ISO26262 Road Vehicles-Functional Safety, Part 1-10, International Organization for Standardization http://www.iso.org 2011
- Holzmann Gerard J. The Spin Model Checker - Primer and Reference Manual Addison-Wesley 2003