Counterexample-Guided Interval Weakening

1. Problemstellung

Systeme, die in dynamischen Umgebungen operieren, erfahren häufig Leistungseinbußen (z. B. Hardwareausfälle, Ressourcenbeschränkungen), die ihre ursprünglichen Zeitgarantien ungültig machen, selbst wenn ihre funktionale Logik korrekt bleibt. Diese Zeitgarantien werden typischerweise mit Metric Temporal Logic (MTL) spezifiziert.

• Die Herausforderung: Wenn ein System degradiert, kann eine ideale MTL-Spezifikation (z. B. „Ankunft innerhalb von 30 Sekunden") nicht mehr erfüllt werden. Eine logisch schwächere Variante (z. B. „Ankunft innerhalb von 60 Sekunden") könnte jedoch immer noch erfüllt sein und nützlich sein.
• Die Lücke: Bestehende Methoden zur Spezifikationskorrektur konzentrieren sich oft auf nicht realisierbare Anforderungen (Finden irgendeiner Implementierung) oder verwenden heuristische, nicht-deterministische Ansätze (wie genetische Algorithmen), die keine Garantie für die stärkste mögliche Abschwächung bieten. Es fehlt an formalen, semantikgetriebenen Methoden, um automatisch die optimale (stärkste) abgeschwächte Intervallgrenze für ein spezifisches degradiertes Systemmodell abzuleiten.

2. Methodik: Der CEGIW-Algorithmus

Die Autoren schlagen CEGIW (Counterexample-Guided Interval Weakening) vor, einen iterativen Algorithmus, der die Zeitintervalle in MTL-Spezifikationen automatisch anpasst, um sicherzustellen, dass sie für ein gegebenes Systemmodell gelten.

Kernkonzepte

• Kontexte: Der Algorithmus behandelt die MTL-Formel als einen „Kontext" $C$ mit einem „Loch" $[-]$, in dem sich die spezifische Teilformel befindet, die das zu schwächende Intervall enthält. Dies ermöglicht es dem Algorithmus, die logische Struktur der ursprünglichen Spezifikation zu bewahren und nur die Intervallgrenzen zu modifizieren.
• Abschwächungsordnung:
  • Für den Until ($U$)-Operator entspricht die Abschwächung einer Erweiterung der rechten Intervallgrenze (mehr Zeit zulassen).
  • Für den Release ($R$)-Operator entspricht die Abschwächung einer Verkleinerung der rechten Intervallgrenze (weniger Zeit erforderlich).
  • Das Papier beweist, dass diese Modifikationen eine totale Ordnung erzeugen, was dem Algorithmus ermöglicht, eine eindeutige „optimale" Abschwächung zu identifizieren.

Algorithmusablauf

Der Algorithmus arbeitet auf zwei verschachtelten Ebenen:

1. Iterative Schleife (Oberste Ebene):

   • Ein Model Checker (speziell nuXmv) prüft, ob die aktuelle MTL-Eigenschaft auf dem Systemmodell gilt.
   • Wenn die Eigenschaft fehlschlägt, erzeugt der Model Checker eine Gegenbeispiel-Spur (speziell eine „Lasso-Spur", bestehend aus einem endlichen Präfix und einem sich wiederholenden Suffix).
   • Der Algorithmus ruft die Funktion Weaken auf, um das Intervall basierend auf diesem spezifischen Gegenbeispiel anzupassen.
   • Der Vorgang wird mit der neuen, abgeschwächten Eigenschaft wiederholt, bis die Eigenschaft auf dem Modell gilt oder keine gültige Abschwächung mehr existiert.

2. Abschwächung auf Gegenbeispielen (Untere Ebene):

   • Lasso-Abdeckung: Anstatt über unendliche Spuren zu iterieren, verwendet der Algorithmus ein „Abdeckungsintervall", um die Erfüllung über die unendliche Lasso-Spur nur mittels endlicher Berechnung zu bestimmen.
   • Rekursive Durchlauf: Die Funktion Weaken durchläuft den MTL-Kontext rekursiv.
     • Basisfälle: Berechnet direkt die minimale erforderliche Intervallerweiterung (für $U$) oder -verkleinerung (für $R$), um die spezifische Spur zu erfüllen.
     • Induktive Fälle: Leitet die Abschwächungsanforderungen den Syntaxbaum hinauf weiter. Wenn beispielsweise eine Teilformel der linke Operand eines $U$-Operators ist, muss der Algorithmus ein Intervall finden, das die Bedingung für alle Zeitschritte erfüllt, bis der rechte Operand wahr wird, und wählt das schwächste Intervall aus, das alle Anforderungen abdeckt.

3. Hauptbeiträge

• CEGIW-Algorithmus: Ein neuartiger, iterativer, gegenbeispielgeleiteter Algorithmus, der automatisch die stärkste mögliche Intervallabschwächung für MTL-Spezifikationen gegeben ein degradiertes Systemmodell ableitet.
• Formale Garantien: Die Autoren liefern rigorose Beweise für:
  • Korrektheit: Wenn der Algorithmus ein Intervall zurückgibt, gilt die abgeschwächte Eigenschaft auf dem System.
  • Optimalität: Das zurückgegebene Intervall ist die „stärkste" mögliche Abschwächung (d. h., kein strikt stärkeres Intervall würde das System erfüllen).
• Kontexterhaltung: Die Methode modifiziert nur die numerischen Grenzen von Intervallen, bewahrt die logische Struktur und Semantik der ursprünglichen Spezifikation, was entscheidend ist, um die Absicht sicherheitskritischer Anforderungen zu erhalten.
• Empirische Validierung: Der Ansatz wurde an realen Fallstudien unter Verwendung des FRET-Frameworks (Formal Requirements Elicitation Tool) getestet.

4. Ergebnisse und Evaluation

Die Autoren evaluierten CEGIW anhand zweier Forschungsfragen:

• FQ1: Diagnosefähigkeit (Fallstudie Sammelflugroboter):

  • Auf ein Schwarmroboter-Modell angewendet, identifizierte CEGIW zunächst einen Designfehler (eine Endlosschleife), bei dem keine Abschwächung existierte.
  • Nach der Korrektur des Modells leitete CEGIW erfolgreich die optimalen Zeitgrenzen ab: Erweiterung der „Zurück-zum-Start"-Zeit von 3 auf 20 Einheiten und Verkleinerung der „Auf Abstand bleiben"-Zeit von 20 auf 3 Einheiten.
  • Dies demonstriert die Fähigkeit von CEGIW, sowohl Modellierungsfehler zu diagnostizieren als auch die Systemresilienz zu quantifizieren.

• FQ2: Anwendbarkeit auf reale Anforderungen:

  • Analyse von 419 Anforderungen aus 8 realen Fallstudien (z. B. mechanische Lungenventilatoren, autonome Drohnen, Flugzeugsteuerungen).
  • Ergebnisse: 124 von 419 Anforderungen (ca. 30 %) waren für eine Intervallabschwächung geeignet.
  • Interpretation: 116 erforderten eine Intervallerweiterung (z. B. einer Kontrollschleife mehr Zeit aufgrund von Netzwerklatenz gewähren), und 11 erforderten eine Verkleinerung (z. B. muss ein Ventilator mindestens eine bestimmte Zeit eingeschaltet bleiben, sodass die untere Grenze verschärft wird).
  • Die Studie bestätigt, dass Intervallabschwächung ein praktisches Werkzeug für sicherheitskritische Domänen ist, in denen Degradation erwartet wird.

5. Bedeutung und zukünftige Arbeit

• Bedeutung: CEGIW schließt die Lücke zwischen formaler Verifikation und Systemdegradation. Es geht über eine einfache „Bestanden/Nicht bestanden"-Verifikation hinaus, um handlungsorientiertes, quantitatives Feedback darüber zu geben, wie stark die Leistung eines Systems degradieren kann, bevor seine Garantien versagen. Dies ist entscheidend für die Entwicklung resilienter sicherheitskritischer Systeme.
• Einschränkungen & zukünftige Arbeit:
  • Derzeit modifiziert der Algorithmus nur die rechte Intervallgrenze. Zukünftige Arbeiten zielen darauf ab, sowohl linke als auch rechte Grenzen zu behandeln, was eine partielle Ordnung einführt und die Definition von „Optimalität" kompliziert.
  • Derzeit wird nur ein Intervall gleichzeitig abgeschwächt. Geplante zukünftige Arbeiten beinhalten die Einbeziehung von Multi-Objective-Optimierung (Pareto-Optimalität), um mehrere Intervalle gleichzeitig zu schwächen.
  • Der Umfang ist derzeit auf Intervallmodifikationen beschränkt; zukünftige Forschung könnte syntaktische Änderungen an der Formelstruktur selbst untersuchen.

Zusammenfassend stellt das Papier ein robustes, mathematisch fundiertes Framework zur automatischen Reparatur von Zeitspezifikationen in degradierten Systemen vor und bietet Ingenieuren eine präzise Möglichkeit, Systemresilienz zu verstehen und zu quantifizieren.