Verification of temporal properties in embedded software

Abstract

For some years ago the main statement among verification engineers was “Bugs in hardware cost money”. Nowadays, the embedded software is playing an important role in the embedded systems industry and the statement can be updated to “Bugs in hardware and in software cost a lot of money”. Embedded software is very powerful in embedded systems in order to implement important functionalities and functional innovations. The developing costs of embedded software are becoming huge and its amount in safety critical systems is increasing. Therefore, the verification of complex systems needs to consider the verification of both hardware and embedded software modules.

The most commonly used approaches to verify embedded software are based on co-simulation or on co-debugging, which consume long verification time and additionally have coverage limitations. Formal verification assures complete coverage, but is limited to the size of the module that can be verified. This dissertation extends the conventional verification limitations with methodologies that are based on temporal properties and formal verification. This work proposes to combine temporal assertions with testing, which is suitable to be applied in existing design flows due to the experience of the verification engineers with conventional verification approaches. Thus, the formalization of the requirements by means of temporal properties is able to improve the understanding about the design and the assertions can be re-used later in the combination of simulation and formal verification approaches.

The main contributions in this dissertation are (1) two new approaches to integrate assertionbased verification in embedded software verification and (2) one new semiformal verification approach to increase state space coverage compared to simulation-based methods. The developed solutions are evaluated against an industrial automotive embedded software application.

Targeting at simulation-based verification techniques, new approaches are identified and investigated to efficiently integrate assertions in the verification of embedded software: On the one hand, a SystemC hardware temporal checker is extended with interfaces to monitor the embedded software variables and functions that are stored in a microprocessor memory model. On the other hand, a SystemC model is derived from the original C code to integrate directly with the SystemC temporal checker. The first approach shows the advantage to verify temporal properties in C programs straightforward under real conditions, however, requiring to explicitly model the microprocessor itself. For the second approach, a shorter verification time is achieved, however, a SystemC model has to be generated with more abstraction information. Due to the limitations of simulation-based approaches, a new semiformal verification is developed.

Targeting at semiformal verification techniques, an approach called SofTPaDS (Semiformal Verification of Temporal Properties in Hardware-Dependent Software), which is based on the combination of both assertion-based and symbolic simulation strategies for the verification of embedded software with hardware dependencies, is designed. In this approach, a simulation-based traversing of the state space is combined with local (temporal restricted) explorations of specific states on the simulation traces. The semiformal approach is evaluated to be more efficient than state-of-the-art model checkers in order to trace deep state spaces, and shows improvements in the state coverage relative to a simulation-based software verification approach.

Vor einigen Jahren war eine gängige Aussage von Verifikationsingenieuren „Fehler in Hardware kosten Geld”. Heutzutage spielt eingebettete Software im Bereich eingebetteter Systeme eine immer wichtigere Rolle und die Aussage kann aktualisiert werden zu „Fehler in Hardware und Software kosten sehr viel Geld”. Eingebettete Software schafft im Bereich eingebetteter Systeme die Grundlage für die Implementierung neuer Funktionalität und liefert damit einen wesentlichen Treiber für die Realisierung von Innovation. Dabei nehmen die Kosten für die Entwicklung eingebetteter Software stetig zu und deren Anteil in sicherheitskritischen Systemen vergrößert sich kontinuierlich. Aus diesem Grund muss die Verifikation komplexer eingebetteter Systeme sowohl die Hardware als auch die Software des Systems in die Betrachtung einbeziehen.

Die heute zum Einsatz kommenden Verifikationstechniken für eingebettete Software basieren auf Co-Simulation oder Co-Debugging, woraus ein hoher Zeitaufwand und eine beschränkte Abdeckung der Verifikation resultieren. Im Gegensatz dazu garantieren formale Verifikationstechniken eine vollständige Abdeckung, besitzen jedoch Beschränkungen hinsichtlich der Größe der verifizierbaren Module. Die vorliegende Dissertation erweitert die bestehende Vorgehensweise um Ansätze auf der Grundlage von temporalen Eigenschaftsbeschreibungen und formalen Verifikationstechniken. Die Arbeit kombiniert temporale Eigenschaftsbeschreibungen mit simulationsbasierten Verfahren und ermöglicht so eine einfache Einbindung neuer Methoden in industriell etablierte Entwurfsabläufe und Denkweisen. Die Formalisierung von Anforderungen in temporale Eigenschaftsbeschreibungen liefert dabei einen wichtigen Beitrag für ein besseres Verständnis des Designs und schafft die Grundlage für eine kombinierte Anwendung von simulationsbasierten und formalen Verifikationstechniken.

Die wichtigsten Beiträge dieser Dissertation sind (1) zwei neuartige Assertion-basierte Ansätze für die Integration von temporalen Eigenschaftsbeschreibungen in die Verifikation eingebetteter Software und (2) ein neuartiger semiformaler Verifikationsansatz, welcher im Vergleich zu rein simulationsbasierten Vorgehensweisen eine höhere Abdeckung der Verifikation erreicht. Die entwickelten Lösungen wurden anhand einer industriellen Anwendung aus dem Bereich der Automobilelektronik evaluiert.

Im Bereich simulationsbasierter Verifikationstechniken wurden zwei neuartige Ansätze identifiziert und untersucht, die eine effiziente Einbindung von Assertions in die Überprüfung eingebetteter Software ermöglichen: Zum einen wurde ein Hardware-Verifikationswerkzeug, der SystemC Temporal Checker (SCTC), um Schnittstellen zur Überwachung von Variablen und Funktionen eingebetteter Software innerhalb eines Mikroprozessor-Speicher-Modells erweitert. Zum anderen wurde ein Vorgehen aufgebaut, welches die Ableitung eines SystemC-Modells aus dem ursprünglichen C-Code beinhaltet und so eine direkte Integration in den SCTC ermöglicht. Der erste Ansatz ermöglicht es, temporale Eigenschaften in C-Programmen einfach unter realen Bedingungen zu überprüfen. Hierzu ist ein explizites Modell des Mikroprozessors erforderlich. Der zweite Ansatz erfordert die Generierung eines abstrakteren SystemC-Modells und ermöglicht so eine Reduzierung des Zeitaufwands für die Überprüfung.

Im Hinblick auf die Beschränkungen simulationsbasierter Ansätze wurde eine neuartige semiformale Verifikationsmethodik mit Bezeichnung SofTPaDS (Semiformal Verification of Temporal Properties in Hardware-Dependent Software) entwickelt. Dieser kombiniert Assertion-basierte und symbolische Simulationsstrategien für die Überprüfung von eingebetteter Software mit Hardware-Abhängigkeiten. Der Ansatz kombiniert eine simulationsbasierte Traversierung des Zustandsraums mit einer lokalen (zeitlich begrenzten) formalen Exploration einzelner Zustände. Das Vorgehen ermöglicht so eine tiefer gehende Untersuchung des Zustandsraums (verglichen zu heutigen Modellprüfungsverfahren) bei verbesserter Abdeckung der Verifikation (verglichen zu rein simulationsbasierten Verfahren).