Home

Federica EU

1/14

Adriano Peron » 11.Proprietà di liveness in SPIN

Temi della lezione

Verifica in PROMELA per proprietà di sequenze cicliche:

Proprietà di progress;
Proprietà di acceptance.

Esempi di applicazione ai protocolli di accesso alla sezione critica.

Limiti dell’approccio.

Proprietà di sequenze cicliche: progress

In PROMELA possono essere espresse direttamente (senza ricorrere ad un linguaggio di specifica di proprietà) due tipi di proprietà delle sequenze cicliche.

Entrambe le proprietà fanno uso di opportune forme di etichettatura nella specifica (come nel caso degli stati di terminazione).

Progresso: non esistono comportamenti infiniti che passano attraverso soli stati non contrassegnati da etichette di progresso (il sistema non può imboccare cicli non contrassegnati da etichette di progresso).

Etichette di progresso:

Ogni etichetta che abbia la stringa progress come prefisso.

Ad esempio: progress0, progress1, .., progresso, etc.

Gli stati marcati da etichette di progress rappresentano stati che debbono (prima o poi) essere attraversati perché la computazione del sistema sia significativa o corretta.

I comportamenti che violano la proprietà sono detti Cicli non-progress.

Proprietà di sequenze cicliche: acceptance

Acceptance: Non ci sono cammini infiniti che includono stati contrassegnati da etichette di acceptance.

Etichette di acceptance:

Ogni etichetta che abbia la stringa accept come prefisso.

Ade esempio: accept0, accept1, .., acceptt, etc.

Le etichette di acceptance contrassegnano stati (del controllo) che in una computazione significativa e corretta non devono poter essere attraversati infinitamente spesso.

La possibilità di ripeterli infinitamente spesso rappresenta una proprietà non desiderata (da cui il nome acceptance per la sua assenza).

I comportamenti che violano la proprietà sono detti Livelock.

Opzioni verifica di base in SPIN

Impostazione delle opzioni di verifica in SPIN per le proprietà di correttezza.

Per verificare le proprietà di sequenze cicliche si seleziona la sezione delle proprietà Liveness;

L’opzione è tra cicli non-progress e cicli di acceptance (livelock);

Opzione aggiuntiva per la verifica è quella di forzare la weak fairness:

I processi che possono eseguire delle istruzioni vengono schedulati.

Accesso in mutua esclusione ad una sezione critica: Soluzione 3

Accesso in mutua esclusione ad una sezione critica: Soluzione 3 (segue)

Proprietà di sequenze: limiti

L’etichetta di progress è legata alle sezioni critica dei due processi.

Si osservi che entrambi i processi possono non-deterministicamente scegliere se richiedere l’accesso alla sezione critica.

La proprietà è garantita con assunzione di weak fairness.

La proprietà di progress non è garantita senza assunzione di weak fairness.

SPIN produce il contro-esempio in Fig.2 con ciclo iniziale sul solo processo A.

Esempi di specifica

Esempio di specifica: soluzione 2

Accesso in mutua esclusione ad una sezione critica: Soluzione 4 (Dekker)

Sezione critica: soluzione 4

Stato di acceptance

Proprietà di sequenze: limiti

Consentono di esprimere solo proprietà semplici delle sequenze.

Esempio:

Nella verifica delle proprietà di liveness consentono di verificare il progresso delle parti ma non consentono di distinguere l’alternanza dall’alternanza stretta.

La verifica richiede che le proprietà siano codificate nelle dichiarazioni della specifica.

E’ utile introdurre un linguaggio autonomo (dal linguaggio della specifica) che permetta di