Che materia stai cercando?

Elementi di Software Dependability Appunti scolastici Premium

Appunti di Elementi di Software Dependability. Nello specifico gli argomenti trattati sono i seguenti: Modellazione Markoviana degli Attributi di Dependability, Valutazione degli attributi RAMS con il Metodo Markoviano, Ridondanza, Rilevazione & Correzione... Vedi di più

Esame di Elementi di Software Dependability docente Prof. U. Monile

Anteprima

ESTRATTO DOCUMENTO

Algoritmi Distribuiti

4. Algoritmi distribuiti

4.1 Introduzione Recovery

Esistono due tecniche di :

Forward error recovery

1. : il sistema viene riportato ad uno stato noto

safe reset

come “ ” (il è un caso particolare: stato iniziale)

Backward error recovery

2. : il sistema viene riportato ad uno stato

“corretto” in cui è già transitato.

Il reset è un caso particolare delle procedure di recovery (recupero) a fronte di

un guasto di una macchina singola. In caso di guasto (crash) la macchina viene

stateful

fatta ripartire, ma nel caso di computazioni “ ” dovremo essere in grado

di ripristinarne lo stato.

Backward

Nel occorre perciò memorizzare lo stato di tanto in tanto su memoria

non volatile (Checkpoint), in una memoria stabile.

La granularità del checkpointing dipende dai valori di disponibilità attesi

(quanta computazione possiamo permetterci di perdere).

Il lavoro svolto tra un checkpoint e il successivo (insieme di operazioni), viene

considerato, per quanto riguarda i guasti, un’azione

azione atomica, che gode della

un’ atomica

proprietà tutto o niente. Questo concetto è molto simile a quello di transizione

su un data base (DB). property

Un’azione atomica deve soddisfare alcune proprietà, note come ACID

(da Atomicità, Consistenza, Isolamento, Durabilità):

 atomicità: un’azione atomica è indivisibile nella sua esecuzione e la sua

atomicità

esecuzione deve essere o totale o nulla, non sono ammesse esecuzioni

intermedie;

 coerenza: un’azione atomica non viola gli invarianti del Sistema

coerenza

(contraddizioni)

 isolamento: ogni azione atomica deve essere eseguita in modo isolato e

isolamento

indipendente dalle altre azione atomiche, l'eventuale fallimento di una

azione atomica non deve interferire con le altre azione atomiche in

esecuzione;

 durabilità:

durabilità dopo che una azione atomica è stata eseguita nella sua

interezza i suoi effetti vengono registrati in maniera permanente.

61 Algoritmi Distribuiti

Vediamo un esempio di Checkpointing in ambito distribuito 

L’inconveniente, come mostrato in figura è l’Effetto-domino. L’effetto domino

provoca il ripristino dello stato di ciascun nodo al proprio valore iniziale,

perdendo quindi tutti i risultati della computazione prodotti fino alla rivelazione

dell'errore.

Introduciamo il concetto di linee di recovery. Le line di recovery, come si può

osservare dalla figura sottostante, attraversano le linee di vita dei vari nodi solo

in corrispondenza dei checkpoint. Le linee di recovery indicano, dato un crash

in un punto di una regione compreso tra due linee, a quale checkpoint deve

essere ricondotto ciascun nodo.

L’azioni

zioni atomiche distribuite = lavoro svolto dai nodi tra due linee di recovery

L’a 62 Algoritmi Distribuiti

4.2 Memoria Stabile

Lo stato di ciascun nodo viene memorizzato su memoria stabile.

La memoria stabile è l’astrazione della memoria reale, con la proprietà di

contenere le informazioni necessarie al recupero e di non essere soggetta ad

alcun tipo di malfunzionamento.

type dati = ........;

pagina = 0 .. Maxpag;

risultato = (OK, BAD);

Procedure Read (P: pagina; var D: dati; var R:Risultato);

Procedure Write (P: pagina; D: dati); crashes

Questa memoria paginata non viene influenzata da del processore,

eccetto la pagina su cui, eventualmente, si scriveva al momento del crash

write

(procedura di non atomica)

Ogni pagina stabile P è realizzata tramite due (o più) pagine reali P e P tali

S 1 2

che non decadano mai contemporaneamente (appartengono a cilindri diversi

dello stesso disco, o a dischi diversi)

read write restart

Le procedure -stabile, -stabile, da-crash, garantiscono, per ogni

pagina stabile P , che valga il seguente invariante:

S

 Validity: i dati replicati sono validi.

 Agreement: i dati replicati sono in accordo.

L’invariante vale sempre, tranne che durante l’esecuzione di una

write-stabile.

Vediamo nel dettaglio le procedure di read-stabile, write-stabile, restart da-

crash. 63 Algoritmi Distribuiti

Read-

- stabile:

ile: legge una pagina, se la lettura non va a buon fine legge la pagina

Read stab

ridondante:

Procedure Read-stabile (Ps: pagina-stabile; var Ds: dati);

begin

Read(P1,d,Ris)*;

if Ris = OK then Ds:=d;

else begin

Read(P2,d,Ris)*; Ds :=d;

end;

end;

2. Write-

- stabile:

: scrive una pagina e la legge per accertarsi che la scrittura sia

Write stabile

avvenuta correttamente, procede nello stesso modo con la pagina ridondante. Il

crash

problema si ha se il avviene tra la fine della prima lettura e l’inizio della

seconda scrittura:

Procedure Write-stabile (Ps: pagina-stabile; var Ds: dati);

Begin

repeat

Write(P1, Ds); Read(P1,d,Ris);

until Ris = OK and Ds = d;

repeat

Write(P2, Ds); Read(P2,d,Ris);

until Ris = OK and Ds = d;

end;

3. Restart da-

- crash: legge la prima e la seconda pagina, se la lettura ha

da

successo passo alla seconda pagina, altrimenti copia la seconda pagina sulla

prima e controllo l’esito della scrittura. Passo alla seconda pagina, se la lettura

ha successo ed è consistente con la prima il recovery è terminato, altrimenti

copia la pagina nella seconda e verifico il successo della scrittura.

Procedure restart-da-crash;

Begin

Read(P1,d1,Ris1);

Read(P2,d2,Ris2);

If Ris1 = BAD then

repeat

Write(P1, d2); Read(P1,d1,Ris1);

until Ris1 = OK and d1 = d2;

else if Ris2 = BAD or d1 != d2 then

repeat

Write(P2, d1); Read(P2,d2,Ris2);

until Ris2 = OK and d1 = d2;

end; 64 Algoritmi Distribuiti

4.3 Two-

- Phase Commit Protocol

Two two-phase commit protocol

Il protocollo (2PC) è un algoritmo distribuito che

consente la gestione delle azioni atomiche in ambiente distribuito.

commit

Con il protocollo di 2PC il dei dati avviene in due fasi. Nel prima fase

PREPARE TO

un "coordinatore" della azione atomiche manda il messaggio di

COMMIT a tutti i partecipanti interessati all’azione atomica, i quali

AGREE

risponderanno positivamente inviando un messaggio di entro il

COMMIT

timeout. Nella seconda fase il coordinatore invia il messaggio di e

ACKNOWLEDGE

tutti risponderanno con un . Se qualcuno risponde

DISAGREE

negativamente inviando un messaggio di o non risponde, viene

ABORT

inviato il messaggio di da parte del coordinatore, e tutti risponderanno

con un messaggio di ACKNOWLEDGE tornando alla situazione definita dagli

ultimi checkpoint.

Nel 2PC il numero dei messaggi è 4 N, dove N è il numero dei partecipanti.

Questo protocollo è appropriato se:

 Esiste il meccanismo di broadcast (in questo caso il totale dei messaggi

è 2N+2).

 Si vuol privilegiare il parallelismo tra i partecipanti.

 La struttura e il numero dei partecipanti variano dinamicamente.

4.4 Linear Two-

- Phase Commit Protocol

Two

 Ad ogni partecipante è assegnato un numero progressivo.

 Ogni partecipante conosce il nome del successivo e l’ultimo sa di essere

l’ultimo.

 I partecipanti comunicano, dal primo verso l’ultimo, di essere arrivati al

punto di commit (fase 1).

 Se tutto va bene l’ultimo risponde OK e il messaggio fluisce in senso

inverso (fase 2).

 Se durante la fase 1 qualcuno decide di abortire il messaggio “Abort”

fluisce nei due sensi.

 Numero totale dei messaggi 2 N.

Questo protocollo è appropriato se:

 Il meccanismo di comunicazione è costoso e in assenza di broadcast,

oppure la tipologia della rete è ad anello

 Non è necessario prevedere concorrenza durante le fasi 1 e 2.

 La struttura dei partecipanti è conosciuta staticamente.

65 Algoritmi Distribuiti

4.5 Considerazioni sugli Algoritmi distribuiti

Gli algoritmi distribuiti vengono utilizzati quando si voglia garantire la

consistenza di dati in tutto o parzialmente replicati in vari server.

In generale, tali algoritmi garantiscono proprietà di Validity e Agreement a

fronte di possibili guasti. Molti di questi algoritmi sono limitati dal principio di

incertezza: un nodo che ha richiesto un’azione remota non può sempre

incertezza

determinare, in un tempo finito, se l’azione è stata eseguita o no.

4.6 Paradosso dei generali bizantini

Si immaginano diverse divisioni dell’esercito bizantino accampate al di fuori di

una città nemica, ognuna delle quali con il proprio generale. I generali possono

comunicare tra loro soltanto attraverso dei messaggeri e dopo aver osservato il

nemico devono decidere un piano di attacco comune (protocollo per

sincronizzare gli attacchi). Tuttavia, alcuni messaggi non arriveranno perché i

messaggeri possono perdere la vita attraversando un campo minato (questo

equivale ad avere un canale trasmissivo con disturbo).

E’ facile da capire che non esiste un protocollo di durata massima fissata.

Dimostrazione: Supponiamo che esistano protocolli di questo tipo, e sia P

quello più corto (in termini di numero di messaggi scambiati). Se l’ultimo

messaggero salta su una mina, allora:

 era inutile, ma allora P non era il più corto;

 o era utile, ma allora P non funziona.

66 Algoritmi Distribuiti

4.7 Consenso Distribuito tra processi asincroni

4.7.1 Introduzione

Definizione: un processo distribuito si dice corretto in un dato contesto se non

va in crash in quel contesto ( si considera il fatto che un processo può andare in

crash ma non può inviare dati errati).

Un algoritmo di consenso distribuito deve soddisfare le seguenti proprietà:

1. Validity: se il sistema restituisce un valore v in uscita allora esiste

almeno un processo che lo ha proposto. faulty

2. Agreement: se due processi sono non allora propongono valori

concordanti.

3. Termination: un processo non faulty propone un valore entro un tempo

massimo

Fischer, Lync e Paterson hanno affermato che è impossibile risolvere il consenso

(cioè soddisfare le tre proprietà) se qualche processo fallisce.

Più precisamente, hanno provato che, sotto l’assunzione di Validità e

Agreement, la possibilità che anche un singolo processo si gusta invalida la

terminazione, cioè l’intero sistema fallisce. Così, mentre la proprietà di Validità

e Agreement possono essere garantite attraverso appropriato algoritmo, al fine

di rispettare la terminazione è necessario introdurre qualche forma di sincronia

nel sistema.

Chandra e Toueg hanno proposto una soluzione a questo problema, aggiungendo

dei “rilevatori di fallimento inaffidabili” (FDS), vale a dire, moduli che possono

essere interrogati a livello locale per trovare se un altro processo a livello locale

è attualmente sospettato di essere faulty (di essere andato in crash).

I rilevatori di fallimento garantiscono le seguenti due proprietà:

Eventual Weak Accuracy

1. : esiste un istante di tempo dopo il quale

qualche processo corretto non è mai sospettato.

Strong Completeness

2. : prima o poi ogni processo faulty diviene

permanentemente sospetto da ogni processo corretto.

67 Algoritmi Distribuiti

4.7.2 Chandra Toueg

Chandra e Toueg [CT96] hanno proposto un algoritmo per risolvere il consenso

crash-failures

in un modello asincrono con , dove:

 i processi sono completamente interconnessi attraverso un canale di

point-to-point

comunicazione bidirezionale quasi-affidabile, in cui la

consegna del messaggio è garantita solo se né il mittente né il ricevitore

falliscono;

 broadcasting

il è affidabile (Reliable broadcast), cioè i messaggi inviati

in broadcasting prima o poi arrivano a tutti i processi non faulty.

Assunzioni di guasti:

1. solo una minoranza di processi può fallire.

2. la presenza dei FDS fornisce informazioni sui processi falliti.

Intuizione:

 L’algoritmo viene eseguito localmente da ogni processo e procede in

cicli (rounds).

 rotating coordinator paradigm

Infatti si basa sul : in ogni giro “r” un

singolo processo sarà il coordinatore e gli altri saranno i partecipanti.

 Ognuno degli n processi conosce il valore “n” e conserva un local round

counter; così, in ogni momento, può determinare localmente il

coordinatore a quel giro .

 Per ogni giro, ciascun partecipante invia il suo valore attuale al

coordinatore di questo giro.

 Il coordinatore sceglie uno tra i più recenti valori proposti che ha

ricevuto e lo invia a tutti i partecipanti usando il meccanismo di

Reliable Broadcast.

 Ciascun processo confronta il valore ricevuto con quello da lui calcolato

e se concorda invia al coordinatore un ACK

 Se la maggioranza dei nodi ha inviato un ACK il coordinatore manda a

tutti i processi corretti il risultato parziale della computazione da

accettarsi come definitivo, a questo punto i processi possono decidere e

uscire dall’algoritmo.

Poiché nessun presupposto sul tempo può essere fatto, è impossibile per un

partecipante capire il motivo (rete lenta o si è schiantato coordinatore), che sta

dietro alla non ricezione di un messaggio del coordinatore.

 In tal modo, ogni partecipante ha la possibilità di sospettare che il

coordinatore abbia fallito.

 In questo caso, il partecipante invia un ACK negativo (NACK) e si

sposta al seguente round, mantenendo il suo attuale valore.

68 Algoritmi Distribuiti

4 . 7 .2.1

1 Quasi-

- reliable point-

- to-

- point communication

.2. Quasi point to

I processi sono completamente interconnessi da canali di comunicazione

bidirezionali che rappresentano il mezzo di comunicazione di base. Le primitive

in pseudo codice sono abbastanza semplici:

 denota l’invio

Qpp send (sender, number, contents) to ricevitore :

quasi-affidabile di un messaggio da parte del processo mittente al

processo ricevitore, dove number svolge il ruolo di numero di sequenza

che permette di distinguere i messaggi provenienti dal mittente;

 Qpp receive(sender, number, contents): è una procedura di ricezione,

estrae i dati pertinenti indicati formalmente dai parametri (sender,

number, contents.)

La proprietà necessaria su queste operazioni è la seguente:

Quasi affidabilità: Se il processo mittente esegue "Qpp send(sender, number,

contents) to ricevitore", e se sia il mittente e il ricevitore sono corretti, il

ricevitore alla fine eseguirà "Qpp receive(s, n, c)" per ricevere i valori (sender,

number, contents).

 Reliable Broadcast

Formalmente il definito da due primitive:

 RBC broadcast(sender, contents): quando il processo invia in broadcast

un messaggio del tipo (sender, contents)

 RBC deliver(sender, contents): quando il processo consegna un

messaggio (sender, contents).

Trasmissione affidabile in broadcast (Reliable broadcast) è caratterizzata da tre

seguenti proprietà:

 Validità: Se un processo corretto esegue RBC broadcast(sender,

Validità

contenuto), alla fine esegue RBC deliver(s, c) per il messaggio (sender,

contents).

 Agreement Se un processo corretto esegue RBC deliver(s, c) per un

messaggio (sender, contents), alla fine tutti i processi corretti eseguono

RBC deliver (s, c) per il messaggio (sender, contents).

 Integrità uniforme Per ogni messaggio (sender, contents), ogni processo

esegue RBC deliver(s, c), al massimo una sola volta, e solo se alcuni

processi precedentemente hanno eseguito un RBC broadcast(sender,

contents). 69 Algoritmi Distribuiti

4 . 7 .2.2

2 Primitive del Consenso

.2.

Formalmente, nel problema del Consenso, i processi corretti propongono un

valore e tutti i processi corretti devono decidere tra i valori proposti un valore

comune. Il consenso definito in termini di due primitive C_ (v) e

 PROPOSE

C_ (v). Quando un processo esegue C_ (v), significa che il processo

DECIDE PROPOSE

propone il valore v. Similarmente quando un processo esegue C_ (v)

DECIDE

significa che il processo decide il valore v.

In sintesi, ogni esecuzione del consenso deve soddisfare le seguenti tre proprietà:

 Validity: Se un processo corretto decide un valore v (esegue

C_ (V)), allora qualche processo deve avere proposto questo valore

DECIDE

(eseguendo C_ (V)).

PROPOSE

 Agreement: Non è possibile che due processi corretti (cioè che eseguono

C_ ) decidono valori differenti.

DECIDE

 Termination: Ogni processo corretto alla fine decide un valore.

4 . 7 .2.3

.3 Algoritmo di Chandra e Toueg che risolve il consenso

.2

In questa sezione viene proposto l’algoritmo di Chandra e Toueg che risolve il

problema del Consenso usando un failure detector di tipo .

 

Questo algoritmo tollera al più di processi guasti (in un sistema

(

n / 2

) 1

 

asincrono con n processi) e assume che processi siano corretti.

(

n 1

) / 2

L'Eventual Weak Accuracy permette al failure detector di sospettare

erroneamente qualsiasi processo corretto, solo dopo un certo istante di tempo

qualche processo corretto non sarà più sospettato.

Questo algoritmo usa il paradigma rotating coordinator e procede in “round”

asincroni.

Sia n il numero di processi, allora la funzione crd(r) restituisce il numero intero

((r - 1) mod n) che indica il coordinatore c durante il round r. Questa funzione è

nota a tutti i processi, pertanto, ciascuno di essi è in grado di calcolare in

qualsiasi momento l'identità del coordinatore di un ciclo. Ciascuno degli n

processi memorizza una stima locale del valore decisionale cercato, insieme con

stamp

uno che dice in quale round il processo è giunto a credere in questa

belief

stima. Facciamo riferimento alla coppia (stima, stamp) con .

L'obiettivo di questo algoritmo è quello di raggiungere una situazione in cui la

maggioranza dei processi è d'accordo sulla stessa stima. Per raggiungere una

tale situazione, i coordinatori e partecipanti si scambiano le loro attuali stime,

round dopo round, attraverso Qpp-messaggi.

70 Algoritmi Distribuiti

Il ruolo di un coordinatore è: (i)raccogliere un numero sufficientemente grande

di beliefs, (ii) per scoprire quello con lo stamp più alto (iii) e selezionarlo, e (iv)

alla fine diffondere a tutti i partecipanti tramite un Reliable broadcast la sua

selezione in modo che essi possano aggiornare le loro beliefs locali.

Analizziamo la struttura del loop dell'algoritmo in

Figura 13.

13

Come detto prima, ogni processo passa attraverso quattro fasi per ciclo, vale a

while

dire il ciclo di :

 Fase 1: durante questa fase ogni processo invia la stima corrente del

valore deciso, e lo stamp pari al valore dell'ultimo round in cui il valore

stimato stato aggiornato, al processo coordinatore c.

 Fase 2: tutti i processi, tranne il coordinatore passano immediatamente

alla fase P3. Il processo coordinatore c durante questa fase raccoglie

  valori, e di tali valori stimati seleziona quello con lo stamp

(

n 1

) / 2

più alto, questa operazione è eseguita attraverso la funzione best

(Qpp:P1 ricevuto) , e lo invia a tutti i processi usando di nuovo Qpp-

r

messanger. Il coordinatore passa alla fase P3.

 Fase 3: durante questa fase per ogni processo corretto ci sono due

possibilità:

 un generico processo p riceve la stima dal processo

coordinatore c e invia un ack a c per indicare che ha adottato la

proposta dal coordinatore come nuova stima; oppure

 in seguito all'aver consultato il modulo locale di failure detector

FD , p sospetta che c abbia fatto crash, e invia un nack a c.

p

 Fase 4: In questa fase, tutti i processi (tranne il coordinatore)

procedono al turno (round) successivo attraverso while-loop. Il

coordinatore aspetta fino a quando non riceve molte risposte di

acknowledgment. La funzione ack(received Qpp: P3 ) seleziona solo

r

messaggi di ack dal sottoinsieme di tutti i messaggi ricevuti ack e nack

 

n

(received_Qpp.P3 ), Se la cardinalità di ack è almeno pari a

r ( 1

) / 2

locked

diciamo che il valore proposto da questa maggioranza è e il

coordinatore “avvia una decisione", altrimenti il coordinatore fallisce

questa occasione e finisce semplicemente questo round. In entrambi i

casi, il coordinatore procede quindi al prossimo round attraverso il

while-loop.

rientro nel 71 Algoritmi Distribuiti

Figura 13 : Algoritmo che risolve il consenso con

72 Algoritmi Distribuiti

L’algoritmo funziona correttamente se sono verificate correttamente le tre

proprietà: Validity, Agreement, e Termination:

 Validity vale perché nessuna delle clausole dell’algoritmo inventa un

valore. Tutti i valori che si verificano in un sistema sono stati

inizialmente proposti da qualche processo.

 Agreement

eement e Terminazione possono essere spiegati in modo intuitivo

Agr

mediante l’esecuzione di tre epoche asincrone, ognuna delle quali pu

generare diversi round asincroni. In epoca 1 tutto è possibile, vale a

dire, ogni valore iniziale potrebbe essere deciso. Nella seconda epoca

un valore diventa “locked": nessun altro valore può essere deciso. Nella

terza epoca i processi decidono il valore “locked".

73 Algoritmi Distribuiti

4.8 Votazione Distribuita

Gli elementi che differiscono la votazione distribuita dal consenso distribuito

sono i seguenti:

 Sincronismo.

 Modello dei guasti prevede la possibilità di generazione di risultati

errati.

4.8.1 Byzantine Agreement

 Con questo nome si indica una famiglia di algoritmi il cui scopo è quello

di raggiungere un consenso anche in presenza di guasti arbitrari

(bizantini), ma introducendo assunzioni di sincronizzazione tra i nodi.

 L’algoritmo prevede l’esistenza di un unico trasmettitore e tutti i nodi

ricevono lo stesso valore da lui inviato (è un modo per realizzare un

broadcast reliable).

 L’algoritmo viene definito in modo che n ricevitori possano raggiungere

un accordo sul valore che è stato trasmesso loro da un trasmettitore.

 Per compiere una votazione distribuita sugli n valori proposti da n nodi

interactive consistency

si usa l’algoritmo di consistenza interattiva ( )

che è composto da n algoritmi interlacciati di byzantine agreement in

cui ognuno degli n nodi si comporta da trasmettitore rispetto agli altri

n-1 nodi.

Definiamo l’algoritmo ZA, algoritmo che si basa sull’autenticazione, deriva

Thambidurai and Park

dall’algoritmo Z [ 1988], ma prima di esporre il

funzionamento introduciamo:

Modello dei guasti Ibridi

Il modello dei guasti che usiamo viene detto modello ibrido, le tre classi di

guasti sono:

 Guasti manifesti

manif esti, ovvero è possibile che un processo invii un valore da

esti

lui calcolato palesemente errato tanto che ogni altro nodo è in grado di

rilevarlo autonomamente.

 Guasti simmetrici, ovvero guasti non rilevabili localmente dai nodi ai

simmetrici

quali è inviato il medesimo valore errato.

 Guasti arbitrari (bizantini), ovvero è possibile che un processo

trasmettitore invii valori diversi a processi diversi e che i processi non

siano in grado di rilevare il guasto localmente.

74 Algoritmi Distribuiti

Sotto questo modello dei guasti, quando un nodo mittente manda un valore v al

nodo ricevitore non guasto, il valore ottenuto è:

 il valore v, nel caso in cui il mittente è non guasto;

 error, se il mittente ha un guasto manifesto.

Assunzioni:

:

Assunzioni

L’algoritmo ZA richiede le seguenti assunzioni:

A1. Ogni messaggio inviato tra due processi non guasti è recapitato

 correttamente.

A2. Il ricevitore conosce il mittente di ogni messaggio.

 A3. I nodi sono sincronizzati, quindi la mancata ricezione di un messaggio è

 rilevata dal ricevente.

A4. I messaggi ritrasmessi non possono essere corrotti.

Proprietà:

:

Proprietà

Le proprietà che l’algoritmo deve verificare sono:

 Validity: se un ricevitore p non è guasto, allora il valore che p associa

al trasmettitore è:

il valore effettivamente inviato nel caso in cui il trasmettitore

 sia corretto o abbia un guasto simmetrico.

Il valore “error” se il trasmettitore ha un guasto manifesto.

 Se il guasto è bizantino non si può fare alcuna assunzione.



 Agreement: dati due ricevitori p e q non fault i valori da loro associati

al trasmettitore sono uguali (hanno la stessa percezione di ciò che il

trasmettitore ha inviato).

 Termination: l’algoritmo termina in un tempo massimo determinato.

L’algoritmo ZA permette la consistenza interattiva (I.C): se ho un processo

guasto gli altri sono in grado di trovare comunque una stima corretta del valore

grazie al meccanismo di votazione interna.

L'algoritmo ZA soddisfa le proprietà sotto le condizioni:

1. n > a + s + m + 1

2. r a

dove:

 n numero di nodi;

 a numero di nodi arbitrariamente guasti;

 s numero di nodi simmetricamente guasti;

 m numero di nodi con guasti manifesti;

 r numero di rounds -1. 75 Algoritmi Distribuiti

L'algoritmo termina sempre a causa dell’ipotesi di sincronia.

Vediamo nel dettaglio il funzionamento dell’Algoritmo

Algoritmo ZA:

ZA(0)

1. Il trasmettitore manda il valore v ad ogni ricevitore.

2. Ogni ricevitore usa il valore ricevuto dal trasmettitore, o il valore

“errore” in caso di guasti manifesti.

ZA(r) r0

1. Il trasmettitore firma v e lo manda ad ogni ricevitore.

2. Sia v il valore ricevuto dal trasmettitore, o il valore “errore” in caso di

p

guasti manifesti, ogni ricevitore p fa partire un algoritmo ZA(r-1) dove

p diventa il trasmettitore e comunica il valore v verso tutti gli altri n-2

p

ricevitori.

3. Per ogni ricevitore p e q, sia v il valore che p riceve da q nel passo 2 di

p

ZA(r-1) o il valore “errore” in caso di guasti manifesti; ogni ricevitore p

esegue localmente la votazione a maggioranza sui v ricevuti (al più

q

n-2).

Il numero di round nell’algoritmo ZA(r) è uguale a r+1.

Innanzitutto c'è un trasmettitore che trasmette il suo valore; se l’algoritmo si

basa su un solo round (r=0), gli altri nodi ricevono e si accontentano.

Se l'algoritmo si basa su più round (r+1), gli altri nodi non si accontentano di

ricevere dal trasmettitore, ma si proclamano trasmettitori facendo partire un

algoritmo di ZA con r round (che è ZA(r-1)) indirizzato agli altri n-2 nodi (cioè

non a se stesso e non al trasmettitore precedente).

Ad esempio, se r=1, quindi ci sono due round, il trasmettitore manda il suo

valore. Ognuno degli altri nodi trasmette il valore a tutti gli altri n-2. I vari

nodi, essendo uno ZA(0) ricevono questo(i) secondo(i) messaggio(i) e non

ritrasmettono. Avendo però ricevuto n-1 messaggi (da tutti i nodi che non siano

il trasmettitore) devono votarli per maggioranza, con le modalità descritte nel

punto 3.

Quindi, il punto 2 serve a far partire un numero di round pari a r+1, il punto 3

(e qui sta forse la fonte maggiore delle possibili incomprensioni) serve a votare

tutti i messaggi ricevuti dall'ultimo round effettuato: notare che questo passo

non è ricorsivo, cioè la votazione viene fatta una volta sola, alla fine di tutti i

round. Quindi, il messaggio originale ad ogni round viene ritrasmesso, e solo

quando giunge alla destinazione dell'ultimo round non viene più ritrasmesso e

viene votato. 76 Algoritmi Distribuiti

Essenzialmente si vuole che il messaggio passi da più nodi possibili.

L’autenticazione serve ad individuare il nodo guasto che ha spedito un

messaggio corrotto.

A causa della velocità attuale dei clock non è possibile assumere la sincronia.

Allo scopo sono nati diversi algoritmi distribuiti di sincronizzazione dei clock.

77 Algoritmi Distribuiti

4.9 Algoritmi di Sincronizzazione in ambito

distribuito

4.9.1 Formalismi e definizioni

Ogni nodo ha un proprio clock, cioè una funzione C(t) con un tempo reale t.

.

C(t) ha un tasso massimo di deriva Siano t e t due istanti di tempo tali per

1 2

cui: 

C

(

t ) C

( t )

t1 t2      

1 1

2 1

t t

2 1

Agreement

Proprietà 1 ( tra Siano C1(t) e C2(t) due clock fisici non

clock):

guasti e sia un valore reale fissato detto scarto. Si dice che i due clock sono

considerati in accordo rispetto allo scarto se vale:

   

t : C (

t

) C (

t

)

1 2 ,

Accurancy

Proprietà 2 ( di un clock): Siano a, b variabili fissate dipendenti

dalle condizioni iniziali di avvio del clock, si dice che un clock fisico C(t) è

accurato se vale:          

(

1 ) t a C

(

t

) (

1 ) t b

   

Questo significa che date due rette e il clock C(t) si

(

1 ) t b

   

(

1 ) t a

mantiene tra le due rette. clock synchronization

Definizione:

izione: un algoritmo di è un algoritmo che soddisfa

Defin

le proprietà 1 e 2.

Un algoritmo di clock synchronization effettua una risincronizzazione ad

intervalli regolari lunghi r. Sia il tasso di deriva, si osserva facilmente che il

massimo scostamento tollerato dalla condizione ideale è pari a ( . r) che

definisce una limitazione superiore per tale scostamento.

78 Algoritmi Distribuiti

4.9.2 Classificazione degli Algoritmi di Sincronizzazione

Ad oggi esistono svariati algoritmi che svolgono il problema della

sincronizzazione in ambito distribuito. Ogni algoritmo differisce principalmente

nel tipo di assunzioni che si fanno per il suo corretto funzionamento nel tipo di

connessione che è richiesta fra i nodi, nella modalità di scambio dei messaggi e

nelle prestazioni: traslazione temporale massima tra due clock non guasti,

massimo clock guasti tollerati. Principalmente si dividono in 3 categorie:

 Algoritmi probabilistici.

 Algoritmi di consistenza.

 Algoritmi a convergenza.

Algoritmi di Sincronizzazione

Convergence Consistency Probabilistic

Averaging Non-Averaging

Mean Median Authentication Broadcast

Algoritmi probabilistici

Questo tipo di algoritmo è in grado di minimizzare la traslazione temporale

massima tra due clock ad un valore piccolo a piacimento ma con una probabilità

di perdita di sincronizzazione crescente.

Il problema di questi algoritmi è, sostanzialmente, che non garantiscono con

probabilità unitaria il mantenimento della sincronizzazione, non vengono quindi

safety-critical

considerati affidabili per sistemi .

Algoritmi di consistenza

Questo tipo di algoritmo considera il valore del clock come un dato qualunque e

interactive

vi applica un algoritmo a più round di consistenza interattiva (

consistency ). Si tratta il problema della sincronizzazione come il problema dei

generali Bizantini. Si vuole creare una condizione di accordo tra i nodi ovvero si

vuole che se due nodi sono non guasti inviano allo stesso trasmettitore il

medesimo valore. Inoltre se il trasmettente è non guasto il valore su cui si

accordano i nodi non guasti è il valore privato del trasmittente.

79 Algoritmi Distribuiti

Algoritmi a convergenza

Gli algoritmi a convergenza si dividono in:

Averaging

1. Algoritmi a media ( )

Non-Averaging

2. Algoritmi non a media ( )

2.

1. Algoritmi a media (Averaging

Averaging)

)

( Averaging

In questo tipo di algoritmi i processi intraprendono una procedura di

risincronizzazione ogni R secondi. Contemporaneamente in una finestra di

tempo centrata (o meno) sull’istante di risincronizzazione attendono i messaggi

degli altri processi. Giunti alla fine della finestra di attesa calcolano il valore

temporale logico a cui convergere con una funzione fault-toleran.

Vi sono due diversi algoritmi, tollerano al più m clock guasti su 3m+1 nodi, che

calcolano tale funzioni in maniera diversa:

 Mediana: si eliminano m valori estremi più alti e più bassi e si calcola

la media dei restanti.

 Media: si effettua la media tra i valori ricevuti a patto che non

differiscano più di una costante dal valore locale.

Tali valori vengono sostituiti dal valore locale. In entrambi gli algoritmi viene

data una stima nel caso pessimo per la massima traslazione temporale dei due

clock.

Questi due algoritmi si basano sul fatto che ogni clock è in grado di conoscere

non il valore locale degli altri clock ma la differenza tra essi, misurata appunto

come ritardo (anticipo) tra il proprio istante di risincronizzazione e l’arrivo dei

messaggi degli altri orologi. Entrambi gli algoritmi fanno l’assunzione della

-limitatezza dei clock coinvolti. Si considera tipicamente una rete di tipo

broadcast. E’ stato anche dimostrato che in assenza di un meccanismo di firma

digitale dei messaggi scambiati 3m+1 nodi il minimo possibile per poter

risolvere il problema della sincronizzazione in presenza di m clock bizantini.

Figura 14:

: Desincronizzazione di due clock non guasti e la presenza di un clock

14

con guasto bizantino. 80 Algoritmi Distribuiti

Non-

- Averaging

ng

Non Averagi

2. Algoritmi non ( )

a media

Come è stato detto precedentemente R è il periodo di risincronizzazione, ogni R

ki 1

secondi viene avviato il nuovo clock locale. In particolare, sia il clock

C ( t

)

durante il k-1 esimo ciclo di risincronizzazione. Alla fine di tale ciclo si avrà che

  

ki 1 . In questo istante il nodo invia in broadcast il messaggio firmato

C (

t

) k R

“round k” quanti sono i nodi. Tutti i nodi fanno la stessa cosa, quindi il nostro

nodo appena ne ha raccolti m+1, incluso il proprio, imposta il suo valore locale

  

ki dove:

C ( t

) k R a

 R è il periodo di risincronizzazione;

 k il round dell’algoritmo;

 

a   

una costante tale che .

     

 

 

Successivamente effettua un relay degli m+1 messaggi ricevuti “round k” agli

altri nodi. Grazie all’uso di firme non alterabili durante i relay, questo algoritmo

tollera t nodi guasti con 2t+1 nodi. Tuttavia il ritardo massimo tra due clock è

maggiore del ritardo dovuto alla trasmissione sulla rete.

Il seguente algoritmo può essere descritto attraverso il seguente pseudocodice:

pseudocodice

if C (t) =k R

k-1 .

then manda in broadcast il messaggio (round k)

//

if (m+1) messaggi ricevuti “round k”

  

ki

then C ( t

) k R a

relay degli (m+1) messaggi a tutti

Figura 15:

: Tolleranza di un clock Bizantine in un sistema a 3 nodi

15 81 Algoritmi Distribuiti

4.10 Guasti software su un sistema distribuito

o

distribuit

Un guasto software in un sistema distribuito si ripercuote su tutti i nodi; per

tollerare guasti software si fa ricorso alla diversità (ho repliche di HW diversi su

cui posso far funzionare software diverso).

Il software usato da questi sistemi sarà composto da:

1. Algoritmi Funzionali.

2. Meccanismi di Tolleranza ai guasti: quest’ultimi permettono di ottenere

la consistenza anche in presenza di guasti HW o guasti agli algoritmi

funzionali.

L’architettura di un software di comunicazione distribuito tra più nodi è così

definito:

 Livello Applicativo (Algoritmi funzionali)

 Middleware (Meccanismi di Tolleranza)

 Software di Base (Comunicazione)

Mentre sul livello applicativo i guasti software possono essere tollerati per

diversità, per gli altri due livelli le cose cambiano; più precisamente il

diversità

middleware non deve contenere guasti, mentre la comunicazione deve rispettare

le assunzioni di guasto che sono state fatte.

Per poter fare la diversità a livello applicativo, è necessario fare più versioni

dello stesso algoritmo (per esempio comprarlo n volte o installarlo in n sistemi

operativi differenti) e questo ha un costo, quindi si preferisce avere il livello

applicativo senza guasti è per verificare tale assenza lo si fa tramite:

 Verifica Formale.

 Testing (non è esaustivo ma molto usato in ambito industriale).

proven in

Anche sul software di base si fa la verifica oppure la prova sul campo (

use ). Commercial Off-t

t he-S

Shelf component)

COTS ( , si riferisce a componenti

hardware e software disponibili sul mercato per l'acquisto da parte di aziende di

sviluppo interessate a utilizzarli nei loro progetti, in questo modo evitano alle

aziende acquirenti di fare tutti i processi di verifica in quanto sono già stati fatti

dalle case produttrici.

Il processo di verifica del software viene scelto in base al costo e all’utilità,

comunque ci sono delle normative da rispettare.

82 Algoritmi Distribuiti

Definizione di Integrità

egrità della Sicurezza: Il grado di fiducia assegnato al

Int

sistema per svolgere soddisfacentemente le funzioni di sicurezza richieste in tutte

le condizioni fissate e all’interno di un fissato periodo di tempo

SIL (Safety Integrity Level):

: Insieme di livelli discreti utilizzati per specificare

Level)

i requisiti di integrità della sicurezza da assegnare ai sistemi:

 SIL 1-4: al valore 4 è associato il livello di integrità più alto mentre al

valore 1 è associato il più basso.

Nelle normative EN 50128, IEC 1508 è definito anche il livello 0 per indicare che

non ci sono requisiti di Sicurezza. Un sistema con SIL 0 è detto sistema non

critico altrimenti è detto critico. Il SIL 0 significa che un guasto su qualche

componente non ha effetto sulla sicurezza, mentre SIL 4 il guasto ha effetto

immediato e diretto sulla sicurezza.

Esempio di descrizione qualitativa del SIL (normativa Def-STAN 00-56)

… claim limits shall be determined for each Safety Integrity Level that give the

inimum failure rate that can be claimed for a function or component of that

level…” Claim Limits

Safety Level Minumum failure rate

Integrity

S4 Remote

S3 Occasional

S2 Probable

S1 Frequent

SIL apportonment

Una volta definito il SIL del sistema, tramite il si definisce il

SIL dei vari componenti, per esempio se il sistema ha un SIL4 ed uso la

diversità, i vari moduli software possono avere un SIL più basso ad es 3 o 2.

Si possono avere due tipi di interazione negativa nel caso in cui un oggetto di

livello di SIL più basso interagisce con uno di SIL più alto (si può indicare così

il il

(A)< (B)):

1. A blocca B vediamo come:

 tramite meccanismi di priorità: un S.O real time da priorità ad A.

 A impedisce a B di ricevere messaggi (DoS).

2. A invia informazioni scorrette a B o scrive scorrettamente sulle variabili

di B. 83 Algoritmi Distribuiti

Per evitare il verificarsi di queste due interazioni negative si adotta

Service Oriented

l’architettura “ ”: questa architettura tende alla coesistenza di

Multi-Level Integrity

moduli (oggetti) con SIL diversi in un sistema secondo la

Policy.

Supponiamo di avere una funzione Object-Oriented: si hanno degli oggetti ai

quali è associato un livello di integrità. Questi oggetti possono avere un solo

livello di integrità o più infatti si parlerà di :

single level object

1. SLO ( ) : ogni oggetto ha un solo livello di integrità

che rimane costante nel tempo ed è pari a quello prescritto dalla

normativa di riferimento. Un oggetto può ricevere dati (essere invocato)

solo da oggetti con un livello di integrità (il) superiore e non può

inviare dati (invocare) a oggetti con livello di integrità (il) superiore.

multiple level object

2. MLO( ) : un oggetto può con livello di integrità

max il

variabile tra un che è il livello di integrità al quale sono stati

min il

validati ed un che è il più basso livello di integrità a cui possono

scendere per ricevere dati da un oggetto con livello di integrità inferiore,

max il il min il

riassumendo MLO[ , , ] dove:

 max il è il livello intrinseco (costante);

 il livello attuale;

 min il è il livello minimo raggiungibile durante l’esecuzione.

Esempio: SLO MLO

4 A max il

=3

3

2 B

1 min il (può cambiare)

Dato un livello di integrità le normative dicono quale deve essere il tipo di test

da fare perché il software sia integro (ad esempio nel campo avionico si ha la

Modified Condition Decision Coverage

copertura del testing a livello MCDC ( )).

Le normative sono rispettate se (consideriamo il caso di due oggetti SLO A e

B):  

il il

A read B (AB) (A) (B)

 

il il

A write B (AB) (A) (B)

 il il

A r&w B (AB) (A) = (B)

84 Algoritmi Distribuiti

Vediamo nel dettaglio cosa succede quando si instaura una comunicazione tra

componenti di tipo diverso o meglio quale sono le normative da rispettare

considerando condizioni, effetti all’invocazione e gli effetti al ritorno

dell’invocazione:

Condizioni A&B (SLO) A & B (MLO)

SLO

 

A read B il(A) il(B) il(A) il(B)

 

A write B il(A) il(B) il(A) il(B)

A r&w B il(A)= il(B) il(A)= il(B)

Effetti A read B min il(B) = il(A); il(B):= maxil(B)

A write B il(B) := min(il(A), max il(B))

Invocazione A r&w B min il(B); il(B):= il(A)

Effetti A read B

A write B

Ritorno A r&w B

C ondizioni A & B (SLO) A (MLO)

(MLO) & B

 

A read B min il(A) il(B) min il(A) max il(B)

A write B il(A) il(B) true

  

A r&w B min il(A) il(B) il(A) min il(A) max il(B)

Effetti A read B min il(B)=min il(A); il(B)=maxil(B)

A write B il(B)= min(il(A), max il(B))

Invocazione A r&w B min il(B)=min il(A);

il(B)=min(il(A), max il(B))

A read B il(A) := min(il(A),il(B)) il(A) := min(il(A),il(B))

Effetti A write B il(A) := min(il(A),il(B)) il(A) := min(il(A),il(B))

Ritorno A r&w B il(A) := min(il(A),il(B)) il(A) := min(il(A),il(B))

validation object il

Esistono dei che alzano il livello di integrità ( ) dei dati, ad

esempio il votatore. In generale se si rispettano le regole in tabella si può far

coesistere più oggetti diversi a diversi livelli di integrità.

Risultato

4 Votatore

3

2 

1 in

85 Logica

5. Logica

5.1 Logica delle proposizioni

Sintassi:             

:= true false p

dove p è una proposizione che può valere true o false.

Questa definizione è ridondante perché ad esempio:

    (  

= )

1 2 1 2

 true

false =

A questo punto possiamo ridefinire la sintassi solo con gli operatori primitivi:

       

:= true p

Semantica:

:

Semantica  {true, 

Data una formula definiamo una funzione S() dove S: false} con

l’ insieme delle formule, per fare questo serve una funzione di valutazione:

si chiama funzione di valutazione una funzione che va dall'insieme P

nell'insieme {true, false} {true,

V : P false}.

 S(false) = false.

 S(P) = V(P). false se S() = true

 S()

S() = = true se S() = false

false altrimenti

   

S( )= S( ) S( ) =

1 2 1 2 true se S( ) = true e S( ) = true

1 2

La naturale estensione di questa logica è il calcolo dei predicati del 1° ordine.

86 Logica

5.2 Logica dei predicati del primo ordine

Sintassi:        

:= true p(exp, ….., exp)

 D.

Con exp:=x f(exp , ….., exp ) dove x è una variabile e f : D

n

1 n

In questo caso p non è una proposizione ma è il predicato:

{true,

P : D false}

n

Inoltre possiamo introdurre un quantificatore tra gli operatori logici:

 ,

quantificatori ed denominati rispettivamente il quantificatore universale e

il quantificatore esistenziale.

x  

Esempio: : (esiste x per cui è vera).

lega la variabile x variabile x è libera

La negazione di una formula universale è una formula esistenziale e viceversa:

  

x x

  

x x

Inoltre posso definire:

 true.

false =

    (  

= )

1 2 1 2

 x  x  

: = :

Semantica:

Per definire la semantica dobbiamo introdurre la struttura di interpretazione

  

=(D, V, , ) dove:

 D è il dominio di interpretazione delle variabili.

 V è la funzione di valutazione delle variabili.

   D).

è la funzione di interpretazione delle funzioni : F(D

n

   {true,

è la funzione di interpretazione dei predicati :P(D false})

n

A questo punto definiamo la semantica come :

 S’: exp D

  

S : {true, false} 87 Logica

In particolare:

 S’(x) = V(x) valutazione di x

 

S’(f(exp , ….., exp )) = (f)(S’(e ),……,S’(e ))

1 n 1 n

 S(true) = true

 S()

S() =

   

S( ) = S( ) S( )

1 2 1 2

 (p)(S’(e

S(p(e , ….., e )) = ), …., S(e ))

1 n 1 2

 )

S(x : = ….

x  ,

poiché : lega le occorrenze di x in x non ha valore in V, infatti

solo le x libere hanno un valore in V, allora si può concludere dicendo:

y 

se D : S() = true allora true

 

[V/V [x y]]

S(x =

)

 altrimenti false

Possiamo ridefinire la semantica attraverso la relazione di soddisfacibilità ( |= ):

 

soddisfa

 

|= =   

è un modello per quando è vera

Ottenendo così:

  |= true sempre

    

|= se solo se |=

         

|= se solo se |= |=

1 2 1 2

   (p)(

|= p(e , ….., e ) se solo se |= S’(e ), …., S(e ))=true

1 n 1 2

  x  ’ ’   ’ , )   

|= : sse : |= = (D, V, V’ = V [xy] yD

x

Esempio: Consideriamo la formula: : p(x , f(x , x))

1 1

Consideriamo:

 p come >

 f come +

 D = \ {0}

+

x

Dunque ho : x > x + x = false sempre, dunque la struttura presa in

1 1 .

considerazione non è un modello per

Se invece consideriamo:

 p come >

 f come +

 D =

x

Dunque ho : x > x + x = true, dunque la struttura presa in considerazione

1 1

.

è un modello per 88 Logica

5.3 Logica Modale

Nell'ambito della logica formale, si indica come logica modale una qualsiasi

logica in cui è possibile esprimere il "modo" in cui una proposizione è vera o

falsa (calcolo proposizioni). Generalmente la logica modale si occupa dei concetti

di possibilità e necessità, infatti, si ha che p è necessariamente vera ( o p è

)

necessità

possibilmente vera ( p).

La possibilità o necessità si riferisce all’esistenza di “mondi”, comunque

raggiungibili, in cui p possa o debba essere vera:

 p significa che in tutti i mondi raggiungibili p è vera.

 

p significa che un mondo raggiungibile in cui p è vera.

 

p 

Proprietà della dualità: = p

Esempio: 

( p = true) , W raggiungibile in cui p è vera

2

p = false

W

1 p = false

W ( p = true)

3

W

2

p = true

( p = true)

Sintassi: 

         

:= true p

Semantica:

:

Semantica

Per definire la semantica dobbiamo introdurre la struttura di interpretazione

 = (W, R, V) dove:

 W è l’insieme dei mondi.

 

R è la relazione di raggiungibilità tra mondi R W W.

×

 V è la funzione di valutazione delle proposizioni V : P W{true, false}

×

89 Logica

In particolare consideriamo w il mondo di partenza :

0

 ,w = true sempre

0

 ,w =    

se solo se

0

 ,w =    =   = 

se solo se ( ) ( )

0 1 2 1 2

 ,w = p se solo se V(p, w )=true

0 o

 ,w =  w   = )

sse W: (w , w) R, V(, w) = true cioè (,w

0 o 

Spesso si trascura il riferimento alla struttura di interpretazione scrivendo

= =).

(w ) invece di (,w

0 0

Le proprietà della relazione di raggiungibilità considerate inducono degli assiomi

di equivalenza tra formule della logica:

:

1. Transitiva w R w , w R w w R w :

0 1 1 2 0 2

 

  

i)  

  

ii) w 

:

2. Riflessiva W, w R w:

  

i) 

  

ii)  

’  ’

iii)  

’  ’

iv)

3. :

Riflessiva e Transitiva (assorbimento delle modalità)

     

      )

= ( e

     

       

= ( e )

CASO 1: Supponiamo che W sia infinito e numerabile, con la relazione di

  

 

R w , w

raggiungibilità della forma , che non è altro che una catena

i i 1

i 0

lineare: ...........

w

w w 2

0 1

 

   

Allora vale sia (se è vera in tutti i mondi raggiungibili allora esiste

 

    

un mondo in cui è vera) che (se esiste un mondo in cui è vera

allora è vera in tutti i mondi).    

  )   )

Dunque le due modalità si equivalgono, cioè ( e ( quindi

 

 .

posso affermare che = 90 Logica

In questo caso si usa spesso un unico simbolo che si legge anche “next”



perché indica che p è vera nel prossimo mondo raggiungibile.

p  

p   p

Vale ancora la dualità = p =

p

Esempio: ...........

w

w w 2

0 1 p

p

è vero in w se p è vera in w

P 0 2

CASO 2: Consideriamo il caso di W infinita e numerabile con

  

 

R w , w riflessiva e transitiva (chiusura transitiva), non vale più la

i i 1

i 0  

 ,

proprietà = mentre vale :

   

   

 

   

Per la proprietà riflessiva e transitiva abbiamo:

 

  

=

 

  

=

Dove: 

 :  .

significa che mondo prossimo (incluso se stesso) in cui è vera

 :  .

significa che un mondo (incluso se stesso) in cui è vera

91 Logica

5.4 Logica Temporale

emporale

T

Supponiamo di considerare un dominio temporale; l’insieme dei mondi è il

cosiddetto tempo discreto dove ogni mondo è un istante di tempo. Gli istanti di

tempo t ,t ,…..t sono chiamati STATI.

0 1 n

Il sistema evolve attraverso vari stati quindi una sua evoluzione è una

successione di stati (o traccia o storia):

t t t t

0 1 2 ...........

w

w w 2

0 1

Nella logica temporale:

 

  

diventa ALWAYS (sempre); quindi indica che è vero d’ora in

=  t 

poi: t se solo se t il tempo t=

0 0

 

  

diventa EVENTUALLY (prima o poi) quindi indica che sarà

=  t 

vero prima o poi: t sse t il tempo t=

0 0

 

L’operatore NEXT

T non subisce cambiamenti, quindi indica che

 

NEX

sarà vero nell’istante successivo.

Logica temporale si divide nelle seguenti categorie:

1. Ramificata o Lineare.

2. Numero finito o Numero Infinito di stati.

3. Tempo passato o Tempo futuro.

4. Tempo continuo o tempo discreto.

92 Logica

5.4.1 Logica temporale Lineare con numero infinito

o di stati

infinit

(LTL)

Dominio temporale costituito da una sequenza infinita e discreta di dove

,

,

i  S è in relazione S e si indica S R S .

i i+1 i i+1 ...........

........... S

S S n

0 1

La logica LTL definita dai seguenti o peratori temporali:

  

Globally

1. L’operatore Always (detto anche indica che è vero

)

d’ora in poi. 

 

Future

2. L’operatore Eventually (detto anche indica che sarà

)

vero prima o poi. 

3. L’operatore Next indica che sarà vero nell’istante successivo, da

 .

notare che il suo duale è ancora se stesso: =

  

4. L’operatore Until : esiste uno stato futuro in cui vale , e in



1 2 2

tutti gli stati precedenti vale .

1

  (  

5. L’operatore Precede = ) sta ad indicare che

  

1 2 1 2 1

 

precede : non è possibile che esista uno stato futuro in cui vale ,

2 2

preceduto da stati in cui non vale .

1 

     

6. L’operatore Unless

nless = ( ) sta ad indicare che è

 

1 2 1 2 1 , 1

sempre vera a meno che non diventi vera 2

Sintassi:            

:= p   

Attraverso l’operatore U è possibile definire l’operatore eventually ( ) nel

 .

seguente modo: = true 

Si può dire che :

 è l’ operatore derivato da .

 

 

è l’operatore derivato da , quindi da infatti: ¬ ¬

Semantica:

:

Semantica 

Un modello LTL è una quintupla = (S, S , R, V, P) dove:

0

 S è insieme infinito di stati,

 

S è lo stato iniziale (S S)

0 0

,

 i 

R è la relazione : S R S

i i+1

 

V : P S {true, false}

×

 P sono le preposizioni atomiche.

93 Logica

, =  

Fissato la relazione di soddisfacibilità S ( soddisfa in S) è definita

):

come (per semplicità di notazione omettiamo

 = 

S p, p P se solo se V(p, S)=true.

 = , S = 

S se solo se

 =    =   = 

S , se solo se (S ) (S )

1 2 1 2

 = , S’: 

S

S se solo se = chiusura transitiva di R, S R , S’=

R '

 = , S’: 

S

S se solo se = chiusura transitiva di R, S R , S’=

R '

Nel caso più specifico, per i singoli stati S :

i

 = 

S p, p P se solo se V(p, S)=true

i

 = , S = 

S se solo se

i

 =   =   = 

S , se solo se (s ) (S )

i 1 2 1 2

 = , k  = 

S se solo se i: S

i k

 = , k  = 

S se solo se i : S

i k

 = = 

S se solo se S

,

i i+1

 =   k  =  i  = 

S , se solo se i : S e k’ k : S

i 1 2 k 2 k’ 1

Alcune tipiche formule LTL che esprimono proprietà interessanti possono essere

le seguenti:

 y > n+1, proprietà Invariante (è sempre vero).

 Liveness

p, proprietà (prima o poi succede qualcosa).

 bad, Safety

proprietà (non è mai vero che qualcosa è scorretto).

 

  Liveness

(request reply), proprietà (se faccio una richiesta

prima o poi risponde).



 Infinitel

ely

y often

Infinit el

p (GFp), proprietà (p è vera infinitamente spesso).



 Eventually always

p (FGp), proprietà (prima o poi arrivo in uno

stato tale che da li in poi risulta sempre vero p).

Fairness:

L’ infinitely often è usato per definire la proprietà di

 

request replay

k k

se richiedo infinitamente spesso, infinitamente spesso ottengo risposte.

94 Logica

Esempio: p è vera in ogni stato pari

p p p

S S S S S

0 1 2 3 4

Formule che esprimono la condizione:

 

(p non va bene, perché vale anche per i dispari.

p)

  

(p non va bene, è sempre falsa.

p p)

 

X = p questa formula va intuitivamente bene, ma non è una



formula della logica, è un’equazione sulla logica, a cui bisogna dare

soluzione.

Definizione: Se x = f(x) allora x è un Punto Fisso di f.

true Sottoreticolo: insieme

massimo delle formule che sono

punti fissi di f, che ha

1 un massimo e un min.

Reticolo: 

2 minimo

insieme di

tutte le

formule  false

 

L’ ordinamento dell’implicazione ( ) costituisce un reticolo, in cui ho:

1 2

   

false (minimo del reticolo)

   

true (massimo del reticolo)

Definiamo: x

1. Il minimo punto fisso all’interno del sottoreticolo è f(x), vale che:

.

     i

x f ( x ) f ( false )

i 0 x

2. Il massimo punto fisso all’interno del sottoreticolo è f(x), vale che:

.

     i

x f ( x ) f ( true )

i 0

95 Logica

Calcoliamo min e max per la formula x = p x

Ricordando che x = f(x) = p quando x è un punto fisso di f

x

 

f (x) = p x

0

 

f (x) = p (x)

f

1 0

 

f (x) = p (x)

f

2 1

 : x

Calcoliamo il minimo: f(x):

.

 

x = p = false

false

0

 

x = p = false

x

1 0

 

x = p = false

x

2 1

 

Andando avanti otteniamo sempre false, quindi si può concludere dicendo:

x x 

= = false

x

f(x) p

 

x

Calcoliamo il massimo: f(x):



 

x = p = (dipende da p)

true

0

  

x = p = (dipende da p)

(p true)

1

   

x = p = (dipende da p)

(p (p true))

2

  x 

continuando cresce all’infinito; la formula che vogliamo è p x



(massimo punto fisso) è una formula infinita, cioè non rappresentabile in modo

finito con gli operatori della logica.

x xf(x).

Definizione: f(x) =

.

Possiamo avere una logica temporale con punto fisso definito solo

lineare

x x

attraverso e f(x), oppure solo con e f(x) perché da questi due

 

 

posso derivare . 96 Logica

Esercizio: Vogliamo dimostrare la seguente uguaglianza :

x     

( =

x) 

2 2 1 2

  

dove ( = f(x)

x)

2 2 

2 

È vera su 2

  

x = ( =

false)

0 2 1 2  

È vera su

2 2

 

x = ( ) =



1 2 1 2   

È vera su e al

1 2 1

prossimo stato è vera

2

2

     

x = ( ( ))) =

( 

2 2 1 2 1 1 1 2

  

1 1 2

 

Come si evince si ha sempre che 

1 2

97 Logica

5.4.2 Logica

ogica temporale Lineare con numero finito di stati

L ,

i 

Il dominio temporale costituito da una sequenza finita di dove

,

S è in relazione S e si indica S R S .

i i+1 i i+1 ........... S

S S n

0 1

Appare subito ovvio che non vale più che il duale dell’operatore è ancora se

p,

stesso = questo perché se valesse (usiamo provvisoriamente i

p

 

simboli ’ e ’ per denotare il next e il suo duale):

 

’p stato successore vale p.

 

’ stato successore per cui vale p.

Per la sequenza finita vale :

 = p

S ’p, (debole): non raggiungo nessun nodo in cui è vero quindi

n

è soddisfatta.

 = p

S ’, (forte): non esiste alcun nodo raggiungibile in cui è vero

n

quindi è soddisfatto.

Introduciamo due operatori NEXT: Forte e DEBOLE

  ~

  

= si può indicare anche nel seguente modo =

 

Per un generico stato S ha che :

i

 = = 

S se solo se i < n, S



i i+1

 = = ) 

S se solo se (i < n, S (i = n)



i i+1

Inoltre:

 = true all’ultimo stato.

false

 = false.

false

 =

S S = S (stato finale).

false  n 98 Logica

5.4.3 Logica temporale con Tempo passato

Consideriamo il caso di non avere un tempo iniziale, cioè ammettiamo di avere

un passato, abbiamo nuovi operatori simmetrici a quelli appena visti:

 p tutti gli stati precedenti è vera p.

 p esiste uno stato precedente in cui è vera p.

 p nello stato precedente p è vera (PAST).

Introduciamo l’operatore Since :

    

: dal momento in cui è stato vero è vero Si evince che il

1 2 2 1 .

Since è il corrispettivo al passato dell’Until.

Ai fini pratici, si può spesso esprimere la logica del passato attraverso la logica

del presente.

E sempio: se accade p, allora è accaduto q si può esprimere come:

sempio   (q

p q, dove p q è equivalente a cioè q p.

p) 

5.4.4 Logica temporale Continua e tempo reale

Il tempo si è considerato finora discreto; nel caso di tempo continuo si perde il

concetto di tempo prossimo (NEXT), possiamo solo dire che un tempo è

 

maggiore dell’altro; si mantengono gli operatori .

Inoltre vale che t R t’ t t’

Questa logica è interessante quando si vuole quantificare puntualmente il

tempo, cioè indicare nelle formule precisi istanti o intervalli di tempo.

E’ evidente la relazione di questo aspetto con i sistemi “real-time”.

Nel discreto esprimere sotto forma di formula la seguente operazione: “se viene

fatta una richiesta la risposta viene data dopo 3 unità di tempo “ può essere

fatto nel seguente modo:  

(request replay)

99 Logica

Mentre per un operazione del tipo “se viene fatta una richiesta la risposta viene

data entro 3 unità di tempo”, si esprime nel seguente modo:

   

(request replay replay replay)

E’ ovvio che voler indicare un istante di tempo preciso, diciamo t, richiede una

specifica formula con t operatori di next, perdendo quindi di generalità. Sono

state proposte varie logiche come la ITL (interval logic) e la RTL (real time

temporal logic) che usano appositi operatori per indicare intervalli o istanti di

tempo. Per esempio nella ITL l’operatore eventually si indica nel seguente modo

 p e sta a significare che p è vera nell’intervallo 3-5.

(3-5)

Questa classe di logiche temporali può essere definita sia in un dominio

temporale discreto che continuo.

5.4.5 Logica temporale Ramificata (CTL)

Partendo da una macchina a stati posso ottenere un albero (una struttura

ramificata), attraverso l’operazione di Unfolding “srotolamento” della macchina

a stati: S

1

S

0 S

2

Con la logica CTL è possibile esprimere formule logiche su cammini (ossia

sequenze di transizioni di stato) a partire da un determinato stato iniziale. La

caratteristica principale di questa logica è che ogni formula deve essere premessa

da un quantificatore di cammino, per cui ogni formula viene sempre riferita

all’insieme dei cammini a partire da uno stato iniziale. La logica CTL

computation tree logic

( ) è definita dagli operatori temporali (next), che

p

significa che una certa proprietà p si verifica nell’istante successivo, p

eventually, p si verifica in futuro, always, p è sempre verificata,

p

p q (until) e p q (precede). Questi operatori non possono però essere

 

utilizzati liberamente: essi devono essere sempre prefissi da un quantificatore di

cammino, si indica con il quantificatore

antificatore universale (per tutti i cammini) e

 qu

con il quantificatore esistenziale (esiste almeno un cammino).

 100 Logica

Sintassi:

La logica CTL è definita per mezzo di due categorie sintattiche:

1. Formule di Stato ().

2. Formule di Cammino ().

Formule di Stato:

Dato p AP (insieme di proposizioni atomiche) si ha che:

         

:= true p  

Formule di Cammino

     

:=    

 ,

Esempio: true è una formula di cammino e vuol dire che prima o poi vale

  

questo non è altro che Eventually true =

 

Semantica:

Una struttura di Kripke M su un insieme di proposizioni atomiche AP è una

,L)

4−upla M = (S, S , dove:

0

1. S è un insieme finito di stati.

2. S S è l’insieme degli stati iniziali.

0

 

3. S×S è la relazione di raggiungibilità.

4. L : S 2 è una funzione che assegna ad ogni stato un’etichetta

AP

che contiene le proposizioni atomiche vere in quello stato.

Semantica per le Formule di Stato:

 =

S true sempre.

 = 

S p, se solo se p L(S).

 =      

S (S= ) (S= )

1 2 1 2

 =  S= 

S 

 =    =  

S Path(S), dove è un cammino e Path(S)

 

restituisce tutti i cammini a partire da S

 =    = 

S Path(S),

 

Semantica per le Formule di Cammino:

  =   = 

= S , S , S , ….., S ,….. S

  0 1 2 n 1

  =     i =   k =

= S , S , S , ….., S ,….. : S < i S

 

1 2 0 1 2 n i 2 k

  =  i = 

= S , S , S , ….., S ,….. : S

  0 1 2 n i

  =  i = 

= S , S , S , ….., S ,….. : S

  0 1 2 n i

101 Logica

Ad esempio consideriamo le seguenti formule:

 esiste un cammino in cui ho una risposta.

(reply):

 per ogni cammino ho una risposta.

(reply):

Alcune tipiche formule CTL che esprimono proprietà interessanti possono essere

le seguenti:

 (reply) = (reply)

 (reply) = (reply)

 (reply) = (reply)

  tutte le volte che c’è una richiesta il sistema

(request reply)):

risponde

  almeno in un caso il sistema risponde.

(request (reply))

 [p q] p precede q

  vale infinitamente spesso su ogni cammino

():

 

da ogni stato è possibile raggiungere lo stato

(): not

Come si può notare il si applica solo alle formule di stato, che consentono la

dualità. 102 Logica

5.4.6 CTL*

Come detto precedentemente la logica Temporale si divide in:

 logica temporale lineare (LTL), dove gli operatori sono forniti per la

descrizione di eventi lungo un unico percorso.

 logica temporale ramificata (CTL) dove gli operatori temporali

quantificano i percorsi che sono possibili da un dato stato.

La computation tree logic CTL* combina la logica temporale lineare e la logica

temporale ramificata, in pratica rimuove la distinzione tra formula di stato e

formula di cammino. Si può affermare che CTL* comprende sia la CTL che la

LTL.

In questa logica un quantificatore di cammino può essere messo come prefisso in

una asserzione composta da combinazioni arbitrarie di operatori temporali

lineari

1. Quantificatore di cammino

 quantificatore universale “per tutti i cammini”

 quantificatore esistenziale “esiste almeno un cammino”.

2. Operatori temporali lineari

 (next)

p

 (Future)

p

 (Globally)

p

 p q (Until)

Sintassi:

La sintassi delle formule di stato è data dalle seguenti regole:

 

Se p AP, allora p è una formula di stato.

 

Se f e g sono formule di stato, allora (f) e (f g) sono formule di

stato.

 Se f è una formula di cammino, allora è una formula di stato.

(f)

Due regole necessarie per specificare la sintassi delle formule di cammino sono:

 Se f è una formula di stato, allora f è anche una formula di cammino

 f, 

Se f e g sono formule di cammino, allora (f g), e (f g) sono

f, 

formule di cammino 103 Logica

Semantica

mantica Formule Stato:

Se di Stato

Se f è una formula di stato, la notazione M,s |= f significa che f vale nello stato

s nella struttura di Kripke M.

Assumiamo f e f siano formule di stato e g una formula di cammino. La

1 2

relazione M,s |= f (omettiamo M) è definita induttivamente come segue :

 =

s true sempre.

 = 

s p p L(S).

 =  =  =

s f f (S f ) (S f ).

1 2 1 2

 = f S =

s f .

1 1

 =    =  

s Path(S) dove è un cammino e Path(S)

() 

restituisce tutti i cammini a partire da S.

 =    = .

s Path(S)

() 

Semantica Formule di Cammino: 

Se f è una formula di cammino, la notazione M, |= f significa che f è valida

lungo il cammino nella struttura di Kripke M.

Assumiamo g e g siano formule di cammino e f una formula di stato. La

1 2

|=

relazione M, f è definita induttivamente come segue :

  = 

f s è il primo stato di e s= f

  = g  = g

1 1

  =  = =

g g (S g ) o (S g )

1 2 1 2

  =  =

g g

  1

1 1

  =   =   =

g g esiste un k 0 : g e for 0 j k, g

  k j

1 2 2 1

CTL è un sottoinsieme limitato di CTL* che autorizza solo gli operatori di

logica temporale ramificata, ciascuno degli operatori tempo lineari e

 

deve essere immediatamente preceduta da un quantificatore di cammino (A, E).

Esempio: (p)

LTL consiste di formule se e solo se f è una “path formula” nella quale le sole

f

“state formula” ammesse sono le proposizioni atomiche.

Esempio: (p) s |= f se e solo se s |= f

LTL semantics CTL* semantics

104 Logica

5.5 Comparazione tra LTL, CTL e CTL*

Le tre logiche LTL, CTL, CTL* hanno potere espressivo differente, per esempio:

 In CTL non esiste un equivalente alla formula LTL e

(FG) (GF).

 In LTL non esiste un equivalente alla formula CTL ().

 

La disgiunzione è una formula CTL* che non si può

(p) (p)

esprimere né in LTL né in CTL.

Esempio: La proprietà FAIRNESS è esprimibile in LTL ma non in CTL perché

non esiste una formula equivalente in CTL della formula (LTL).

p

La fairness in LTL è:

 : se è vero infinitamente spesso p, allora è vero infinitamente

p q

spesso q. 105 Model Checking CTL

6. Model Checking CTL

6.1 L’algoritmo di Checking

Il problema del Model Checking si può definire come il problema, data una

struttura di Kripke M e una formula f (che esprime una proprietà desiderata per

M), di verificare se M soddisfa f (M |= f), cioè se M è un modello per f.

Un algoritmo che risolve il problema del Model Checking per la logica CTL è

stato definito da Clarke, Emerson e Sistla; l'algoritmo etichetta ogni stato di M

con le sottoformule di f che sono soddisfatte in quello stato, iniziando con le

sottoformule di lunghezza 0 (i predicati atomici), per poi passare a quelle di

lunghezza 1 (in cui cioè un solo operatore logico viene applicato ai predicati

atomici), poi a quelle di lunghezza 2 (in cui cioè un operatore logico viene

applicato a formule di lunghezza 1), ecc..

Di seguito riportiamo la versione semplificata di questo algoritmo di

etichettamento per le sole formule base della logica, cui si possono ricondurre

tutte le altre. Questo algoritmo assume che tutti gli stati siano già etichettati

con le proposizioni atomiche che vi valgono; la formula da verificare è p ,

0

mentre S è lo spazio degli stati su cui verificarla:

for i =1 to length(p )

0

for each subformula p of p of length i

0

case on the form of p

p = P, an atomic proposition /* nothing to do */

p = q and r: for each s in S

if q in L(s) and r in L(s) t hen add q and r to L(s)

end

p = ~q: for each s in S

if q in L(s) then add ~q to L(s)

end

p = for each s in S

q: if(for some successor t of s, q in L(t)) then add EXq to L(s)

if

end 106 Model Checking CTL

p = r]: f or each s in S

[q  if r in L(s) then add r] to L(s)

[q 

end

for j = 1 to card(S)

for each s in S

if q in L(s) and (for each successor t of s, r]

[q 

in L(t)) then add r] to L(s)

[q 

end

end

p = r]: for each s in S

[q  if r in L(S) then add r] to L(s)

[q 

end

for j = 1 to card(S)

for each s in S

if q in L(s) and (for some successor t of s, r]

[q 

in L(t)) then add r] to L(s)

[q 

end

end

end of case

end

end

Il risultato del model checking si evince dalle formule che etichettano lo stato

iniziale: la formula è verificata se e solo se etichetta lo stato iniziale.

L’algoritmo ha complessità |S| dove:

|T| ||

 

 |S | numero di stati.

 |T| transizioni uscenti da ogni stato

 || lunghezza della formula (||

Tramite ottimizzazione si può arrivare a |S|)



Quindi CTL ha un algoritmo di model checking lineare con lo spazio degli stati.

Questo è importante poiché nella pratica lo spazio degli stati tende ad esplodere

esponenzialmente. Per risolvere tale problema si è passati dalla rappresentazione

esplicita dello spazio degli stati ad una rappresentazione implicita (simbolica).

Questo viene fatto tramite i binary decision diagrams (BDD).

107 Model Checking CTL

Dato che CTL* ha più potere espressivo di CTL e LTL, perché non si usa?

L’algoritmo di model checking CTL* ha complessità:

dove k è il grado di annidamento dei e degli ( ha

 

 ((|| )

k

|S|)

 annidamento pari a 2).

che confrontata con quella del CTL, ha al suo interno un fattore di

esponenzialità che lo rende meno efficiente.

108 Model Checking CTL

6.2 Algoritmo del Model Checking Simbolico.

Symbolic Model Checking Ordered Binary Decision

L’algoritmo di utilizza gli

Diagram ( OBDD) come rappresentazione simbolica di transizioni e insiemi di

stati.

6 .2.1 Ordered Binary Decision Diagrams (OBDD)

Binary Decision Tree

Per definire l’OBDD dobbiamo innanzitutto definire il

Binary Decision Diagram

(BDT) e il (BDD) infatti possiamo schematizzare nel

seguente modo: BDT BDD OBDD

 

Binary Decision Tree (BDT)

Una funzione booleana in più variabili si può rappresentare tramite un albero

binario di decisione. I nodi non terminali fanno riferimento alle variabili (la

stessa per tutti i nodi allo stesso livello). I livelli sono tanti quante sono le

variabili. Ogni nodo non terminale ha due archi (low e hight) uscenti etichettati

rispettivamente 1 e 0 (valori possibili della variabile che etichetta il nodo). Le

foglie sono etichettate con 1 e 0. Il valore della funzione sui suoi input si ottiene

attraverso i nodi di decisione dell’albero dalla radice fino alle foglie.

E s empio: Binary Decision Tree per un comparatore a due bit, data dalla

seguente formula:   

f(a , a , b , b )=(a b ) (a b )

1 2 1 2 1 1 2 2

È mostrato nella figura sottostante: 109 Model Checking CTL

Binary Decision

ision Diagrams (BDD)

BDD)

Dec (

I BDT hanno dimensione esponenziale nel numero di variabili. Per compattare

la rappresentazione dobbiamo eliminare le ridondanze:

 Combinare tutti i sottoalberi isomorfi.

 Eliminare tutti i nodi con figli isomorfi.

Si ottiene così un D.G.A (grafo diretto aciclico) chiamato BDD. A questo

punto non rimane che trovare una rappresentazione canonica.

Ordered Binary Decision Diagrams (OBDD)

(O BDD)

L’OBDD è una rappresentazione canonica di una funzione booleana, dove

l’ordinamento delle variabili avviene nel seguente modo:

 In ogni cammino dalla radice alle foglie si mantiene lo stesso ordine,

senza ripetizioni.

 Non tutte le variabili devono comparire lungo un cammino.

 Non devono esserci sottoalberi isomorfi o vertici ridondanti nel

diagramma.

Se usiamo un ordine a < b < a < b per il comparatore, otteniamo il seguente

1 1 2 2

OBDD: 110 Model Checking CTL

Se usiamo un ordine a < a < b < b per il comparatore, otteniamo il seguente

1 2 1 2

OBDD:

6 .2.1.1

.1 Logica operazionale OBDD:

.2.1

 f(a,b,c,d)

Negazione Logica:

Si sostituisce ciascuna foglia con la sua negazione.

 

Congiunzione logica: f(a,b,c,d) g(a,b,c,d)

Si usa l’espansione di Shannon:

    

      

f g a f g a f g

a a

a a

Divide il problema in due sottoproblemi. Questo significa

 a

costruire un albero la cui prima variabile è , il ramo 0 porta

all’OBDD del sottoproblema sinistro, il ramo 1 porta all’OBDD

del sottoproblema destro. I sottoproblemi si risolvono

ricorsivamente.

 a

Quantificatore Booleano: : f(a, b, c, d)

Per definizione

  

  

 

a : f f f

 

a

a

a

: sostituire tutti gli nodi con il sotto-albero sinistro.

 f (

a

, b

, c

, d

) a a

: sostituire tutti gli nodi nel sotto-albero destro.

f

(

a

, b

, c

, d

)

 a

Utilizzando le operazioni appena viste, si può costruire un OBDD per funzioni

booleane complesse. 111 Model Checking CTL

6.2.2 Rappresentazione delle transizioni con OBDD

Come detto prima il Symbolic Model Checking utilizza gli OBBD come

rappresentazione simbolica di transizioni e insiemi di stati, ma come si

rappresenta le transizioni di stato di un grafo con OBDD?

Si supponga che il comportamento del sistema è determinato dalle variabili

booleane di stato: v ,v , v ,…….v

1 2 3 n

La relazione di transizione T sarà data come una formula booleana in termini di

variabili di stato: T(v ,v , v ,…….v v’ ,v’ , v’ ,…….v’ )

1 2 3 n, 1 2 3 n

dove v ,v , v ,…….v rappresenta lo stato attuale e v’ ,v’ , v’ ,…….v’ rappresenta

1 2 3 n 1 2 3 n

il prossimo Stato.

A questo punto possiamo rappresentare T in OBDD.

Supponiamo di avere la seguente struttura di Kripke:

La relazione di transizione può essere rappresentata sotto forma di formule

Booleane, nel seguente modo:

 b           b’)

(a a’ b’) (a b a’ b’) (a b a’

Poi si trasforma tale formula booleana in OBDD

112 Model Checking CTL

Consideriamo la seguente formula f = EXp .

Introduciamo le variabili di stato e la relazione di transizione:

v’ 

f(v) = [T(v,v’) p(v’)]

A questo punto si calcola l’OBDD per la relazione prodotta sul lato destro della

formula.

Ora consideriamo la formula f = EFp e valutiamo il punto fisso utilizzando

OBDDs: 

U U

EFp = Lfp .p EX dove Lfp (minimo punto fisso).

Introducendo le variabili di stato e la relazione di transizione otteniamo:

 v’  

U U

EFp = Lfp .p(v) [T(v,v’) (v’)]

A questo punto si calcola la sequenza:

U U U 

(v), (v), (v),

0 1 2

fino alla sua convergenza. U

La convergenza può essere rilevata dato che gli stati (v) sono rappresentati

i

come OBDDs. 113

Automi di Büchi & Model Checking LTL

7. Automi di Büchi & Model

Checking LTL

7.1 Problema del Model Checking

Dato un modello M, uno stato s ed una proprietà espressa con una formula LTL

, determinare se 

M, s |=

Soddisfacibilità formule LTL Model Checking per LTL

Decidibile decidibile

Il Model Checking LTL è basato su una variante degli automi a stati finiti,

chiamati Automi di Büchi

7.2 Automa

ma a stati finiti

Auto

Definizione:

: Un Automa a stati finiti etichettato (LFSA) è una tupla

Definizione

,

(, S, S , F, L):

0

  è un alfabeto di simboli.

 S è un insieme finito di stati.

 

S S è l’insieme di stati iniziali.

0

  : S S è la funzione di transizione di stato.

 

F S è l’insieme di stati finali.

 

L : S è la funzione di etichettatura degli stati.

Definizione: Un LFSA è deterministico sse

  a  

1. |{s S | L(s) = a}| 1

0

  a  , s 

2. |{s (s) | L(s ) = a}| 1 S

 114

Automi di Büchi & Model Checking LTL

Esempi determinismo

eterminismo

d

Esempi di non determinismo

7.2.1 Linguaggio accettato 

Definizione: Un run per un LFSA è una sequenza finita = s s . . . s tale che

0 1 n

 0 

s S e s s i < n

0

0 i i+1 

accepting

Definizione: Un run è detto se s F

n

Definizione:

e: Una parola w = a a . . . a è accettata sse esiste un accepting

Definizion 0 1 n

 0   )

run = s s . . . s : L(s ) = a i < n (a

0 1 n i i i

 ,

Definizione: Se si indica con l’insieme di tutte le possibili parole finite su

il linguaggio accettato dall’LFSA A è:

*

= { w | w è accettata da A }

(A) 115

Automi di Büchi & Model Checking LTL

Esempio linguaggio accettato (c*ab ) :

+ +

7.3 Automa di Büchi

Definizione di Automa di Büchi: Un Automa di Büchi etichettato (LBA) è un

Büchi

LFSA che accetta parole di lunghezza infinita invece che di lunghezza finita

Definizione:

izione: Un run per un LBA è una sequenza infinita = s s . . . tale che

Defin 0 1

 i

s S e s s 0

0

0 i i+1 

Definizione: Sia lim() l’insieme di stati che occorre in infinitamente spesso.

  

Allora è un accepting run sse lim() F 

Poiché il numero di stati dell’automa è finito, mentre la sequenza ha

lunghezza infinita, sicuramente lim()

7.3.1 Linguaggio accettato

Definizione: Una parola w = a a . . . è accettata da un LBA sse esiste un

0 1

accepting run  i   )

= s s . . . tale che L(s ) = ai 0 (a

0 1 i i

Definizione: Se si indica con l’insieme di tutte le possibili parole infinite su

, il linguaggio accettato dall’LBA A è:

 

(A) = { w | w è accettata da A }

  116

Automi di Büchi & Model Checking LTL

Esempio:

: Linguaggio accettato (a c)

Esempio

7.3.2 Equivalenza ed Espressività

D efinizione: Due automi A e A sono equivalenti se accettano lo stesso

1 2

linguaggio. Valgono in generale le seguenti considerazioni:

 

(A ) = (A ) (A ) = (A )

   

 

1 2 1 2

 

(A ) = (A ) (A ) = (A )

   

 

1 2 1 2

. . .

inoltre

 

A LFSA non deterministico esiste A LFSA deterministico tale che

(A) = (A )

 

A LBA non deterministico esiste A LBA deterministico tale che

(A) = (A )

 

 

7 .4 Model Checking LTL

7.4.1 Idee alla base del Model Checking LTL

 Modifichiamo la funzione di etichettatura degli stati in modo da

considerare insiemi di simboli L : S 2

 Una parola w = a a . . . è accettata da un LBA sse esiste un accepting

0 1

   

run = s s . . . tale che a L(s ) i 0

0 1 i i

 

Consideriamo = 2 , così gli stati saranno etichettati con insiemi di

AP

insiemi di proposizioni atomiche.

117

Automi di Büchi & Model Checking LTL

Si vuole associare ad ogni formula LTL un LBA il cui linguaggio accettato

corrisponda alle sequenze di proposizioni atomiche che rendono valida

Esempio: corrispondente a p

7.4.2 Codifica delle

lle formule proposizionali

de

Gli insiemi di insiemi di proposizioni atomiche codificano le formule

proposizionali:

 

Se AP , . . . ,AP AP, allora ogni AP codifica la formula

1 n i

 

  

AP , , AP

L’insieme , per m 1 e 0 < k n codifica

 j

k k

1 m

Gli insiemi di insiemi di proposizioni atomiche non possono essere vuoti.

Esempio: codifica di una formula AP = {p, q}

 p)

s : (q

0  q)

s : (p

1

Formula LTL:

 p)  q)]

G[(q U (p

Stati formule proposizionali = Formule LTL

Transizioni comportamento temporale

118

Automi di Büchi & Model Checking LTL

7 .4.3 Model Checking

Model Checking (primo approccio)

Il metodo più semplice è quello di verificare che tutti i comportamenti del

sistema siano desiderabili: 

1. Costruire l’LBA per = A

 

2. Costruire l’LBA per il modello del sistema A

sys

3. Verificare se (A ) (A )

 

  

sys

Ma decidere l’inclusione tra i linguaggi accettati è un problema NP

Model Checking (secondo approccio)

Il problema di verificare l’inclusione tra linguaggi può essere aggirato poiché

   A

(A ) (A ) (A ) ( ) =

   

    

sys sys 

A è l’LBA complementare di A e accetta il linguaggio \ (A )

  

 A

In generale la costruzione di è quadraticamente esponenziale.

 2

n

c

 A

A ha n stati ha stati (c > 1)

 

Model Checking (terzo approccio) A

Infine, osservando che (A )= ( ) si arriva ad un metodo efficiente di

 

   

model checking: 

1. Costruire l’LBA per = A



2. Costruire l’LBA per il modello del sistema = A sys

3. Verificare se ) (A ) =

(A 

 

sys ,

(i run in comune tra A e A violano quindi sono indesiderati)



sys

Il terzo passo dell’algoritmo è decidibile in tempo lineare.

119

Automi di Büchi & Model Checking LTL

7 .4.4

4 Complessità

omplessità temporale Model Checking LTL

.4. C

Se definiamo con S l’insieme degli stati dell’LBA A , si ha che nel caso

sys sys

peggiore la complessità temporale del model checking LTL è :

O (|S | 2 )

2 | |

sys

(il fattore 2 è legato alla costruzione del grafo)

| |

Anche se la complessità è esponenziale nella lunghezza della formula LTL, nella

pratica le formule sono abbastanza corte (max 2 o 3 operatori)

120 Algebra dei Processi

8. Algebre di Processi

Un algebra di processi è un formalismo che consente di modellare sistemi

concorrenti che eventualmente interagiscono tra loro.

Gli elementi di base per ottenere questo formalismo sono le azioni e gli

operatori (o combinatori). Questi ultimi permettono di costruire espressioni che

simulano il comportamento del sistema considerato. Con questo simbolismo si

facilita la specifica e la manipolazione di processi soprattutto in un computer.

Nelle algebre più utilizzate gli operatori sono in numero ristretto, ma riescono a

definire gran parte delle proprietà richieste perché possono simulare molti

comportamenti di un sistema.

Esistono vari approcci per descrivere la semantica di un'algebra di processi. Dal

punto di vista operazionale, possiamo utilizzare dei grafi di transizione che

descrivono i comportamenti del sistema da modellare. In particolare, i due tipi

Kripke Labelled Transition

di grafi più comuni sono le Strutture di (KS) ed i

Systems (LTS). Nel primo caso si etichettano gli stati del grafo per descrivere in

che modo sono modificati dalle transizioni; nel secondo caso, come dice il nome,

le transizioni sono etichettate con azioni che causano il passaggio da uno stato

all'altro. S

1

a b S

S 1

1 b

a

d

c c,d

S

1 KRIPKE

LTS 121


PAGINE

136

PESO

1.55 MB

AUTORE

Sara F

PUBBLICATO

+1 anno fa


DESCRIZIONE APPUNTO

Appunti di Elementi di Software Dependability. Nello specifico gli argomenti trattati sono i seguenti: Modellazione Markoviana degli Attributi di Dependability, Valutazione degli attributi RAMS con il Metodo Markoviano, Ridondanza, Rilevazione & Correzione d'Errore, ecc.


DETTAGLI
Corso di laurea: Corso di laurea in ingegneria informatica
SSD:
Università: Firenze - Unifi
A.A.: 2013-2014

I contenuti di questa pagina costituiscono rielaborazioni personali del Publisher Sara F di informazioni apprese con la frequenza delle lezioni di Elementi di Software Dependability e studio autonomo di eventuali libri di riferimento in preparazione dell'esame finale o della tesi. Non devono intendersi come materiale ufficiale dell'università Firenze - Unifi o del prof Monile Umberto.

Acquista con carta o conto PayPal

Scarica il file tutte le volte che vuoi

Paga con un conto PayPal per usufruire della garanzia Soddisfatto o rimborsato

Recensioni
Ti è piaciuto questo appunto? Valutalo!

Altri appunti di Elementi di software dependability

Elementi di Software Dependability -Interpretazione Astratta
Appunto
Elementi di Software Dependability -Interpretazione Astratta – Verifica codice
Dispensa
Elementi di Software Dependability - Software Safety
Appunto
Elementi di Software Dependability - Formal Methods in Practice
Dispensa