+**********************************************************************

*

*

*                          Einladung

*

*

*

* Informatik-Oberseminar

*

*

*

+**********************************************************************

Zeit:  Mittwoch, 13. Dezember 2023, 16:00 Uhr

Ort:   Informatikzentrum Ahornstr. 55, Raum 5053.2 (B-IT)

Referentin:  Jana Berger M.Sc.

Lehrstuhl Informatik 2

Thema: Applying Software Model Checking: Experiences and Advancements

Abstract:

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 EmbeddedPlatform. 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 EmbeddedPlatform. 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.

Es laden ein: die Dozentinnen und Dozenten der Informatik