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.<br />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.<br />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.<br />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.<br />Durch die Optimierungen am Framework konnte die Geschwindigkeit des Observers, gegenüber dem bestehenden Prototypen, verzwölffacht werden.<br />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.<br />
de
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.<br />Based on existing approaches, this thesis presents a runtime verification framework, capable of observing embedded real-time systems.<br />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.<br />After an introduction to runtime verification methods, this thesis captures the state-of-the- art 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.<br />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.<br />
