Combining model checking with simulation-based techniques for protocol verification

Sintesi Tecnica: Combinare il Model Checking con Tecniche Basate sulla Simulazione per la Verifica di Protocolli

Problema
Il model checking è una tecnica rigorosa per la verifica di sistemi a stati finiti, tuttavia è frequentemente ostacolato dal problema dell'esplosione dello spazio degli stati. Man mano che i parametri del sistema aumentano (ad esempio, capacità dei canali o dimensioni delle finestre), lo spazio degli stati raggiungibili cresce esponenzialmente, rendendo l'esauriente verifica impraticabile. Questo articolo affronta tale limitazione nel contesto dei protocolli di comunicazione, nello specifico l'Alternating Bit Protocol (ABP) e lo Sliding Window Protocol (SWP). Mentre astrazioni più semplici come il Simple Communication Protocol (SCP) possono essere verificate direttamente, l'aumento dei parametri in ABP e SWP fa sì che lo spazio degli stati superi le capacità degli standard strumenti di model checking, anche con hardware moderno.

Metodologia
Gli autori propongono una metodologia di verifica ibrida che combina il model checking con le relazioni di simulazione per superare l'esplosione dello spazio degli stati. Il fondamento teorico centrale si basa sul principio secondo cui, se una macchina a stati concreta $M$ è simulata da una macchina a stati astratta $M_A$, e $M_A$ soddisfa una proprietà invariante, allora l'invariante corrispondente vale per $M$.

La metodologia è operazionalizzata utilizzando il linguaggio di logica di riscrittura Maude e prevede due framework primari:

1. Verifica della Simulazione Diretta:
   Per verificare un protocollo concreto $M$ rispetto a un protocollo astratto $M_A$:

   • Passaggio 1: Eseguire il model checking diretto sulla macchina astratta $M_A$ per verificare la sua proprietà invariante.
   • Passaggio 2: Congetturare un candidato di relazione di simulazione $r$ tra $M$ e $M_A$. Dimostrare che l'invariante di $M$ è logicamente deducibile dall'invariante di $M_A$ sotto l'assunzione di $r$, utilizzando il partizionamento dei casi (case splitting) statico e la riduzione.
   • Passaggio 3: Dimostrare che $M$ è effettivamente simulato da $M_A$. Ciò comporta la verifica delle condizioni di simulazione (corrispondenza dello stato iniziale e preservazione delle transizioni) per tutte le regole di riscrittura di $M$.
   • Implementazione: Il Passaggio 3 utilizza una procedura a tre comandi in Maude:
     • srew: Per trovare gli stati successori in $M$ utilizzando costanti fresche per rappresentare valori arbitrari.
     • red: Per verificare che la relazione di simulazione sia valida tra gli stati concreti e quelli astratti.
     • search: Per confermare che la macchina astratta possa raggiungere uno stato corrispondente in zero o più passi.
   • Per garantire la correttezza nonostante l'uso di supersetti di stati raggiungibili (a causa dell'indecidibilità della raggiungibilità), gli autori impiegano il Lemma 1, che dimostra come la verifica della condizione di transizione su questi supersetti sia sufficiente a garantire la condizione sugli stati effettivamente raggiungibili.

2. Composizione di Relazioni di Simulazione:
   Per sistemi altamente complessi dove una singola astrazione non è sufficiente, gli autori propongono un approccio gerarchico. Ciò comporta l'incatenamento di relazioni di simulazione (ad esempio, $SWP \to ABP \to SCP$).

   • L'invariante del sistema più concreto è dedotto dal sistema intermedio, che a sua volta è dedotto dal sistema più astratto.
   • Ciò consente la verifica di sistemi con spazi di stati massicci sfruttando gli invarianti verificati di astrazioni stratificate più semplici.

Contributi Chiave
L'articolo presenta due contributi principali:

1. Una metodologia che combina il model checking con le relazioni di simulazione per verificare sistemi in cui il model checking diretto fallisce a causa dell'esplosione dello spazio degli stati.
2. Una metodologia per la composizione di relazioni di simulazione, che consente la verifica gerarchica collegando più livelli di astrazione per gestire modelli ancora più grandi e complessi.

Risultati e Casi di Studio
Gli autori hanno valutato il loro approccio utilizzando tre protocolli: SCP, ABP e SWP.

• Caso di Studio I (ABP):

  • Sfida: Il model checking diretto di ABP con maxIndex = 64 e maxQueueLength = 32 ha causato un timeout (>3.600 secondi) a causa dell'esplosione dello spazio degli stati.
  • Soluzione: Gli autori hanno stabilito una relazione di simulazione da ABP al più semplice SCP.
  • Risultato: L'intero processo di verifica (controllo di SCP, deduzione dell'invariante e verifica della simulazione) è stato completato in meno di 1 secondo per passaggio. Ciò ha confermato che ABP soddisfa la sua proprietà invariante senza esplorazione esaustiva degli stati.

• Caso di Studio II (SWP):

  • Sfida: SWP introduce la gestione della finestra e i numeri di sequenza, creando uno spazio di stati significativamente più grande di ABP, rendendo impossibile la verifica diretta.
  • Soluzione: Gli autori hanno impiegato la composizione di relazioni di simulazione: $SWP \to ABP \to SCP$. Hanno verificato la simulazione da SWP a ABP e combinato la relazione precedentemente verificata tra ABP e SCP.
  • Risultato: L'approccio gerarchico ha verificato con successo la proprietà invariante di SWP (garantendo che i messaggi siano ricevuti in ordine senza perdita o duplicazione) con parametri (windowSize = 16, maxQueueLength = 32) che sarebbero stati impraticabili per il controllo diretto.

Significatività e Rivendicazioni
L'articolo sostiene che questo approccio mitiga efficacemente il problema dell'esplosione dello spazio degli stati spostando il carico computazionale dall'esplorazione esaustiva degli stati alla verifica simbolica su modelli astratti più piccoli. Gli aspetti chiave della significatività includono:

• Scalabilità: Il metodo permette la verifica formale di protocolli con grandi parametri (ad esempio, dimensioni delle finestre e lunghezze delle code) che sono oltre la portata del model checking diretto.
• Riutilizzabilità: Le specifiche formali esistenti possono essere riutilizzate come modelli astratti per nuovi target più complessi, riducendo significativamente lo sforzo di verifica.
• Automazione e Rigore: Sebbene la costruzione dei modelli astratti e delle relazioni di simulazione richieda una conoscenza del dominio manuale, la validità di tali relazioni viene verificata semi-automaticamente utilizzando i comandi standard di Maude. Gli autori hanno sviluppato uno strumento di supporto per automatizzare il partizionamento dei casi e l'esecuzione dei comandi, minimizzando l'errore umano.
• Distinzione dal Lavoro Esistente: A differenza del Counterexample-Guided Abstraction Refinement (CEGAR), che è reattivo e raffina i modelli basandosi su controesempi spurii, questo approccio è proattivo, sfruttando la conoscenza del dominio per costruire astrazioni strategiche. Ciò fornisce una maggiore trasparenza e interpretabilità, poiché le relazioni di simulazione mantengono una mappatura comprensibile all'uomo tra i comportamenti concreti e quelli astratti.

Gli autori concludono che, operazionalizzando la teoria della simulazione in una sequenza standardizzata di comandi Maude, hanno colmato il divario tra le relazioni teoriche astratte e i flussi di lavoro di verifica eseguibili, offrendo un percorso pratico ed efficiente per la verifica di sistemi distribuiti complessi.