Applying software model checking: experiences and advancements

Berger, Philipp; Beyer, Dirk; Katoen, Joost-Pieter

doi:10.18154/RWTH-2024-10081

Applying software model checking: experiences and advancements

Berger, Philipp^RWTH*

2024

Verantwortlichkeitsangabevorgelegt von Philipp Berger, M. Sc.

ImpressumAachen : RWTH Aachen University 2024

Umfang1 Online-Ressource : Illustrationen

Dissertation, RWTH Aachen University, 2023

Veröffentlicht auf dem Publikationsserver der RWTH Aachen University 2024

Genehmigende Fakultät
Fak01

Hauptberichter/Gutachter
Katoen, Joost-Pieter (Thesis advisor)^RWTH* ; Beyer, Dirk (Thesis advisor)

Tag der mündlichen Prüfung/Habilitation
2023-12-13

Online
DOI: 10.18154/RWTH-2024-10081
URL: https://publications.rwth-aachen.de/record/995701/files/995701.pdf

Einrichtungen

Inhaltliche Beschreibung (Schlagwörter)
C code (frei) ; Simulink (frei) ; automotive (frei) ; case studies (frei) ; model checking (frei) ; verification (frei) ; witness validation (frei)

Thematische Einordnung (Klassifikation)
DDC: 004

Kurzfassung
Wir stellen eine ausführliche Untersuchung über die Anwendbarkeit formaler Methoden für Software Model Checking vor, wobei ein besonderer Schwerpunkt auf der Automobilindustrie liegt. Die Arbeit basiert auf einer praktischen Studie, die mit der Ford Motor Company durchgeführt wurde und eine Grundlage für die Erforschung und Verbesserung von kommerziellen sowie akademischen Model Checkern bietet. Im ersten Teil der Studie arbeiteten wir mit der Ford Motor Company zusammen, um anhand zweier Fallstudien aus der Automobilindustrie ihre natürlich sprachlichen Anforderungen mit Hilfe des kommerziellen C-Code Model Checkers BTC Embedded Platform zu formalisieren. Unsere Untersuchung konzentrierte sich auf die Verifikation von C-Code, der aus Simulink-Modellen automatisch generiert wurde. Dabei analysierten wir die damit verbundenen Herausforderungen und erarbeiteten praktische Empfehlungen sowohl für Ingenieure als auch für Tool-Entwickler. Auf dieser Grundlage haben wir akademische C-Code Model Checker auf dieselben Fallstudien angewandt und ihre Leistung mit der von BTC Embedded Platform verglichen. Dieser Vergleich lieferte eine Reihe neuer Erkenntnisse und Empfehlungen zur Verbesserung akademischer Model Checker. Der zweite Teil dieser Arbeit befasst sich mit der Entwicklung neuer Werkzeuge und Methoden, um den Stand der Technik im Software Model Checking zu verbessern. Zunächst haben wir NITWIT entwickelt, einen neuartigen Violation Witness Validator basierend auf der Interpretation von C-Code. Dieser Ansatz ermöglicht kurze Laufzeiten mit minimalem Speicherbedarf und ist unabhängig von bestehenden Model Checkern. Als nächstes haben wir ein Werkzeug zum Verfassen von Spezifikationen mit formaler Semantik entwickelt, das speziell auf die Automobilindustrie zugeschnitten ist. Dieses erzeugt automatisch einerseits Spezifikationen in Simulink, BTC und reinem C-Code, wodurch der formale Verifizierungsprozess verschlankt wird, sowie andererseits Repräsentationen in natürlicher Sprache mit wohldefinierter Semantik, die auch von Nicht-Experten geprüft und verwendet werden können. Schließlich haben wir ein Tool zur Erzeugung von C-Code entwickelt, um das Testen und Benchmarken von C-Code Model Checkern zu erleichtern. Der erzeugte Code orientiert sich an den beiden Fallstudien und stellt somit eine wertvolle Ressource für Stresstests von Model Checkern dar, da eine Vielzahl von kontrollierbaren Code-Metriken, Features und Transformern angeboten wird. Zusätzlich können Geheimhaltungsvereinbarungen durch Anonymisierung und Verfremdung eingehalten werden. Zusammenfassend bietet diese Arbeit neue und relevante Einsichten sowie innovative Werkzeuge zur Verbesserung der Anwendung und Vergleichbarkeit von Software Model Checking - insbesondere im Kontext der Automobilindustrie. Sie bietet praktische Lösungen für reale Herausforderungen und hilft, die Lücke zwischen kommerziellen und akademischen Ansätzen des Software Model Checkings zu schließen.

We present a comprehensive investigation into the applicability of formal methods for software model checking, with a particular emphasis on the automotive sector. The work is grounded in a practical study carried out with Ford Motor Company, offering a basis for the exploration and enhancement of both commercial and academic model checking tools. In the first part of the study, we collaborated with Ford Motor Company to formalise their natural language requirements for two automotive case studies employing the commercial C code model checker, BTC Embedded Platform. Our investigation focused on the verification of auto-generated C code from Simulink models, analysing the associated challenges and providing practical recommendations for both engineers and tool developers. Building on this foundation, we then applied academic C code model checkers to the same case studies, comparing their performance against BTC Embedded Platform. This comparison yielded a fresh set of insights and recommendations aimed at enhancing academic model checking tools. The second part of this work addresses the development of new tools and methods aimed at advancing the state of the art in software model checking. First, we designed NITWIT, a novel violation witness validator based on C code interpretation. This approach yields fast execution with a minimal memory footprint and is agnostic of existing model checkers. Next, we developed a tool for writing specifications with formal semantics, tailored specifically for the automotive industry. This tool is capable of auto-generating (a) specifications in Simulink, BTC and pure C code for verification, streamlining the formal verification process, and (b) natural language representations with fixed semantics for stakeholders and non-experts to review and use.Finally, to better facilitate the testing and benchmarking of C code model checkers, we built a tool that generates C code. The style of the generated code borrows from the two case studies, thus providing a valuable resource for stress-testing model checkers while respecting non-disclosure agreements, offering a wide variety of controllable code metrics, features and transformers. In summary, this thesis provides new and relevant insights as well as novel tools aimed at improving the application and comparison of software model checking, particularly in the context of the automotive industry. It offers practical solutions to real-world challenges, and helps to bridge the gap between commercial and academic approaches to software model checking.

OpenAccess:
PDF
(additional files)