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
