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

Sintesi Tecnica: Vincoli Ritardati nel Narrowing per le Analisi Logiche di Sistemi Real-Time

Enunciato del Problema
L'analisi formale dei sistemi real-time affronta due sfide primarie riguardanti l'infinità: la potenziale presenza di un numero illimitato di agenti e messaggi, e uno spazio di stato infinito a causa del tempo denso. I metodi di verifica tradizionali nella Logica di Riscrittura (RL), in particolare quelli implementati nel motore di riscrittura Maude, sono stati storicamente limitati. Sebbene Maude supporti la verifica degli invarianti per sistemi con componenti completamente specificati (termini ground) e vincoli SMT, fatica con sistemi contenenti un numero ignoto di agenti o parametri arbitrari. Inoltre, le precedenti tecniche simboliche spesso si affidavano al campionamento temporale, che manca di correttezza (soundness) e completezza negli scenari di tempo denso. Gli approcci esistenti che utilizzano variabili logiche per agenti illimitati risultano spesso in procedure di semi-decisione con spazi di ricerca infiniti, mancando di meccanismi per garantire la terminazione.

Metodologia
Gli autori propongono un nuovo framework di verifica che integra tre tecniche fondamentali per affrontare queste limitazioni:

1. Rewriting Modulo SMT: Utilizzo di teorie SMT per la rappresentazione simbolica dei vincoli temporali.
2. Narrowing con Variabili Logiche: Impiego di variabili logiche per ragionare su sistemi con un numero ignoto o arbitrario di agenti.
3. Vincoli Ritardati e Folding: Introduzione di un archivio di vincoli (constraint store) su termini parzialmente istanziati, ispirato alla Programmazione Logica con Vincoli (CLP).

L'innoviazione centrale è il Delayed Folding Narrowing. A differenza del narrowing standard, questo metodo permette alle espressioni SMT nelle condizioni delle regole di contenere parti "ritardate"—sotto-espressioni che non possono essere valutate finché i termini non vengono ulteriormente istanziati. Ciò viene ottenuto attraverso un'Estensione SMT in cui le espressioni SMT non valide (ad esempio, mte(t, T') che rappresenta un tempo massimo trascorso) vengono astratte in variabili fresche. Questi vincoli vengono accumulati e risolti o propagati solo una volta che i termini sono sufficientemente istanziati.

Il framework definisce le Teorie di Riscrittura Real-Time Logiche, che estendono le teorie di riscrittura real-time standard per permettere:

• Condizioni nelle regole di riscrittura che includano espressioni SMT con parti ritardate.
• I lati destri (RHS) che includano variabili non presenti nei lati sinistri (LHS).
• Query che contengano variabili condivise tra gli stati iniziali e target.

Per garantire la terminazione, il metodo impiega un meccanismo di folding. Viene costruito un grafo di stato in cui un vettore di stato simbolico $v'$ viene rimosso se è un'istanza di uno stato precedentemente esplorato modulo la teoria equazionale. Gli autori dimostrano che, sotto specifiche condizioni (nello specifico, una gerarchia di sort attentamente progettata), questo preordine di folding assicura uno spazio di ricerca finito, trasformando la procedura di semi-decisione in una procedura di decisione per la verifica degli invarianti.

Contributi Chiave

1. Delayed Folding Narrowing: La definizione e l'implementazione di una relazione di narrowing che gestisce espressioni SMT estese con vincoli ritardati. Ciò consente la verifica di sistemi con arbitrariamente molti parametri logici e SMT sia nella configurazione iniziale che nell'invariante.
2. Verifica del Protocollo Fischer Temporizzato: Il documento presenta la prima verifica automatica della correttezza del protocollo di mutua esclusione di Fischer in tempo reale nel suo setting più generale. Questo include un numero arbitrario di processi e parametri temporali arbitrari ($\gamma$ e $\delta$). Ciò è stato ottenuto progettando una specifica gerarchia di sort per garantire la terminazione della procedura di folding e utilizzando variabili logiche per rappresentare il numero non specificato di processi.
3. Sintesi del Controller per i Filosofi Dinanti: Il framework è applicato al problema dei filosofi dinanti temporizzati per sintetizzare un controller (il "lackey"). Lasciando le transizioni del controller non specificate (rappresentate da variabili logiche), la procedura di narrowing sintetizza le transizioni mancanti necessarie per soddisfare una proprietà di raggiungibilità (ad esempio, l'ingresso di specifici filosofi nella sala da pranzo entro una scadenza).

Risultati
Il metodo è stato implementato come estensione del motore di riscrittura Maude utilizzando funzionalità di meta-livello.

• Protocollo Fischer: Gli autori hanno verificato con successo la mutua esclusione per un numero arbitrario di processi. Quando lo stato iniziale era vincolato in modo che $\gamma > \delta$, lo spazio di ricerca era finito (contenente solo 3 stati grazie al folding), e lo strumento ha confermato che nessun stato raggiungibile violava l'invariante. Al contrario, quando $\delta \ge \gamma$, è stato trovato un controesempio.
• Filosofi Dinanti: Il sistema ha sintetizzato con successo un automa "lackey" che permetteva a specifici filosofi di entrare nella sala da pranzo. L'output ha fornito un insieme concreto di transizioni e posizioni per il controller, dimostrando la capacità del framework di gestire compiti di sintesi.
• Efficienza: Il meccanismo di folding ha ridotto significamente lo spazio di ricerca, consentendo l'analisi di sistemi che sarebbero altrimenti intrattabili a causa di spazi di stato infiniti.

Significatività e Rivendicazioni
Il documento rivendica di fornire una base sonora ed espressiva per la verifica simbolica di teorie di riscrittura real-time. La sua significatività risiede nel colmare il divario tra l'espressività della programmazione logica (gestione di agenti illimitati tramite variabili logiche) e la precisione dell'analisi real-time (gestione del tempo denso tramite SMT e vincoli ritardati).

Gli autori sottolineano che il loro approccio va oltre il "Maude standard" e gli strumenti esistenti per gli Automi Temporizzati Parametrici (PTA), che tipicamente richiedono un numero fisso di processi o limiti temporali fissi. Supportando un numero arbitrario di parametri e un numero illimitato di agenti all'interno di un unico framework, il metodo offre un approccio uniforme per l'analisi di modelli real-time complessi, inclusa la sintesi di componenti mancanti del sistema. Il lavoro suggerisce che i vincoli ritardati siano un meccanismo cruciale per raggiungere la terminazione nelle analisi simboliche di sistemi real-time a stato infinito.