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
 
I corsi di Scienze Matematiche Fisiche e Naturali
 
Il Corso Le lezioni del Corso La Cattedra
 
Materiali di approfondimento Risorse Web Il Podcast di questa lezione

Adriano Peron » 9.Promela


SPIN

SPIN è un sistema per il model checking per proprietà di programmi software asincroni.

Il sistema è reperibile nel sito Spinroot.

Linguaggio per la scrittura di programmi asincroni.

PROMELA: linguaggio testuale di tipo imperativo con costrutti per la descrizione di processi paralleli e comunicanti.

Manuale in linea

Linguaggio per la scrittura delle proprietà da verificare.

LTL: Linear Temporal Logic.

PROMELA: Variabili e tipi di dato

Variabili dei seguenti tipi di dati di base predefiniti

  • bit Dimensione 1, Valori 0..1
  • bool Dimensione 1, Valori 0..1
  • byte, Dimensione 8, Valori 0..255
  • short Dimensione 16, Valori -2^{15}..2^{15}-1
  • int Dimensione 32, Valori -2^{31}..2^{31}-1
  • chan (Tipo canale di comunicazione)_

Dichiarazioni variabili

<tipo><variabile>;<tipo><variabile> ;
int    state;
byte    msg;

Dichiarazioni array

<tipo><variabile>[dimensione];
byte stato[100] (locazioni 0..99)_

PROMELA: alcune istruzioni di base

Assegnamento

<nome><variabile>=<espressione>;

Es. state = state + 1

Azione nulla

skip

Condizione

(<espressione booleana>)

Es. (a == b)

  • Una condizione booleana è una istruzione eseguibile.
  • La condizione è eseguibile se la sua valutazione è vero; se eseguita permette al flusso del controllo di passare all’istruzione successiva.
  • L’esecuzione di una istruzione booleana con valutazione diversa da vero è sospesa finché la sua valutazione non diviene vero.

PROMELA: Tipi processo

Per eseguire un processo serve

  • avere la possibilità di nominarlo;
  • definire il suo tipo;
  • istanziarlo.

proctype  <nome> ([parametri])‏
{            <body>            }

Il corpo comprende dichiarazioni locali e/o istruzioni.

Esempio: dichiarazione di una variabile globale (statoglobale) e di due processi (A e B).

proctype A (byte parametro)
{ byte statolocale;(parametro==1) ->statolocale=4 }

byte statoglobale

proctype B ()
{ (statoglobale==4)-> statoglobale=statoglobale-1 } ‏

(; e -> sono due separatori di istruzioni tra loro intercambiabili)
Possono essere associati solo parametri di tipo base e non array.

Istanziazione processi

In ogni specifica è necessario dichiarare un processo iniziale

init{ <body>}

(assimilabile ad un main() in un programma C).

Nel processo init è possibile inizializzare variabili globali e instanziare processi

init{ statoglobale=4; run A(1); run B() }

il corpo comprende dichiarazioni locali e/o istruzioni.

Istanziazione di processo

run ([valori parametri])

  • è un comando sempre eseguibile;
  • inizializza una copia del tipo di processo;
  • inizializza i parametri;
  • restituisce un intero pid (run time process number) che dipende dall’implementazione;
  • non aspetta che il processo inizializzato termi per terminare;

(Es. dopo aver inizializzato A non si aspetta la terminazione del processo A per inizializzare B).

Istanziazione processi (segue)

  • Operazione di spawn
    • Run può essere usato per istanziare processi in ogni processo, non solo nel processo Init.
    • PROMELA modella sistemi a stati finiti e dunque il numero di processi istanziabili è limitato (limite hardware dependent).
  • Terminazione dei processi
    • Un processo in esecuzione termina quando il corpo del processo tipo attivato raggiunde l’istruzione finale;
    • Un processo non termina finché tutti i processi che ha istanziato siano terminati.
  • Attivazione concorrente Init{ statoglobale=4; run A(1); run B() }
    • le istanziazioni dei processi A e B sono concorrenti;
    • le loro istruzioni sono eseguite in interfogliazione (interleaving).

Interleaving processi

byte stato = 1

proctype A() { (stato ==1)-> stato = stato +1 }

proctype B() { (stato ==1)-> stato = stato - 1 }

init{ run A(); run B() }

Possibili esecuzioni:

  • A termina prima dell’esecuzione dell’iscruzione condizionale di B: stato=2 e B è di conseguenza bloccato;
  • B termina prima dell’esecuzione dell’istruzione condizionale di A: stato=0 e A è di conseguenza bloccato;
  • A e B eseguono l’istruzione condizionale; A esegue l’incremento e poi B il decremento; stato = 1; A e B terminano;
  • A e B eseguono l’istruzione condizionale; B esegue il decremento e poi A l’incremento; stato = 1; A e B terminano.

Atomicità di sequenze di istruzioni

L’interfogliazione può essere limitata rendendo atomica l’esecuzione di sequenze di istruzioni.

byte stato = 1

proctype A() { atomic {(stato ==1)-> stato = stato +1 }}

proctype B() { atomic {(stato ==1)-> stato = stato -1 }}

init{ run A(); run B() }

Possibili esecuzioni:

  • A termina prima dell’esecuzione dell’iscruzione condizionale di B: stato=2 e B è bloccato;
  • B termina prima dell’esecuzione dell’istruzione condizionale di A: stato=0 e A è bloccato;
  • Solo un processo (scelto in modo non deterministico) ha la possibilità di terminare.

Comunicazione asincrona via canali

PROMELA permette forme di comunicazione sincrona e asincrona mediante canali.

I canali sono tipi di base dichiarati come gli altri tipi di base

chan <nomecanale>= [dim] of { tipo1, .., tipon }

  • Comunicazione asincrona
    • dichiara il nome di un canale;
    • il canale è associato ad un buffer di dimensione [dim] > 0 per ospitare messaggi; ciascun valore di messaggio è strutturato come un record con campi di tipo base { tipo1, .. ,tipon }.

Esempio:

chan coda = [10] of { short, short }

I messaggi sono strutturati in coppie di interi. La capacità del buffer è di dieci unità.

Invio e ricezione asincroni su canali

chan <nomecanale> = [dim] of { tipo1, .., tipon }

Comunicazione asincrona (dim > 0)_

Istruzione di Invio

<nomecanale>! <expr1>,..,<exprn>

L’operazione di invio è eseguibile solo se il buffer associato al canale non è pieno.
Il messaggio è memorizzato in coda al buffer;
Se vengono passati solo m < n valori, gli ultimi n-m campi del messaggio hanno valore indefinito.

Istruzione di Ricezione

<nomecanale>? <Var1>,..,<Varn>

L’operazione di ricezione è eseguibile solo se il buffer del canale non è vuoto;
L’operazione estrae il messaggio dalla testa del buffer e memorizza le componenti del messaggio in ordine nelle variabili;
Se sono presenti solo m < n variabili, gli ultimi n-m campi del messaggio sono ignorati.

Invio e ricezione asincroni su canali (segue)

Per verificare il numero di messaggi in coda ad un canale

len (<nomecanale> )

atomic { (len(canale) > 1) -> canale?X }

Per condizionare la ricezione alla presenza di valori specifici nel messaggio

<nomecanale>? <Const1> ,..,<Varn>

Al posto di una variabile si può avere un valore costante;
L’istruzione viene eseguita solo se la componente corrispondente a una costante ha lo stesso valore espresso dalla costante.

Canale?0
eseguibile solo se il messaggio in testa al buffer è 0

Variante in forma di condizione

Canale?[0]
Condizione verificata se Canale? 0 è eseguibile. Non altera il contenuto del buffer.

Invio e ricezione asincroni su canali (segue)

I nomi dei canali per le operazioni di comunicazione possono essere parametrici e comunicati dinamicamente ai processi

proctype A(chan c1)_
{ chan c2 ;
c1?c2;
c2!25
}

sul canale parametrico c1 A riceve il nome di un canale (C2) e su quel canale trasmette 25. Nell’esempio il canale effettivamente usato è “canale”.

Init
{
short X;
chan passaggio = [1] of { chan };
chan canale = [1] of { short };
run A( passaggio );
paggaggio!canale;
canale?X
}

Sequence chart della simulazione dell’esempio della slide precedente:

  • Ogni blocco rappresenta un processo ed il suo stato di avanzamento;
  • Ogni freccia rappresenta una comunicazione tra processi;
  • Esempio 1!2 indica che il processo Init tramite il canale 1 (passaggio) comunica il canale 2 (canale);
  • Sul canale 2 (canale) il processo A invia poi il valore 25.
Fig.1 Sequence chart

Fig.1 Sequence chart


Comunicazione sincrona su canali

chan <nomecanale>[0] of { tipo1, .., tipon }

con dimensione 0 del buffer la comunicazione è sincrona nella forma dell’ HANDSHACKING.

Esempio:

chan canale = [0] of {int}

proctype A (){ canale!125; canale!126 }
proctype B (){ int X; canale?X }
init {run A(); run B()}

Solo il processo B può terminare dopo la prima sincronizzazione.
Il processo A rimane in attesa della seconda sincronizzazione e non può terminare (stato waiting).

Costrutti di controllo

Costrutto di scelta
if
:: istruzione1
:: istruzione 2

:: istruzione n
fi

Tra le istruzioni elencate, viene scelta una istruzione eseguibile; Se più di una istruzione è eseguibile la scelta è non-deterministica; L’istruzione If non è eseguibile quando nessuna delle istruzioni è eseguibile.

Costrutto iterativo

do
:: istruzione1
:: istruzione 2

:: istruzione n
od

  • Ad ogni iterazione viene scelta una sola istruzione eseguibile con lo stesso criterio del costrutto if;
  • L’uscita dall’iterazione è attuata mediante l’esecuzione dell’istruzione break.

Esempio

proctype contatore()
{    int X =1;
do
:: (X != 0);     if
:: X=X+1
:: X=X-1
fi
:: (X == 0);    break
od    }

  • Ad ogni iterazione solo una delle istruzioni del ciclo do può essere eseguita;
  • Se X è pari a zero si termina il ciclo;
  • Se X è diverso da zero la scelta tra incremento e decremento è non-deterministica;
  • Non è garantito che il processo termini.

Costrutti di controllo

Costrutto di salto incondizionato

<etichetta>:
.
.
goto <etichetta>

Il salto incondizionato è una istruzione sempre eseguibile;
La scelta dei nomi delle etichette deve essere fatta con cura: le etichette che abbiano i seguenti prefissi “end“, “progress“, “accept” assumono significato specifico chiarito nelle lezioni successive.

Esempi di specifica

Fig. 2 Esempio di specifica: shift register con due posizioni e canali di comunicazione asincroni.

Fig. 2 Esempio di specifica: shift register con due posizioni e canali di comunicazione asincroni.


Esempi di specifica (segue)

Fig. 3 Esempio di specifica: shift register con due posizioni e canali di comunicazione sincroni.

Fig. 3 Esempio di specifica: shift register con due posizioni e canali di comunicazione sincroni.


Esempio

Processi ricorsivi descritti mediante run (spawn) e canali.
Esempio della definizione per il fattoriale.

proctype fact(int n; chan p)
{ chan child = [1] of { int };
int result;
if :: (n <= 1) -> p!1
:: (n >= 2) -> run fact(n-1, child); child?result; p!n*result
fi }

init { chan child = [1] of { int };
int result;
run fact(4, child);
child?result }

SPIN, permettendo di definire solo programmi a stati finiti, consente solo la creazione di un numero limitato (dall’implementazione) di processi e dunque non consente di calcolare il fattoriale per numeri arbitrari.

Esempi di specifica

Fig. 4 Esempio di specifica: simulazione del fattoriale.

Fig. 4 Esempio di specifica: simulazione del fattoriale.


  • 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