[Back]

A. Hagmann:
"Performance Aware Hardware Runtime Monitors";
Supervisor: A. Steininger; Institut für Technische Informatik, 2013.

Due to the complexity of today´s computer systems, (automated) testing and verification are
integral parts of their development process. The field of research for runtime verification deals
with lightweight verification methods, which are classified between common testing methods
and formal verification. In a runtime verification setting, the system under test is observed by
a runtime monitor that checks the monitored behaviour against a specification. Beside testing,
runtime verification may be used in the field to add self-checking capabilities to a system.
Based on existing approaches, this thesis presents a runtime verification framework, capable
of observing embedded real-time systems. The proposed framework features a runtime monitoring
unit, implemented as a micro-processor architecture. The monitoring unit is built entirely in
hardware and may be used stand-alone or integrated, as IP-core, in the target system. It evaluates
claims, specified as atomic propositions and temporal logic formulas, where Linear Temporal
Logic and Metric Temporal Logic are supported. The connection to the system under test is
established by wire-taping its external interfaces.
After an introduction to runtime verification methods, this thesis captures the state-of-theart
and provides theoretical background, covering temporal logics and observer algorithms. It
proceeds with an analysis of existing parts and proposes optimizations on them. Thereby, the
influence of different improvements is compared and verified by benchmarks, conducted with a
software model of the runtime verification unit. Furthermore, the runtime verification framework
is extended to support natively the evaluation of future time temporal formulas. A prototype
implementation, targeting a Field Programmable Gate Array (FPGA), shows the feasibility of
the novel approach. The design of the runtime verification unit is done with special focus on not
influencing the behaviour of the system under test and getting along with the limited resources
available within embedded systems.
Benchmark results compare the improved runtime verification unit to the existing design
and show a speed up factor of twelve. Synthesis runs are used to discuss the scalability of the
FPGA implementation and show, that the proposed design fits well into a low-end commercial
off-the-shelf FPGA. A case study completes this thesis and uses the prototype implementation
in a real-world scenario. It demonstrates the benefit of a runtime verification unit within an
Unmanned Aerial System (UAS) to detect erroneous sensor readings.

Aufgrund der Komplexität aktueller Computersysteme sind (automatisierte) Test- und Verifikationsmethoden
wichtige Bestandteile der Produktentwicklung. Das Forschungsgebiet der Laufzeitverifikation
untersucht Testmethoden, die zwischen klassischem Testen und formaler Verifikation
angesiedelt sind. Dabei wird das zu testende System während der Laufzeit von einem
Observer gegen eine vorgegebene Spezifikation geprüft. Neben dem Testen können Methoden
der Laufzeitverifikation auch permanent in einem System angewandt werden, um es mit Selbstüberprüfungsmechanismen
auszustatten.
Diese Diplomarbeit präsentiert, aufbauend auf einem existierenden Prototypen, ein Framework
zur Laufzeitverifikation, das speziell für eingebettete System entworfen wurde. Der Observer
dieses Frameworks basiert auf einer Mikroprozessorarchitektur und ist vollständig in Hardware
implementiert. Diese Einheit kann über externe Schnittstellen an das zu prüfende System
angeschlossen oder vollständig in das Zielsystem eingebunden werden. Um das erwartete Verhalten
des zu prüfenden Systems zu spezifizieren, werden atomare Aussagen und die temporalen
Logiken LTL (Linear Temporal Logic) und MTL (Metric Temporal Logic) verwendet.
In dieser Diplomarbeit werden, nach einer Einführung in die Laufzeitverifikation, der Stand
der Technik und theoretische Hintergründe erläutert. Dabei werden die verwendeten temporalen
Logiken und Observer Algorithmen näher behandelt. Danach werden existierende Teile des
Frameworks analysiert und Verbesserungen vorgeschlagen. Die Einflüsse verschiedener Optimierungsschritte
werden mit Hilfe von Benchmarks, die in einer Software basierten Simulationsumgebung
ausgeführt werden, untersucht. Weiters wird das Framework so erweitert, dass
auch Aussagen über zukünftige Ereignisse ausgewertet werden können. Um die Realisierbarkeit
der Optimierungen und Erweiterungen zu zeigen, werden diese in einer FPGA-Implementierung
(Field Programable Gate Array) angewandt. Beim Entwurf des Frameworks wird speziell darauf
geachtet, dass durch dessen Einsatz das zu testende System nicht beeinflusst wird. Weiters
muss die Implementierung mit den in eingebetteten Systemen nur beschränkt zur Verfügung
stehenden Ressourcen auskommen.
Durch die Optimierungen am Framework konnte die Geschwindigkeit des Observers, gegenüber
dem bestehenden Prototypen, verzwölffacht werden. Syntheseergebnisse zeigen die Skalierbarkeit
der FPGA-Implementierung und den möglichen Einsatz in handelsüblichen FPGAs.
Zum Schluss zeigt ein Fallbeispiel die Anwendung des Laufzeitverifikationssystems an einem
unbemannten Flugzeug. Dabei konnte erfolgreich der Ausfall eines Sensors detektiert werden.

Project Head Andreas Steininger:
Framework für CounterExample Validierung und Testfallgenerierung für die Verifikation von eingebetteter Software