Bryan Daniel Olmos Suquillo

• Electronic safety systems need to guarantee a certain level of dependability. Therefore, their development must consider robust hardware and trustworthy and reliable embedded software such as firmware, drivers and bare metal software. The main purpose of these elements is to interact with the hardware elements such as timers, ADC converters, bus interfaces, peripherals, counters and I/O interfaces. For this reason, their verification also needs to consider these elements, which brings new challenges compared with traditional verification of high-level software, which has mainly been studied in the past 20 years. Additionally, safety-critical systems such as automotive systems are required to ensure high levels of dependability. Thus, the use of formal methods has increased in the industry, especially in the case of hardware. However, the application of formal methods in firmware development lacks a methodology that considers its interaction with hardware elements, its automation and the current verification techniques to be easily adapted. For this reason, this thesis proposes a Compositional Formal Verification of Automotive Firmware Development. This development must comply with standards such as ISO 26262-6 and ISO 21434. Furthermore, it must address the inherent challenges of software verification, including reachability, software weaknesses, and code coverage. The proposed methodology shows how different formal verification techniques can be applied in various development stages to increase the reliability of FW designs of 8, 16, and 32 bits, considering C and Rust-based designs. Furthermore, the use of metamodeling techniques and Model-Driven Engineering (MDE) allows for the automation of the verification process. The results show that the approach is scalable for big designs if we consider modular verification. Most of the properties run in minutes or even seconds, and the results show that complete designs can be verified in hours, which is a significant advantage over simulation methods, where the runtime increases exponentially with the bit width of the function variables. Besides, the HW interaction considers the inclusion of FWHW Co-verification and High-Level Equivalence Checking techniques, which normally rely on constraints that can be reused not only in the FW verification phase, but also in the integration phase. Finally, this thesis provides the main guidelines to be considered during the design process to enable automated verification. These guidelines include recommendations for software verification and new optimization techniques for hardware development, which will be proposed and analyzed during the development of this thesis.
• Sicherheitskritische elektronische Systeme müssen ein hohes Maß an Zuverlässigkeit garantieren. Die Entwicklung solcher Systeme muss daher sowohl robuste Hardware sowie vertrauenswürdige und zuverlässige Softwarekomponenten berücksichtigen. Hierbei handelt es sich um eingebettete Software wie Firmware, Treiber und Bare-Metal-Applikationen, deren Hauptzweck die Interaktion mit Hardwareelementen wie Timern, Analog-Digital-Wandlern, Busschnittstellen, Peripheriegeräten, Zählern und I/O-Schnittstellen ist. Die Verifikation solcher Systeme muss daher all die genannten Hard- und Softwarekomponenten und deren Interaktionen berücksichtigen, was im Vergleich zur traditionellen Verifikation von High-Level-Software neue Herausforderungen mit sich bringt, welche hauptsächlich in den letzten 20 Jahren untersucht wurden. Insbesondere in der Automobilindustrie, in der strenge Zuverlässigkeitsstandards wie ISO 26262-6 und ISO 21434 gelten, hat der Einsatz formaler Methoden in der Hardwareentwicklung zugenommen. Allerdings fehlt es der Anwendung formaler Methoden in der Firmwareentwicklung an einer Methodik, welche die Interaktion mit Hardwareelementen sowie den Einsatz aktueller Verifikationstechniken und deren Automatisierung berücksichtigt. Zudem müssen hierbei inhärente Herausforderungen der Softwareverifikation, einschließlich Erreichbarkeit, Softwareschwachstellen und Codeabdeckung, adressiert werden. Diesen Herausforderungen nimmt sich die vorliegende Arbeit an und präsentiert eine kompositionelle formale Verifikation der Automobil-Firmwareentwicklung. Die ausgearbeitete Methodik zeigt, wie verschiedene formale Verifikationstechniken in unterschiedlichen Entwicklungsphasen angewendet werden können, um die Zuverlässigkeit von Firmware-Designs mit 8, 16 und 32 Bit zu erhöhen, insbesondere bei C- und Rust-basierten Designs. Darüber hinaus ermöglicht der Einsatz von Metamodellierungstechniken und modellgetriebener Entwicklung die Automatisierung des Verifikationsprozesses. Experimentell lässt sich zeigen, dass unter dem Einsatz modularer Verifikation der Ansatz auch für große Designs skalierbar ist. Der Großteil der formalen Eigenschaftsprüfung konvergiert innerhalb von Sekunden bis Minuten, und die Ergebnisse zeigen, dass auch komplexe Designs innerhalb von Stunden vollständig verifiziert werden können. Gegenüber Simulationsmethoden, bei denen die Laufzeit exponentiell mit der Bitbreite der Funktionsvariablen zunimmt, stellt dies einen erheblichen Vorteil dar. Außerdem berücksichtigt die Hardwareinteraktion die Einbeziehung von Firmware-Hardware-Co-Verifikation und High-Level-Equivalence-Checking-Techniken, die normalerweise auf Einschränkungen beruhen, die nicht nur während der Firmwareverifikationsphase, sondern auch in der Integrationsphase wiederverwendet werden können. Darüber hinaus beinhaltet diese Arbeit Hauptleitlinien zur Automatisierung der Verifikation, die während des Entwicklungsprozesses berücksichtigt werden müssen. Diese Leitlinien umfassen Empfehlungen zur Softwareverifikation und neue Optimierungstechniken für die Hardwareentwicklung, welche im Zuge dieser Arbeit formuliert und analysiert werden