Verification of Functional Requirements of Embedded Automotive C Code

Abstract: Today's vehicles are increasingly controlled by embedded computer systems. Such systems are of safety-critical nature, where an error in the computation could have dire consequences. A common way to ensure that software works is testing, but as the complexity of these systems grows larger it gets harder to ensure enough coverage in the tests. Another way to ensure that software fulfills its requirements is formal verification, where properties of the code are proven mathematically to hold under certain conditions. Formal verification gives a higher level of confidence in the correctness of code than testing alone, but it is not as widely used within the industry. This project has examined whether current state-of-the-art tools for formal verification are ready to be used to verify real-life safety-critical code. To answer this, a case study on a module running in Scania's vehicles was performed. Several of the requirements were successfully verified. The thesis also identifies for what type of code and requirements this is possible, and describes a process for how it can be done.