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

Technische Samenvatting: Vertraagde Constraints in Narrowing voor de Logica-gebaseerde Analyses van Real-Time Systemen

Probleemstelling
De formele analyse van real-time systemen staat voor twee primaire uitdagingen met betrekking tot oneindigheid: het potentieel voor een onbegrensd aantal agenten en berichten, en een toestandsruimte die oneindig is door dichte tijd. Traditionele verificatiemethoden in Rewriting Logic (RL), met name die geïmplementeerd in de Maude rewriting engine, zijn historisch beperkt geweest. Hoewel Maude support biedt voor invariant-verificatie voor systemen met volledig gespecificeerde componenten (ground terms) en SMT-constraints, heeft het moeite met systemen die een onbekend aantal agenten of willekeurige parameters bevatten. Bovendien vertoonden eerdere symbolische technieken vaak afhankelijkheid van tijdssampling, wat in dichte tijd-settings gebrek aan soundheid en volledigheid oplevert. Bestaande benaderingen die gebruikmaken van logische variabelen voor onbegrensde agenten resulteren vaak in semi-beslissingsprocedures met oneindige zoekruimtes, waarbij mechanismen ontbreken om terminatie te garanderen.

Methodologie
De auteurs stellen een nieuw verificatiekader voor dat drie kerntechnieken integreert om deze beperkingen aan te pakken:

1. Rewriting Modulo SMT: Het gebruik van SMT-theorieën voor de symbolische representatie van timing-constraints.
2. Narrowing met Logische Variabelen: Het inzetten van logische variabelen om te redeneren over systemen met een onbekend of willekeurig aantal agenten.
3. Vertraagde Constraints en Folding: Het introduceren van een constraint store over gedeeltelijk geïnstantieerde termen, geïnspireerd door Constraint Logic Programming (CLP).

De kerninnovatie is Delayed Folding Narrowing. In tegenstelling tot standaard narrowing, staat deze methode toe dat SMT-expressies in regelvoorwaarden "vertraagde" delen bevatten—sub-expressies die niet geëvalueerd kunnen worden totdat de termen verder geïnstantieerd zijn. Dit wordt bereikt door een SMT Extension waarbij niet-geldige SMT-expressies (bijv. mte(t, T') dat een maximale tijdverloop representeert) worden geabstraheerd naar verse variabelen. Deze constraints worden geaccumuleerd en pas opgelost of gepropageerd zodra de termen voldoende geïnstantieerd zijn.

Het kader definieert Logical Real-Time Rewrite Theories, die standaard real-time rewrite theories uitbreiden om het volgende mogelijk te maken:

• Voorwaarden in rewrite rules die SMT-expressies met vertraagde delen bevatten.
• Rechterzijden (RHS) die variabelen bevatten die niet aanwezig zijn in de linkerzijde (LHS).
• Queries die gedeelde variabelen bevatten in initiële en doeltoestanden.

Om terminatie te waarborgen, maakt de methode gebruik van een folding mechanism. Een toestandsgraaf wordt geconstrueerd waarbij een symbolische toestand $v'$ wordt verwijderd als deze een instantie is van een eerder verkende toestand modulo de equivalentietheorie. De auteurs bewijzen dat onder specifieke condities (met name een zorgvuldig ontworpen hiërarchie van sorts), deze folding preorder een eindige zoekruimte garandeert, waardoor de semi-beslissingsprocedure wordt getransformeerd in een beslissingsprocedure voor invariant-verificatie.

Belangrijkste Bijdragen

1. Delayed Folding Narrowing: De definitie en implementatie van een narrowing-relatie die uitgebreide SMT-expressies met vertraagde constraints afhandelt. Dit maakt de verificatie van systemen met willekeurige logische en SMT-variabelen in zowel de initiële configuratie als de invariant mogelijk.
2. Verificatie van het getimede Fischer Protocol: Het artikel presenteert de eerste automatische verificatie van de correctheid van het getimede Fischer mutual exclusion protocol in zijn meest algemene setting. Dit omvat een willekeurig aantal processen en willekeurige getimede parameters ($\gamma$ en $\delta$). Dit werd bereikt door een specifieke hiërarchie van sorts te ontwerpen om de terminatie van de folding procedure te garanderen en door logische variabelen te gebruiken om het ongespecificeerde aantal processen te representeren.
3. Controller Synthese voor Dining Philosophers: Het kader wordt toegepast op een getimed dining philosophers probleem om een controller (de "lackey") te synthetiseren. Door de transities van de controller ongespecificeerd te laten (gerepresenteerd door logische variabelen), synthetiseert de narrowing procedure de ontbrekende transities die nodig zijn om een reachability property te voldoen (bijv. specifieke filosofen die de eetkamer binnenkomen vóór een deadline).

Resultaten
De methode is geïmplementeerd als een extensie van de Maude rewriting engine met behulp van meta-level features.

• Fischer Protocol: De auteurs hebben succesvol mutual exclusion geverifieerd voor een willekeurig aantal processen. Wanneer de initiële toestand geconstraint was zodanig dat $\gamma > \delta$, was de zoekruimte eindig (bevatnd slechts 3 toestanden door folding), en het instrument bevestigde dat geen enkele bereikbare toestand de invariant schond. Omgekeerd, wanneer $\delta \ge \gamma$, werd een tegenvoorbeeld gevonden.
• Dining Philosophers: Het systeem heeft succesvol een lackey-automaat gesynthetiseerd die specifieke filosofen de eetkamer liet betreden. De output leverde een concrete set transities en locaties voor de controller, wat de capaciteit van het framework demonstreert om synthese-taken aan te kunnen.
• Efficiëntie: Het folding mechanisme heeft de zoekruimte aanzienlijk verkleind, waardoor de analyse van systemen mogelijk werd die anders onhandelbaar zouden zijn vanwege oneindige toestandsruimtes.

Betekenis en Claims
Het artikel claimt een sound en expressief fundament te bieden voor de symbolische verificatie van real-time rewrite theories. De significantie ligt in het overbruggen van de kloof tussen de expressiviteit van logische programmering (het afhandelen van onbegrensde agenten via logische variabelen) en de precisie van real-time analyse (het afhandelen van dichte tijd via SMT en vertraagde constraints).

De auteurs benadrukken dat hun aanpak verder gaat dan "standaard" Maude en bestaande tools voor Parametric Timed Automata (PTA), die doorgaans een vast aantal processen of vaste tijdbounds vereisen. Door het ondersteunen van willekeurige parameters en een onbegrensd aantal agenten binnen één enkel kader, biedt de methode een uniforme aanpak voor het analyseren van complexe real-time modellen, inclus\n_bijvoorbeeld de synthese van ontbrekende systeemcomponenten. Het werk suggereert dat vertraagde constraints een cruciaal mechanisme zijn om terminatie te bereiken in symbolische analyses van oneindige-toestand real-time systemen.