Delayed Constraints in Narrowing for the Logic-Based Analyses of Real-Time Systems

Technische Zusammenfassung: Verzögerte Constraints beim Narrowing für die logikbasierte Analyse von Echtzeitsystemen

Problemstellung
Die formale Analyse von Echtzeitsystemen steht vor zwei primären Herausforderungen hinsichtlich der Unendlichkeit: dem Potenzial für eine unbeschränkte Anzahl von Agenten und Nachrichten sowie einem Zustandsraum, der aufgrund dichter Zeit unendlich ist. Traditionelle Verifikationsmethoden in der Rewriting Logic (RL), insbesondere jene, die in der Maude-Rewriting-Engine implementiert sind, waren historisch begrenzt. Während Maude die Invariantenverifikation für Systeme mit vollständig spezifizierten Komponenten (Ground-Terms) und SMT-Constraints unterstützt, stößt es bei Systemen mit einer unbekannten Anzahl von Agenten oder beliebigen Parametern an seine Grenzen. Zudem basierten frühere symbolische Techniken oft auf Zeitabtastungen (Time Sampling), was in Settings mit dichter Zeit weder korrekt noch vollständig ist. Bestehende Ansätze, die logische Variablen für unbeschränkte Agenten verwenden, führen oft zu Semi-Entscheidungsverfahren mit unendlichen Suchräumen, denen Mechanismen zur Garantie der Terminierung fehlen.

Methodik
Die Autoren schlagen einen neuartigen Verifikationsrahmen vor, der drei Kerntechniken integriert, um diese Einschränkungen zu adressieren:

1. Rewriting modulo SMT: Nutzung von SMT-Theorien für die symbolische Repräsentation von Zeitbeschränkungen.
2. Narrowing mit logischen Variablen: Einsatz von logischen Variablen, um über Systeme mit einer unbekannten oder beliebigen Anzahl von Agenten zu argumentieren.
3. Verzögerte Constraints und Folding: Einführung eines Constraint-Speichers über teilweise instanzierten Terms, inspiriert durch Constraint Logic Programming (CLP).

Die zentrale Innovation ist das Delayed Folding Narrowing. Im Gegensatz zum Standard-Narrowing erlaubt diese Methode, dass SMT-Ausdrücke in den Regelbedingungen „verzögerte“ Teile enthalten können – Teil-Ausdrücke, die nicht ausgewertet werden können, bis die Terms weiter instanziiert sind. Dies wird durch eine SMT-Erweiterung erreicht, bei der nicht-valide SMT-Ausdrücke (z. B. mte(t, T'), was eine maximale Zeitspanne repräsentiert) in frische Variablen abstrahiert werden. Diese Constraints werden akkumuliert und erst gelöst oder propagiert, wenn die Terms ausreichend instanziiert sind.

Der Rahmen definiert Logical Real-Time Rewrite Theories, welche Standard-Echtzeit-Rewriting-Theorien erweitern, um zu ermöglichen:

• Bedingungen in Rewrite-Regeln können SMT-Ausdrücke mit verzögerten Teilen enthalten.
• Die rechten Seiten (RHS) können Variablen enthalten, die nicht auf den linken Seiten (LHS) vorhanden sind.
• Abfragen (Queries) können gemeinsame Variablen in den Initial- und Zielzuständen enthalten.

Um die Terminierung zu gewährleisten, verwendet die Methode einen Folding-Mechanismus. Ein Zustandsgraph wird konstruiert, wobei ein symbolischer Zustand $v'$ entfernt wird, wenn er eine Instanz eines zuvor explorierten Zustands modulo der Äquivalenztheorie ist. Die Autoren beweisen, dass unter spezifischen Bedingungen (insbesondere durch eine sorgfältig entworfene Hierarchie von Sorts) diese Folding-Präordnung einen endlichen Suchraum gewährleistet und das Semi-Entscheidungsverfahren in ein Entscheidungsverfahren für die Invariantenverifikation transformiert.

Zentrale Beiträge

1. Delayed Folding Narrowing: Die Definition und Implementierung einer Narrowing-Relation, die erweiterte SMT-Ausdrücke mit verzögerten Constraints handhabt. Dies ermöglicht die Verifikation von Systemen mit beliebigen logischen und SMT-Variablen sowohl in der Initialkonfiguration als auch in der Invariante.
2. Verifikation des getimten Fischer-Protokolls: Das Paper präsentiert die erste automatische Verifikation der Korrektheit des getimten Fischer-Mutual-Exclusion-Protokolls in seinem allgemeinsten Setting. Dies umfasst eine beliebige Anzahl von Prozessen und beliebige Zeitparameter ($\gamma$ und $\delta$). Dies wurde durch das Design einer spezifischen Hierarchie von Sorts erreicht, um die Terminierung des Folding-Verfahrens zu garantieren, sowie durch die Nutzung logischer Variablen, um die unbestimmte Anzahl von Prozessen zu repräsentieren.
3. Controller-Synthese für das Dining Philosophers Problem: Der Rahmen wird auf ein getimtes Dining Philosophers Problem angewendet, um einen Controller (den „Lackey“) zu synthetisieren. Durch das Unspezifizieren der Übergänge des Controllers (repräsentiert durch logische Variablen) synthetisiert das Narrowing-Verfahren die fehlenden Übergänge, die erforderlich sind, um eine Erreichbarkeitseigenschaft zu erfüllen (z. B. dass bestimmte Philosophen vor einer Deadline in den Speisesaal eintreten).

Ergebnisse
Die Methode wurde als Erweiterung der Maude-Rewriting-Engine unter Verwendung von Meta-Level-Features implementiert.

• Fischer-Protokoll: Die Autoren verifizierten erfolgreich die Mutual Exclusion für eine beliebige Anzahl von Prozessen. Als der Initialzustand so eingeschränkt wurde, dass $\gamma > \delta$ galt, war der Suchraum durch Folding endlich (er bestand aus nur 3 Zuständen), und das Tool bestätigte, dass kein erreichbarer Zustand die Invariante verletzt. Im Gegensatz dazu wurde bei $\delta \ge \gamma$ ein Gegenbeispiel gefunden.
• Dining Philosophers: Das System synthetisierte erfolgreich einen Lackey-Automaten, der es bestimmten Philosophen ermöglichte, den Speisesaal zu betreten. Die Ausgabe lieferte eine konkrete Menge an Übergängen und Lokalitäten für den Controller und demonstrierte damit die Fähigkeit des Rahmens zu Syntheseaufgaben.
• Effizienz: Der Folding-Mechanismus reduzierte den Suchraum signifikant und ermöglichte die Analyse von Systemen, die aufgrund unendlicher Zustandsräume andernfalls unhandhabbar gewesen wären.

Bedeutung und Ansprüche
Das Paper beansprucht, eine sounde und expressive Basis für die symbolische Verifikation von Real-Time Rewrite Theories zu liefern. Seine Bedeutung liegt in der Überbrückung der Lücke zwischen der Expressivität der Logikprogrammierung (Umgang mit unbeschränkten Agenten via logischer Variablen) und der Präzision der Echtzeitanalyse (Umgang mit dichter Zeit via SMT und verzögerten Constraints).

Die Autoren betonen, dass ihr Ansatz über das „Standard“-Maude und bestehende Tools für Parametric Timed Automata (PTA) hinausgeht, die typischerweise eine feste Anzahl von Prozessen oder feste Zeitgrenzen erfordern. Durch die Unterstützung beliebiger Parameter und einer unbeschränkten Anzahl von Agenten innerhalb eines einzigen Rahmens bietet die Methode einen einheitlichen Ansatz zur Analyse komplexer Echtzeitmodelle, einschließlich der Synthese fehlender Systemkomponenten. Die Arbeit legt nahe, dass verzögerte Constraints ein entscheidender Mechanismus sind, um die Terminierung in symbolischen Analysen von unendlichen Zustands-Echtzeitsystemen zu erreichen.