PolyVer: Ein kompositorischer Ansatz zur Modellierung und Verifikation polyglotter Systeme

Grundlegende Informationen

• Papier-ID: 2503.03207
• Titel: PolyVer: A Compositional Approach for Polyglot System Modeling and Verification
• Autoren: Pei-Wei Chen, Shaokai Lin, Adwait Godbole, Ramneet Singh, Elizabeth Polgreen, Edward A. Lee, Sanjit A. Seshia
• Klassifizierung: cs.PL (Programmiersprachen)
• Veröffentlichungszeit/Konferenz: Formal Methods in Computer-Aided Design 2025
• Papierlink: https://arxiv.org/abs/2503.03207

Zusammenfassung

Polyglotte Softwaresysteme bestehen aus Programmen, die in mehreren Programmiersprachen implementiert sind. Allerdings sind bestehende Programmverifizierungswerkzeuge typischerweise nur für einzelne Sprachen konzipiert. Um polyglotte Systeme zu verifizieren, müssen diese normalerweise in eine universelle Verifikationssprache oder formale Darstellung übersetzt werden. Dieses Papier stellt PolyVer vor – einen alternativen Ansatz, der Abstraktion, kompositorisches Schließen und Synthesetechniken nutzt, um die Verifikation polyglotter Systeme direkt durchzuführen. PolyVer modelliert polyglotte Systeme als formale Modelle von Transitionssystemen, wobei die transitionsrelevanten Aktualisierungsfunktionen in Zielsprachen (wie C oder Rust) implementiert sind. Zur Durchführung der Verifikation verbindet PolyVer einen Modellprüfer für Transitionssysteme mit sprachspezifischen Verifikationswerkzeugen durch Vorbedingung/Nachbedingung-Verträge der Aktualisierungsfunktionen. Diese Verträge werden automatisch durch syntaxgesteuerte Synthese oder Synthese basierend auf großen Sprachmodellen generiert und von sprachspezifischen Verifikationswerkzeugen überprüft.

Forschungshintergrund und Motivation

Problemdefinition

Moderne Softwaresysteme verwenden zunehmend polyglotte Architekturen. Frameworks wie ROS2 und Lingua Franca ermöglichen es Entwicklern, die am besten geeignete Programmiersprache für verschiedene Komponenten auszuwählen. Diese Flexibilität bringt jedoch Verifikationsherausforderungen mit sich:

1. Unterschiede in der Sprachsemantik: Verschiedene Programmiersprachen haben unterschiedliche Syntax und Semantik. Beispielsweise sättigt Rusts saturating_add-Funktion bei Überläufen auf den Maximalwert, während die Addition in C zu Umbruch führen kann.
2. Einschränkungen bestehender Verifizierungswerkzeuge: Die meisten Programmverifizierungswerkzeuge (wie CBMC für C, Kani für Rust) sind speziell für einzelne Sprachen konzipiert und können polyglotte Systeme nicht direkt verarbeiten.
3. Komplexität der Übersetzung: Die Übersetzung eines gesamten polyglotten Systems in eine einzelne Verifikationssprache erfordert die Unterstützung der vollständigen Syntax und Semantik aller Sprachen, was für moderne Sprachen prohibitiv ist.

Forschungsbedeutung

Die zunehmende Komplexität polyglotter Systeme erhöht das Risiko von Softwarefehlern. In sicherheitskritischen Bereichen (wie autonomes Fahren, Luft- und Raumfahrt) sind die starken Garantien erforderlich, die formale Verifikation bietet, nicht nur unvollständige Methoden wie Tests.

Einschränkungen bestehender Ansätze

• Monolithische Übersetzungsmethoden: Erfordern die Entwicklung einer vollständigen Compiler-Infrastruktur für jede Sprache
• Schwierigkeiten bei der Semantikbewahrung: Schwierig, alle sprachspezifischen Konstrukte der Quellsprache in der Zielverifikationssprache treu zu erfassen
• Skalierungsprobleme: Die generierten Verifikationsprobleme können zu groß werden

Kernbeiträge

1. Formalisierung des polyglotten Verifikationsproblems: Erstmalige systematische Formalisierung des polyglotten Verifikationsproblems und Vorschlag einer kompositorischen Lösung, die mehrere sprachspezifische Verifizierungswerkzeuge integriert.
2. Automatisierte Vertragssynthese: Vorschlag einer Methode zur automatischen Synthese und Verfeinerung von Vorbedingung/Nachbedingung-Verträgen unter Verwendung einer Zwischensprache und CEGIS-CEGAR-Schleifen, mit Unterstützung für syntaxgesteuerte Synthese und große Sprachmodelle als Syntheseorakel.
3. Werkzeugimplementierung: Implementierung des PolyVer-Werkzeugs basierend auf UCLID5 mit Unterstützung für C und Rust durch CBMC- und Kani-Verifizierungswerkzeuge. Nachweis, dass LLM-basierte Syntheseorakel symbolische Synthesemethoden übertreffen.
4. Fallstudien und Bewertung: Entwicklung eines Verifizierungswerkzeugs für die Lingua-Franca-Koordinationssprache mit Verifikation polyglotter Systeme mit C- und Rust-Prozessen sowie C-Sprachfragmenten, die von früheren Arbeiten nicht unterstützt wurden.

Detaillierte Methodenbeschreibung

Aufgabendefinition

Eingabe: Polyglottesmodell M = (Q,V,I₀,T,F) und Systemeigenschaft φ Ausgabe: Verifikationsergebnis (Bestanden/Fehlgeschlagen) und möglicherweise eine Gegenbeispieltrasse Ziel: Bestimmung, ob M ⊨ φ gilt

Wobei:

• Q: Menge von Modi
• V: Menge typisierter Variablen
• I₀: Menge von Initialzuständen
• T: Menge von Modusübergängen
• F: Menge von Prozessen

Modellarchitektur

1. Erweiterter Zustandsautomat (ESM)

PolyVer modelliert polyglotte Systeme als erweiterte Zustandsautomaten, wobei:

• Zustände aus Modi und Variablenzuweisungen bestehen
• Übergänge mit Schutzbedinungen und Aktualisierungsrelationen verknüpft sind
• Aktualisierungsrelationen zu Prozessaufrufssequenzen spezialisiert sind

2. Zwischenvertragssprache L*

Die Schlüsselinnovation ist die Einführung einer Zwischensprache L* als "Klebstoff" zwischen verschiedenen Sprachen:

• Verträge werden in L* geschrieben
• Werden durch semantikbewahrende Kompilation compL in konkrete Sprachen transformiert
• Vermeidet die Komplexität vollständiger Sprachübersetzung

3. Hybride CEGIS-CEGAR-Methode

Der Algorithmus-Kern ist eine zweischichtige iterative Schleife:

Äußere CEGAR-Schleife:

1. Konstruktion eines abstrakten Modells M' mit aktuellen Verträgen
2. Modellprüfer verifiziert M' ⊨ φ
3. Bei Fehlschlag wird überprüft, ob das Gegenbeispiel falsch ist
4. Bei falschem Gegenbeispiel wird der Vertrag verfeinert; andernfalls wird ein echtes Gegenbeispiel gemeldet

Innere CEGIS-Schleife:

1. Syntheseorakel generiert Kandidatenverträge
2. Verifikationsorakel überprüft Vertragsgültigkeit
3. Bei Ungültigkeit werden positive Beispiele hinzugefügt und neu synthetisiert

Technische Innovationen

1. Kompositorische Verifikationsstrategie

Im Gegensatz zu monolithischen Übersetzungen verfolgt PolyVer eine "Teile-und-herrsche"-Strategie:

• Verwendung von Vertragsabstraktion für einzelne Prozesse
• Sprachspezifische Verifizierungswerkzeuge überprüfen Vertragsgültigkeit
• Modellprüfer verifiziert Systemeigenschaften

2. Automatisierte Vertragsgenerierung

Unterstützung mehrerer Syntheseorakel:

• LLM-basierter Synthesizer: Verwendet Gedankenketten-Prompting und Python-DSL
• SyGuS/SyMO-Synthesizer: Kodiert Probleme als Beispielprogrammieraufgaben

3. Falschheitsprüfung

Überprüfung der Erreichbarkeit von Gegenbeispieltrassen durch Verifikation von {V = d} C {V' ≠ d'}, um echte Gegenbeispiele von falschen zu unterscheiden.

Experimentelle Einrichtung

Datensatz

1. LFVerifier-Benchmark: 22 Lingua-Franca-Programme mit eingeschränkter C-Syntax
2. Vollständige LF-Beispiele: LED-Steuerung, Klettroboter, Satellitenlageregelungssysteme und andere eingebettete Systeme
3. Polyglotte Systeme: C/Rust-gemischte LF-Programme, ROS2-Anwendungen, FFI-Aufrufe zwischen Sprachen

Bewertungsmetriken

• Anzahl der Syntheseiterationen (IS: CEGIS-Iterationen, AR: CEGAR-Iterationen)
• Laufzeit (SOT: Syntheseorakelzeit, VOT: Verifikationsorakelzeit, UT: UCLID5-Zeit)
• Verifikationserfolgsquote

Vergleichsmethoden

Vergleich mit LFVerifier15, dem einzigen bekannten End-to-End-Automatisierungswerkzeug für LF-Programmverifikation.

Implementierungsdetails

• Verwendung von OpenAI o1-mini als LLM-Synthesizer mit 3 parallelen Abfragen pro Prozess
• CBMC-6.3.1, Kani-0.56.0, z3-4.8.7 als Verifikations-Backends
• 3,7-GHz-Intel-Core-i9-Maschine mit 62 GB RAM

Experimentelle Ergebnisse

Hauptergebnisse

RQ1: Vergleich mit bestehenden LF-Verifikationsarbeiten

Bei 22 Benchmark-Tests:

• PolyVer verifiziert erfolgreich alle Benchmarks, LFVerifier kann das TrafficLight-Beispiel nicht verifizieren
• 18 Benchmarks synthetisieren Verträge korrekt in einer einzelnen CEGIS-Schleife, durchschnittlich 37 Sekunden
• Obwohl die Gesamtlaufzeit langsamer ist (hauptsächlich durch Vertragssynthesiszeit dominiert), bietet sie erhebliche qualitative Verbesserungen

RQ2: Verarbeitung vollständiger LF-Beispiele

Erfolgreiche Verifikation eingebetteter Systeme mit vollständigem C-Code:

• LED-Steuerung: 1 Prozess, 123 Zeilen C-Code, 31,0 Sekunden Synthesiszeit
• Klettroboter: 12 Prozesse, 75 Zeilen C/Rust-Code, 685,4 Sekunden Synthesiszeit
• Satellitensteuerung: 6 Prozesse, 424 Zeilen C-Code, 729,0 Sekunden Synthesiszeit

RQ3: Verifikation polyglotter Systeme

Verifikation echter polyglotter Systeme:

• C/Rust-gemischte LF-Programme
• ROS2-Serviceanwendungen
• FFI-Aufrufe zwischen Sprachen

Wichtige Erkenntnisse

1. LLM übertrifft symbolische Methoden: SyGuS/SyMO-Solver erfordern viele CEGAR-Iterationen und terminieren oft nicht
2. Herausforderungen der Vertragssynthese: Prozesse mit komplexem Kontrollfluss und Datenabhängigkeiten erfordern mehr Iterationen
3. Praktische Validierung: Kann echte Implementierungscode verarbeiten, nicht nur Spielzeugbeispiele

Verwandte Arbeiten

Verifikation polyglotter Systeme

• Manuelle Übersetzungsmethoden: Cook et al. übersetzten Assembler-Code in C zur Verifikation des Xen-Hypervisors
• Automatische Fragmentübersetzung: LFVerifier übersetzt automatisch C-Fragmente in Verifikationssprachen
• Black-Box-Methoden: Inferieren Zusammenfassungen aus Ein-/Ausgabeverhalten

Kompositorische Verifikation

• Kompositorische Verifikation basierend auf Hoare-Logik wird weit verbreitet bei großen einsprachigen Programmen angewendet
• Verwendung von abstrakter Interpretation und CEGAR zur Automatisierung des Lernens von Vor-/Nachbedingungen

Vertragsableitung

• Eigenschaftsgesteuerte Vertragsableitungsmethoden
• Constraint-Horn-Clause-Solver
• Jüngste Anwendungen von LLMs beim Spezifikationslernen

Schlussfolgerung und Diskussion

Hauptschlussfolgerungen

1. PolyVer löst erfolgreich die Schlüsselherausforderungen der Verifikation polyglotter Systeme
2. Der kompositorische Ansatz vermeidet die Komplexität vollständiger Sprachübersetzung
3. Automatisierte Vertragssynthese macht die Methode praktisch
4. LLM-basierte Synthesizer übertreffen traditionelle symbolische Methoden

Einschränkungen

1. Terminierung: Der Algorithmus garantiert keine Terminierung und hängt von der Qualität des Syntheseorakels ab
2. Sprachunterstützung: Unterstützt derzeit nur C und Rust; andere Sprachen erfordern die Entwicklung von Verifikationsorakeln
3. Ausdruckskraft von Verträgen: Die Ausdruckskraft der Zwischensprache L* begrenzt die Komplexität verifizierbarer Eigenschaften
4. Skalierbarkeit: Die Vertragssynthesiszeit für große Systeme kann zum Engpass werden

Zukünftige Richtungen

1. Erweiterung auf andere polyglotte verteilte Softwaresysteme und Robotersoftwaresysteme
2. Anwendung auf formale Verifikation von Codeübersetzungen (z. B. C-zu-Rust-Übersetzungen)
3. Verbesserung der Effizienz und Genauigkeit der Vertragssynthese
4. Unterstützung für komplexere temporale Logik-Eigenschaften

Tiefgreifende Bewertung

Stärken

1. Problemwichtigkeit: Verifikation polyglotter Systeme ist ein praktisches und wichtiges Problem
2. Methodische Innovation: Die Kombination aus kompositorischer Verifikation und automatischer Vertragssynthese ist neuartig
3. Theoretische Grundlagen: Formale Definitionen sind klar, Korrektheitszusicherungen sind explizit
4. Praktischer Wert: Kann echte Systeme verarbeiten, nicht nur Spielzeugbeispiele
5. Werkzeugimplementierung: Bietet eine einsatzfähige Werkzeugimplementierung

Mängel

1. Leistungsaufwand: Die Vertragssynthesiszeit ist erheblich und könnte praktische Anwendungen einschränken
2. Sprachabdeckung: Unterstützt derzeit nur C und Rust; Erweiterbarkeit muss noch verifiziert werden
3. Begrenzte Benchmarks: Obwohl echte Beispiele enthalten, sind die Größen relativ klein
4. LLM-Abhängigkeit: Abhängigkeit von kommerziellen LLM-Diensten könnte die Reproduzierbarkeit beeinträchtigen

Auswirkungen

1. Akademischer Beitrag: Eröffnet eine neue Forschungsrichtung für die Verifikation polyglotter Systeme
2. Praktischer Wert: Bietet Verifikationswerkzeuge für sicherheitskritische polyglotte Systeme
3. Technische Inspiration: Die Idee von Verträgen als Schnittstellen zwischen Sprachen hat universellen Wert

Anwendungsszenarien

1. Eingebettete Systeme: Echtzeitsysteme mit gemischtem C/Rust
2. Verteilte Systeme: ROS2, gRPC und andere polyglotte Frameworks
3. Sicherheitskritische Anwendungen: Systeme, die formale Verifikationszusicherungen erfordern
4. Integration von Altsystemen: Systeme mit gemischtem altem und neuem Code

Literaturverzeichnis

Das Papier zitiert 50 relevante Arbeiten, die wichtige Arbeiten in mehreren Bereichen abdecken – polyglotte Systeme, formale Verifikation, Vertragsableitung, syntaxgesteuerte Synthese – und bietet eine solide theoretische Grundlage für die Forschung.

Gesamtbewertung: Dies ist ein hochqualitatives Systemforschungspapier, das ein wichtiges und praktisches Problem löst. Die Methode ist innovativ, die Experimente umfassend und die Werkzeugimplementierung vollständig. Obwohl es Raum für Verbesserungen bei Leistung und Skalierbarkeit gibt, leistet es einen wichtigen Beitrag zum Bereich der Verifikation polyglotter Systeme.