Durand, T., Fazekas, K., Weissenbacher, G., & Zwirchmayr, J. (2021). Model Checking AUTOSAR Components with CBMC. In Proceedings of the 21st Conference on Formal Methods in Computer-Aided Design – FMCAD 2021 (pp. 96–101). TU Wien Academic Press. https://doi.org/10.34727/2021/isbn.978-3-85448-046-4_18
E192-04 - Forschungsbereich Formal Methods in Systems Engineering
-
Series:
Conference Series: Formal Methods in Computer-Aided Design
-
Published in:
Proceedings of the 21st Conference on Formal Methods in Computer-Aided Design – FMCAD 2021
-
Date (published):
Oct-2021
-
Number of Pages:
6
-
Publisher:
TU Wien Academic Press, Wien
-
Peer reviewed:
Yes
-
Keywords:
formal method
en
formale Methode
de
Abstract:
Automotive software needs to comply with stringent
functional safety standards to reduce the risk of malfunction.
In particular, the ISO 26262 standard highly recommends the
use of formal verification for highly safety-critical software
components. Automated formal verification techniques (such as
Model Checking) enable the quick detection of intricate software
bugs and can, to a limited extent, even guarantee their absence.
We report our efforts to deploy the openly available verification
tool CBMC to verify AUTOSAR Software Components and
Complex Device Drivers using Bounded Model Checking and
k-induction combined with upfront static analysis.
CC BY 4.0
