Riepilogo Tecnico: Verifica di Sistemi SRA Configurabili

Enunciato del Problema

I sistemi digitali moderni, in particolare nel controllo embedded e nei Sistemi su Chip (ad esempio SystemC), sono frequentemente progettati come sistemi Asincroni a Scheduler Restrittivo (SRA). Questi consistono in collezioni di processi asincroni orchestrati da uno scheduler specifico di dominio che esegue i processi in fasi discrete e non preemptive. Sebbene la verifica formale di una singola istanza SRA fissa sia consolidata, la verifica di sistemi SRA configurabili presenta una sfida significativa.

Un SRA configurabile descrive una famiglia illimitata di sistemi possibili definita da un insieme di template di classe e vincoli di configurazione. Un'istanza specifica del sistema viene generata istanziando questi template con oggetti concreti e interconnessioni che soddisfano i vincoli. L'obiettivo della verifica è la verifica parametrica: dimostrare che una proprietà di sicurezza globale $\phi$ vale per ogni istanziazione legale del sistema configurabile, piuttosto che verificare ogni istanza concreta individualmente. Ciò è difficile a causa delle complesse interazioni tra processi, scheduler e della natura illimitata dello spazio di configurazione.

Metodologia

Gli autori propongono un approccio deduttivo di verifica basato su contratti, fondato sulla logica del primo ordine orientata agli oggetti. Il framework sfrutta il verificatore software Dafny come backend. La metodologia scompone il problema di verifica globale in obblighi locali attraverso tre componenti principali:

1. Modellazione e Semantica

Il sistema è modellato utilizzando un linguaggio orientato agli oggetti in cui:

• Le Classi rappresentano i tipi di processo, definiti come Macchine a Stati Finiti Estese (EFSM) con transizioni protette da espressioni booleane ed effetti descritti come istruzioni imperative.
• Lo Scheduler è un EFSM che coordina l'esecuzione delle istanze di classe attraverso fasi discrete (posizioni).
• Le Configurazioni definiscono l'insieme concreto di oggetti e le loro connessioni, vincolate da un insieme di formule logiche $\Gamma$.

La semantica operativa distingue tra esecuzione locale (passi atomici di singole istanze di processo) ed esecuzione globale (cicli guidati dallo scheduler che coinvolgono cicli di auto-ripetizione e transizioni di fase).

2. Strategia di Verifica Compositiva

Invece di modellare esplicitamente lo scheduler, l'approccio utilizza regole di prova composizionali per astrarre i dettagli di schedulazione. La strategia centrale prevede:

• Contratti Locali: Generazione automatica di triple di Hoare (precondizioni/postcondizioni) per i metodi invocati dallo scheduler (init, exec, tick). Questi contratti descrivono le modifiche allo stato locale di una singola istanza.
• Controlli di Conseguenza Globale: Dimostrare che un invariante globale Inv è preservato dalle transizioni dello scheduler. Ciò è ottenuto mediante:
  • Inizializzazione: Mostrare che init stabilisce Inv.
  • Preservazione del Ciclo di Auto-ripetizione: Dimostrare che l'esecuzione di una singola istanza preserva Inv sotto una condizione locale $g'_p$ (che approssima il guardiano globale), e utilizzare l'induzione per estendere ciò a qualsiasi intercalamento di tutte le istanze.
  • Transizioni di Fase: Verificare che i reset di stato e gli aggiornamenti dei timer (tick) preservino Inv.
  • Implicazione di Sicurezza: Dimostrare che Inv implica la proprietà target $\phi$ alla fine di ogni ciclo di schedulazione.

3. Automazione e Ottimizzazione

• Generazione Automatica dei Contratti: La catena di strumenti esegue simbolicamente gli effetti delle transizioni per generare le necessarie pre/post condizioni per i metodi exec, gestendo assegnazioni quantificate e regole di priorità.
• Grounding dei Quantificatori: Per configurazioni con dimensioni di insiemi limitati (ad esempio, $|s| \le k$), il framework riscrive le espressioni quantificate in congiunzioni/disgiunzioni equivalenti prive di quantificatori. Ciò semplifica le condizioni di verifica per i solver SMT preservando l'equivalenza logica sotto i vincoli dati.

Contributi Chiave

1. Framework Unificato per SRA Configurabili: Una formalizzazione indipendente dal dominio per verificare famiglie illimitate di sistemi asincroni a scheduler restrittivo, andando oltre lavori precedenti limitati a casi di studio specifici o topologie fisse.
2. Regole di Prova Compositive: Un insieme di regole deduttive che astraggono lo scheduler, riducendo le prove di invarianza globale a contratti di metodo locali e controlli di conseguenza del primo ordine.
3. Implementazione Automatica: Una catena di strumenti basata su Dafny che genera automaticamente modelli, contratti e trasformazioni di ottimizzazione (grounding dei quantificatori) da descrizioni di logica di controllo di alto livello.
4. Valutazione Sperimentale Scalabile: Validazione su benchmark su scala industriale (sistemi di controllo ferroviario) che coinvolgono decine di migliaia di righe di codice, dimostrando la capacità di provare automaticamente proprietà di sicurezza per tutte le configurazioni valide.

Risultati Sperimentali

Il framework è stato valutato su benchmark provenienti da sistemi di controllo ferroviario industriali (Sistema di Protezione Ferroviaria - RPS, Logica di Controllo dei Segnali - SCL) e da un Sistema di Controllo Robot Generalizzato (RCS).

• Prestazioni: L'approccio ha verificato con successo proprietà di sicurezza per sistemi con decine di migliaia di righe di codice.
• Impatto dell'Ottimizzazione:
  • Basato su Insiemi vs. Basato su Liste: La formalizzazione insiemistica ha superato i precedenti approcci basati su liste, riducendo il tempo di verifica e il consumo di risorse (RC) nascondendo dettagli strutturali non necessari.
  • Grounding dei Quantificatori: L'applicazione di ottimizzazioni di grounding ha ridotto significativamente il tempo di verifica e l'uso delle risorse, in particolare per proprietà complesse.
  • Livello Metodo vs. Livello Transizione: La verifica delle proprietà sul metodo exec (aggregando le transizioni) è stata significativamente più veloce rispetto alla verifica su singole transizioni, attribuita a un migliore riutilizzo delle informazioni da parte del solver SMT.
• Casi di Studio:
  • RPS: Verificate 25 proprietà di sicurezza (21 esistenti, 4 nuove) su codebase di 10k–15k LoC.
  • SCL: Verificata la correttezza dell'aspetto del segnale su codebase di ~6k LoC.
  • RCS: Verificato l'evitamento degli ostacoli per un numero illimitato di sensori.

Significato e Affermazioni

Il documento afferma di fornire una soluzione pratica e scalabile per la verifica parametrica di sistemi SRA configurabili, una classe di sistemi critica per domini safety-critical come le ferrovie e il controllo embedded.

• Automazione: Il framework riduce lo sforzo di annotazione manuale generando automaticamente contratti e sfruttando il prover di Dafny, permettendo agli ingegneri di concentrarsi sulla logica di sistema piuttosto che sui dettagli di prova di basso livello.
• Generalità: A differenza di lavori precedenti limitati a insiemi finiti di prodotti o topologie specifiche, questo framework gestisce famiglie illimitate con vincoli di configurazione flessibili.
• Applicabilità Industriale: La riuscita applicazione a sistemi di segnalazione ferroviaria reali dimostra che la verifica deduttiva può scalare alla complessità industriale senza sacrificare l'automazione.

Gli autori notano che, sebbene la decomposizione e la generazione dei contratti siano completamente automatizzate, la scoperta di invarianti induttivi adatti per proprietà complesse potrebbe ancora richiedere intervento manuale, sebbene considerino la scoperta automatica di invarianti una direzione promettente per il lavoro futuro. Il documento non afferma di risolvere l'indeterminabilità generale della verifica parametrica, ma fornisce piuttosto una metodologia pratica ed efficace per una classe specifica e importante di sistemi.