Formal Hardware/Firmware Co-Verification of Optimized Embedded Systems

  • Small embedded devices are highly specialized platforms that integrate several pe- ripherals alongside the CPU core. Embedded devices extensively rely on Firmware (FW) to control and access the peripherals as well as other important functionality. Customizing embedded computing platforms to specific application domains often necessitates optimizing the firmware and/or the HW/SW interface under tight re- source constraints. Such optimizations frequently alter the communication between the firmware and the peripheral devices, possibly compromising functional correct- ness of the input/output behavior of the embedded system. This poses challenges to the development and verification of such systems. The system must be adapted and verified to each specific device configuration. This thesis presents a formal approach to formulate these verification tasks at several levels of abstraction, along with corresponding HW/SW co-equivalence checking techniques for verifying correct I/O behavior of peripherals under a modified firmware. The feasibility of the approach is shown on several case studies, including industrial driver software as well as open-source peripherals. In addition, a subtle bug in one of the peripherals and several undocumented preconditions for correct device behavior were detected by the verification method.
Metadaten
Author:Michael Schwarz
URN:urn:nbn:de:hbz:386-kluedo-65620
DOI:https://doi.org/10.26204/KLUEDO/6562
Advisor:Wolfgang Kunz
Document Type:Doctoral Thesis
Language of publication:English
Date of Publication (online):2021/09/10
Year of first Publication:2021
Publishing Institution:Technische Universität Kaiserslautern
Granting Institution:Technische Universität Kaiserslautern
Acceptance Date of the Thesis:2021/06/25
Date of the Publication (Server):2021/09/13
Page Number:V, 112
Faculties / Organisational entities:Kaiserslautern - Fachbereich Elektrotechnik und Informationstechnik
CCS-Classification (computer science):B. Hardware / B.7 INTEGRATED CIRCUITS / B.7.2 Design Aids / Verification
DDC-Cassification:6 Technik, Medizin, angewandte Wissenschaften / 621.3 Elektrotechnik, Elektronik
MSC-Classification (mathematics):94-XX INFORMATION AND COMMUNICATION, CIRCUITS / 94Cxx Circuits, networks / 94C60 Circuits in qualitative investigation and simulation of models
Licence (German):Creative Commons 4.0 - Namensnennung, nicht kommerziell, keine Bearbeitung (CC BY-NC-ND 4.0)