Vai alla Home Page About me Courseware Federica Living Library Federica Federica Podstudio Virtual Campus 3D Le Miniguide all'orientamento Gli eBook di Federica La Corte in Rete
 
 
Il Corso Le lezioni del Corso La Cattedra
 
Materiali di approfondimento Risorse Web Il Podcast di questa lezione

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)


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

  • Esprimere proprietà di safety e liveness in modo indipendente dal testo della specifica;
  • Esprimere un insieme più ricco di proprietà di regolarità.

Un linguaggio standard per la specifica delle proprietà introdotto nella prossima lezione è PLTL

Propositional Linear Temporal Logic

  • Contenuti protetti da Creative Commons
  • Feed RSS
  • Condividi su FriendFeed
  • Condividi su Facebook
  • Segnala su Twitter
  • Condividi su LinkedIn
Progetto "Campus Virtuale" dell'Università degli Studi di Napoli Federico II, realizzato con il cofinanziamento dell'Unione europea. Asse V - Società dell'informazione - Obiettivo Operativo 5.1 e-Government ed e-Inclusion