Formal Verification of AUTOSAR Watchdog Manager Module Using Symbolic Execution

摘要

This paper proposes a new seamless and simple technique for the compliance of AUTOSAR software with functional safety standards presented in ISO-26262 standard. This new technique uses formal verification based on symbolic execution algorithms to verify that the requirements specified by the AUTOSAR software specifications for watchdog manager module are correctly covered in the implemented software. Formal verification trials were recently done in this area as proposed by ASIL C and D levels. However, they faced many barriers either due to the software complexity increase or due to the difficulty of formal verification methods. Our new proposal is a high safety level verification technique, since it verifies the software code using formal verification techniques. This approach helps in unmasking any hidden bug early in the design stage. Experimental results illustrate the efficiency of the approach in reaching high coverage results.