Verifying automotive software components using C model checkers

Abstract

Softwaresysteme, die für die Automobilindustrie entwickelt werden, erleben derzeit einen enormen Anstieg der Komplexität, der mit einer Erhöhung der Sicherheitsanforderungen einhergeht. Die Sicherstellung ihrer Korrektheit ist eine herausfordernde und kostspielige Aufgabe, welcher die Forschung nach neuen technologischen Lösungen motiviert. Software-Verifikationswerkzeuge, die auf C-Code abzielen, sind zwar in der Industrie noch nicht weit verbreitet, zeigen aber jedes Jahr beeindruckende Leistungsverbesserungen, was sie zu guten Kandidaten für die Gewährleistung der Sicherheit eingebetteter Systeme macht. Das Ziel dieser Studie ist es, die Fähigkeit modernster Verifikationswerkzeuge zu bewerten, welche die Abwesenheit von Laufzeitfehlern bei vier Softwarekomponenten unterschiedlicher Komplexität nachzuweisen. Diese Komponenten aus der realen Welt werden von TTTech entwickelt, einer Firma, die auf sicherheitsbezogene Lösungen für die Automobilindustrie spezialisiert ist. Zunächst erstellen wir ein generisches Umgebungsmodell, das auf dem AUTOSAR-Standard basiert, der in der Automobilindustrie weit verbreitet ist. Dieses Modell zielt darauf ab, eine Komponente von der übrigen Software-Plattform für die Verifikation zu isolieren, und verwendet bereits existierende, durch den Standard definierte Spezifikationen. Anschließend prüfen wir den Code mit Ultimate Automizer, CPAChecker und CBMC, ergänzt durch Ideen wie z.B. k-Induktion oder Analyse des variablen Bereichs.Unsere Ergebnisse zeigen, dass Verifikationswerkzeuge in der Lage sind, die Fehlerfreiheit von drei von vier Komponenten erfolgreich nachzuweisen, jedoch für die komplexeste Komponente keine definitive Antwort geben können. Die leistungsfähigste Verifikationsmethode ergibt sich aus der Kombination der Ergebnisse verschiedener Code-Analysen, wobei CBMC das endgültige Urteil mittels k-Induktion feststellt. Für den problematischen Fall geben wir Einblicke in die Ursachen der Schwierigkeiten und die nächsten Schritte, die zu deren Überwindung erforderlich sind. Wir kommen zu dem Schluss, dass die Einführung von Verifikationswerkzeugen in den Entwicklungsprozess positive Veränderungen der allgemeinen Codequalität mit sich bringen kann.

Software systems developed for the automobile industry are currently witnessing a tremendous increase in complexity, happening in concert with an escalation of safety requirements. Ensuring their correctness is a challenging and costly task, which motivates the research for new technological solutions. While not yet broadly adopted in industry, software verification tools targeting C code demonstrate impressive performance improvements every year, which makes them good candidates for ensuring the safety of embedded systems. This study aims at evaluating the capacity of state-of-the-art verification tools for proving the absence of run-time errors on four software components of various complexity. These real-world components are developed by TTTech, a firm specialized in safety-related automotive solutions. Firstly, we establish a generic environment model based on the AUTOSAR standard, which is broadly adopted in the automobile industry. This model aims at isolating a component from the rest of the software platform for verification, and uses already-existing specifications defined by the standard. We then check the code using Ultimate Automizer, CPAChecker and CBMC extended with several ideas, such as k-induction or variable range analysis. Our results show that verification tools are able to successfully prove the absence of errors in three out of four components, and cannot give a definite answer for the most complex one. The most capable verification method is obtained by combining the results of different code analyzes, with CBMC establishing the final verdict using k-induction. For the problematic case, we give insights into the causes of difficulties, and next steps required to overcome them. We conclude that introducing verification tools in the development process can bring positive changes to the general code quality.