(AP3) Runtime-Verification

Ursachen von Fehlern lassen sich entsprechend der Häufigkeit und der Reproduzierbarkeit der resultierenden Fehlfunktion in deterministisch und nichtdeterministisch aktivierbare Defekte unterteilen. Das Erkennen und Beseitigen deterministisch auftretender Fehler ist ein weitgehend gelöstes Problem, die zugrundeliegenden Defekte können mit geeigneten Teststrategien (z.B. Unit-Tests) erkannt, verstanden und beseitigt werden.

infektionen

Anders ist die Situation bei nicht-deterministisch auftretenden Fehlfunktionen (Mandelbugs, in Anspielung auf die Mandelbrot-Menge). Hierbei handelt es sich um chaotische und nichtdeterministisch erscheinende komplexe Fehlfunktionen, deren rationale Ursache nicht immer gefunden werden kann.

Die Komplexität von Mandelbugs kann folgende Ursachen haben:

  • Zeitverlauf zwischen Aktivierung eines Defekts und dem beobachteten Fehlverhalten
  • Fehlerhafte Werte/ Programmzustände werden zwischenzeitlich überschrieben
  • Einfluss indirekter Faktoren, zum Beispiel:
    • Interaktionen von Software mit der system-internen Umgebung (Hardware, Betriebssystem, andere Anwendungen)
    • Einfluss des Zeitverhaltens von Eingaben und Operationen (relativ zueinander oder in Bezug auf die Systemzeit)
    • Einfluss der Reihenfolge von Operationen
    • Einfluss des Beobachtungsvorgangs

Mandelbugs lassen sich mit Tests nur schwer erkennen und treten teilweise erst lange nach dem Release einer Software auf. Erschwerend kommt hier noch hinzu, dass ein falscher Wert zwischenzeitlich wieder überschrieben werden kann und damit die ursprüngliche Infektion nicht mehr nachverfolgbar ist. Die Häufigkeit von nach einem Software-Release gefundenen Mandelbug variiert stark und wird in der Literatur mit Werten von 15% bis 80% angegeben.

Das Auffinden der Ursachen von nichtdeterministisch aktivierten Defekten kann ein äußerst zeitintensiver Prozess sein, der sich teilweise über Jahre hinzieht bzw. auch erfolglos bleiben kann. Mit der zunehmenden Einführung von Multicore-SoCs ist zu erwarten, dass die Anzahl der nichtdeterministisch auftretenden Fehlfunktionen überproportional zunimmt.

Projektziel

Runtime-Verification ist eine recht neue Verifikationstechnik, bei der formal spezifizierte Eigenschaften zur Laufzeit eines Systems überprüft werden. Üblicherweise wird für die formal spezifizierte Eigenschaft ein sogenannter Monitor synthetisiert, der das zugrunde liegende System hinsichtlich der Korrektheitseigenschaft zur Laufzeit überwacht. Die Verwendung eines abstrakten Spezifikationsformalismus zusammen mit einer automatischen Synthese führt zu einer hohen Qualität der Überwachung, da es typischerweise leichter ist, eine Korrektheitseigenschaft abstrakter zu beschreiben, als eine Implementierung für die Überwachung der Korrektheitseigenschaft anzugeben.

In der Runtime-Verification werden bislang vorwiegend Softwarelösungen propagiert. Dazu wird typischerweise das zugrunde liegende Programm mit Annotationen versehen, die interessante atomare Eigenschaften des Programms nach außen sichtbar machen. Die Sequenz dieser atomaren Eigenschaften wird dann verwendet, um mit Hilfe eines synthetisierten Monitors eine komplexere Korrektheitseigenschaft zu überprüfen. Diese Vorgehensweise eignet sich für eine Vielzahl von typischen Softwaresystemen, hat aber für zeitkritische eingebettete Systeme, gerade wenn sie im Kontext von sicherheitskritischen Anwendungen verwendet werden, den Nachteil des erhöhten Ressourcen-Verbrauchs (Zeit, Speicher).

Ziel des Projektes CONIRAS ist es daher, hardware-unterstützt mit Hilfe der Methoden der Runtime-Verification die kontinuierliche Untersuchung und Überwachung von Systemzuständen eines SoCs ohne erhöhten Ressourcen-Verbrauch zu ermöglichen. Damit wird dem Anwender ein neuartiges und sehr mächtiges Werkzeug zur Verfügung gestellt, welches ihn bei der systematischen Suche und der Analyse nichtdeterministisch auftretender Fehlfunktionen unterstützt und somit einen wesentlichen Beitrag zur Verbesserung der Zuverlässigkeit von Software leistet.