Adriano Peron » 10.Specifica e verifica in SPIN

Temi della lezione

Esempi di specifica in PROMELA per accesso in mutua esclusione a una sezione critica:
soluzioni già presentate nella lezione N.8;
Verifica di proprietà delle soluzioni proposte usando le funzionalità di model-checking di SPIN:
asserzioni e invarianti globali;
propietà legate alla corretta terminazione.

Esempio di specifica 1

Accesso in mutua esclusione ad una sezione critica: Soluzione 1 (già introdotta nella lezione 8.)

Esempio di specifica 1: soluzione 1

Esempio di specifica 2

Accesso in mutua esclusione ad una sezione critica: Soluzione 2

Esempio di specifica 2: soluzione 2, versione 1

Esempio di specifica 2: soluzione 2, versione 2

Verifica di proprietà di stato

Proprietà di stato: proposizione che può far riferimento (imponendo vincoli) su tutte le componenti che determinano lo stato del sistema:

• Contenuto delle variabili locali;
• Contenuto della variabili globali;
• Contenuto delle code associate ai canali;
• Punti del flusso del controllo dei processi.

Un tipologia di proprietà in cui si fa riferimento alle propriètà di stato sono gli Invarianti.

Invariante: proprietà di stato che deve essere soddisfatta da tutte le esecuzioni (comportamenti).

In PROMELA un invariante viene espresso nella specifica con il costrutto

assert(<condizione>)

Assert è una istruzione sempre eseguibile;
La condizione è valutata nello stato corrispondente all’esecuzione dell’istruzione;
Se richiesto, SPIN verifica la valutazione della condizione dell’istruzione di tutte le esecuzioni.

Assert: esempio

Esempio 1.

byte stato = 1;
proctype A (){(stato==1);x=x+1;assert(stato==2)}
proctype B (){(stato==1);x=x-1;assert(stato==0)}
init{run A();run B()}

SPIN rileva una violazione dell’asserzione.

Esempio 2.

byte stato = 1;
proctype A (){atomic{(stato==1);x=x+1;assert(stato==2)}}
proctype B (){atomic{(stato==1);x=x-1;assert(stato==0)}}
init{run A();run B()}

SPIN non rileva alcuna violazione dell’asserzione.

Si osservi che il controllo dell’invariante stato==2 (risp. stato==1) avviene solo dopo l’esecuzione dell’incremento (risp. decremento).

Condizione di invarianza su tutti gli stati del sistema

Una condizione di invarianza su tutti gli stati del sistema può essere ottenuta eseguendo in parallelo al sistema un processo del tipo:

proctype invariante (){assert(<condizione>)}

• L’asserzione è eseguita una sola volta ma arbitrariamente ad un qualsivoglia stato di avanzamento dei processi che evolvono parallelamente (grazie all’interleaving);
• La garanzia che il controllo venga fatto è determinata dal fatto che il model checker controlla tutte le possibili esecuzioni.

Esempio.

byte stato = 1;
proctype A (){(stato==1);x=x+1;assert(stato==2)}
proctype B (){(stato==1);x=x-1;assert(stato==0)}
proctype invariante(){assert(stato==1 || stato==2)}
init{run A();run B();run invariante()}

SPIN rileva una violazione dell’invariante in corrispondenza del decremento operato dal processo B.

Esempio di specifica 2: soluzione 2, versione 1

Esempio di specifica 2: soluzione 2, versione 1

Verifica dei protocolli di mutua esclusione

L’uso degli invarianti permette di verificare gli esempi di specifica dei protocolli dati:

• Soluzione 1: rispetta le sezioni critiche;
• Soluzione 2, versione 1: non rispetta le sezioni critiche;
• Soluzione 2, versione 2: rispetta le sezioni critiche.

La tecnica degli invarianti di stato non permette di verificare il soddisfacimento di tutte le proprietà desiderabili.

Ad esempio, la Soluzione 1 rispetta le sezioni critiche ma si presta alla generazione di deadlock.

Il deadlock:

• non è rilevabile mediante la valutazione di proprietà di stato;
• è rilevabile mediante l’accertamento dell’imposibilità di fare una transizione di stato.

Condizioni di terminazione

Rispetto le condizioni di terminazione si possono individuare due macro-categorie di processi:

• Processi trasformazionali: terminano dopo aver svolto la funzionalità programmata.
• Processi reattivi: garantiscono in maniera continuativa lo svolgimento di una funzionalità senza terminare.

La terminazione è una proprietà:

• auspicabile per i processi trasformazionali;
• in genere non auspicabile per i reattivi.

In una esecuzione un processo è in stato di attesa quando, non essendo terminato, in quell’esecuzione non ha la possibilità di effettuare alcun avanzamento del controllo.

Le condizione di attesa per un processo (trasformazionale o reattivo):

• può dipendere da un blocco critico;
• può dipendere dall’attesa di una comunicazione (non necessariamente un blocco critico, ad esempio l’attesa della richiesta di svolgere la funzionalità gestita).

Specifica delle condizioni di terminazione

SPIN permette la specifica di punti di controllo (etichette) dove lo stato di attesa di un processo è compatibile con le funzionalità del processo.

Le etichette che indicano punti di attesa equiparabili a terminazione del processo hanno end come prefisso (end-etichetta)
Es. end0, end1, endd, ….

La condizione di corretta terminazione per un processo attivato richiede che:

• Il processo termina, oppure
• Il processo rimane in attesa in uno stato etichettato con una end-etichetta.

Una specifica è corretta rispetto alle condizioni di terminazione se in ogni sua esecuzione

tutti i processi attivati soddisfano la condizione di corretta terminazione.

Esempio di specifica 1: rilevazione di deadlock

Esempio di specifica 2: assenza di deadlock