Che materia stai cercando?

Elementi di Software Dependability

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 . 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 Algebra dei Processi

8.1 Labelled Transition System (LTS)

Keller

I sistemi di transizioni etichettate furono introdotti da nel 1976 come un

modello formale per descrivere programmi paralleli ed in seguito sono stati usati

per dare una semantica operazionale strutturale ai linguaggi di programmazione.

I sistemi di transizione sono quindi un modello relazionale astratto basato sulle

nozioni primitive di stato e transizione. Molte proprietà dei sistemi concorrenti

possono essere studiate tramite questa rappresentazione; bisogna essere in grado

di conoscere la capacità di tali sistemi di compiere azioni appartenenti ad un

insieme predeterminato Act, azioni che possono essere istantanee o durature.

Ovviamente un sistema sequenziale può effettuare al più un'azione nello stesso

istante, certe azioni però possono essere azioni di sincronizzazione di un processo

con il sistema concorrente di cui fa parte oppure segnali inviati dal resto del

sistema al processo; è ovvio che quest'ultimo tipo di azioni occorrono solamente

nel caso in cui i processi cooperino. Per essere più precisi forniamo una

definizione formale di LTS. 

Definizione: Un LTS è una quadrupla (S, s , Act, ) dove:

0

 S è un insieme di stati;

 s è lo stato iniziale;

0

 Act è un insieme finito e non vuoto di azioni visibili;

   S Act S è la relazione di transizione tale che un'elemento

× ×

 

(s , a , s ) se esiste la possibilità di passare da uno stato s ad un

0 1 0

a

altro s tramite l'azione a (s s ).

1 0 1

Un LTS può essere rappresentato tramite un grafo il cui nodo iniziale è lo stato

iniziale s , le relazioni di transizione sono rappresentate dagli archi fra i nodi

0

(archi etichettati con la azioni appartenenti ad Act), i nodi infine rappresentano

gli stati appartenenti a S.

Definizione: Negli LTS, un cammino (o computazione) è una sequenza

      

(s , , s ) (s , , s ) (s , , s ) dove ogni tripla (s , , s )

0 0 1 1 1 2 2 2 3 i i i+1

Un cammino può essere finito o infinito (in base al numero di transizioni che

contiene) ed eventualmente può avere dei cicli al suo interno; possiamo inoltre

trovare cammini nulli rappresentati da una sequenza vuota.

122 Algebra dei Processi

Esempio:

: Modellazione semplificata ad eventi della macchina del caffè di

Esempio

ingegneria.

Questa macchina permette di eseguire sequenze del tipo :

wake-35-caffè-ok-wake-40-cioccolata

ma non: wake-35-cioccolata

wake

35 cent 40 cent

caffè cioccolata

ok ok

Con un modello del genere posso verificare il comportamento della macchina a

fronte di sequenze ammesse e non ammesse. L’implementazione dovrà contenere

tutte e sole le tracce definite nel modello

Supponiamo di avere la seguente implementazione:

wake

wake

35 cent 40 cent

caffè cioccolata

ok ok

123 Algebra dei Processi

trace equivalence

L’implementazione contiene tutte le tracce del modello ( ) ma

ha un non determinismo sullo stato iniziale infatti è la macchina e non l’utente

a “decidere” se verrà presa una cioccolata o del caffè.

Da notare che la trace equivalence tra i due LTS non cattura la ramificazione:

dunque anche se due macchine contengono le stesse tracce non è detto che siano

capaci di soddisfare i test.

Uno dei vantaggi dell’LTS sta nella possibilità di costruire su di esso una

bisimulazione.

bisimulazione

Definizione: R è una relazione di bisimulazione forte su S, S’ si indica con S R S’

  s  s 

(S e S’ sono insieme degli stati dove s S e s ’ S’) se S e ’ S’:

i i i i

 

    

 

a a

s s s ' S

' : s

' s ' s R s '

 1 1 1 1 1

SRS

'  

    

 

a a

s

' s ' s S : s s s R s '

 1 1 1 1 1

   

Definizione: s S e s’ S’ sono equivalenti (s s’) se R di bisimulazione

forte tra s e s’. ) ’)

Definizione: Due LTS (S, s , Act, e (S’, s ’, Act’, si dicono equivalenti

o o

(o bisimili) se R di bisimulazione forte tra S e S’: s R s ’

0 0

Valutiamo la relazione di bisimulazione sul modello e sull’implementazione

prima definiti: wake

wake

wake R R

35 cent 35 cent 40 cent

40 cent

caffè caffè

cioccolata cioccolata

ok ok ok ok

Modello Implementazione

In questo caso il modello ed l’implementazione non sono equivalenti per la

bisimulazione. 124 Algebra dei Processi

Supponiamo invece di avere un’altra implementazione: wake

wake 35 cent

35 cent 40 cent

40 cent

caffè cioccolata cioccolata

caffè ok

ok ok

Modello Implementazione

In questo caso il modello ed l’implementazione sono equivalenti per le tracce e

per la bisimulazione.

Un’eventualità è che nell’implementazione vengono fatte azioni non osservabili,

indicate con . Si ridefinisce LTS nel seguente modo:

  , 

(S, s , Act )

o

    

Dove in questo caso S × Act × S

Definizione: R è una relazione di bisimulazione debole su S, S’ si indica con

  s 

S R S’ (S e S’ sono insieme degli stati dove s S e s ’ S’) se S e

i i i

s 

’ S’:

i  a a

     

s s s ' S

' : s

' s ' s R s '

 1 1 1 1 1

SRS

'  a a

      

s

' s ' s S : s s s R s '

 1 1 1 1 1

    a

a     

 s s s s s

'

s s

'  

(dove se solo se s , s , …., s tale che ).

1 2 n 1 2 n

   

Definizione: s S e s’ S’ sono observation equivalent (s s’) se R di

bisimulazione debole tra s e s’. 125 Algebra dei Processi

) ’)

Definizione: Due LTS (S, s , Act, e (S’, s ’, Act’, sono observation

o o

equivalent se R di bisimulazione debole tra S e S’: s R s ’

0 0

Oltre all’equivalenza esiste il preordine, usato nel raffinamento dei modelli.

preordine

M è il modello iniziale che viene via via raffinato nella versione M M …,

0 1 2

ottenendo una sequenza:   

M M M M …….

0 1 2 3

8.2 Il Calcolo CCS

In questo paragrafo introduciamo il CCS, cioè una delle algebre di processi più

conosciute ed utilizzate nella teoria della concorrenza. Il Calcolo dei Sistemi di

Calculus of Communicating Systems

Comunicazione ( ) fu introdotto nel 1980 ad

Robin Milner

opera di per studiare le proprietà strutturali di sistemi composti.

Questo calcolo ha una struttura semplice, ma molto efficiente nel modellamento

di sistemi concorrenti. E' composto da un piccolo insieme di operatori con cui si

costruisce un'ampia varietà di descrizioni di sistemi. I blocchi di base di queste

descrizioni sono le azioni le quali rappresentano passi di esecuzione interna

oppure interazioni potenziali con l'ambiente esterno (attraverso input e output).

Le azioni visibili prendono il nome della porta su cui agiscono e se sono output

vengono soprabarrati. In genere l'insieme di tutte le azioni di questo calcolo si

indica con:   

Accs = Act (Act è l'insieme di azioni visibili)

In CCS, i processi sono indicati da una stringa che inizia con lettera maiuscola

(anche tutto maiuscolo), mentre le azioni svolte da un processo sono stringhe

con lettere minuscole. Gli operatori sono pochi, ma con essi si possono simulare

quasi tutti i comportamenti di un sistema.

126 Algebra dei Processi

8.2.1 Struttura Sintattica di CCS   

L'insieme delle azioni del CCS è definito da Accs = Act dove Act

comprende tutte le azioni esterne (input e output) che possono essere svolte dal

sistema, mentre rappresenta l'azione interna.

Gli operatori di base del CCS sono i seguenti (indichiamo con P e Q processi

generici ):

Action Prefix

1. : a.P, azione che trasforma il processo in un altro.

2. Scelta non deterministica:

: P + Q

deterministica

3. Composizione parallela: P | Q

4. Restrizione: P/Q (Q Accs – { })

Relabelling

5. : P[f] (f: Accs Accs)

Schematizzando, i termini di questo calcolo sono generati dalla seguente

Grammatica:  

P :: nil a

.

P P Q P |

Q P / L | P

[ f ]

nil

dove è il processo inattivo che non esegue alcun comportamento.

Esempio: la macchina vista prima può essere scritta come:

wake.(35.coffee.ok.nil+40.chocolate.ok.nile)

la composizione in parallelo sarà a.nil | c.nil (sintassi). Usualmente si dà alla

composizione parallela una semantica “interleaving”:

a c (semantica)

a

c

Ciò che permette di passare dalla formula CCS alla macchina è la semantica

operazionale. 127 Algebra dei Processi

8.2.2 Semantica Operazionale di CCS

Con semantica operazionale di un'algebra di processi si intendono i passi di

esecuzione che possono essere fatti da un processo. Questi comportamenti sono

descritti dagli assiomi e dalle regole di transizione per gli operatori che nel CCS

sono le seguenti:

1. Action Prefix  



a

a P P

Significa che il processo a.P può sempre eseguire l’azione a e trasformarsi nel

processo p ( o meglio attivare il processo p)

Esmpio: a.b.nil a b

a.b.nil b.nil nil

2. Scelta non deterministica

a :

deterministic

 



a a

P P ' P P '

1 1 2 2

 

  



a a

P P P ' P P P '

1 2 1 1 2 2

  



a a

P P ' P P P '

Se allora

1 1 1 2 1

oppure 

  



a a

P P ' P P P '

Se allora

2 2 1 2 2

Esempio: a.nil + b.c.nil (P =a.nil, P =b.c.nil)

1 2

P 1 b

a c.nil

nil c

128 Algebra dei Processi

3. Composizione parallela:



a

P P '

1 1 (Interleaving Semantic)



a

P P P ' P

1 2 1 2



 a

a P P P ' P

P P '

Se allora 1 2 1 2

1 1

Oppure: 



a

P P '

2 2 (Interleaving Semantic)



a

P P P P '

1 2 1 2



 a

a P P P P '

P P '

Se allora

2 2 1 2 1 2

Esempio: a.nil|b.nil (P =a.nil e P =b.nil)

1 2 P 1

a b

a.nil| nil=a.nil

nil| b.nil=b.nil

b a

nil| nil=nil

Da notare che le uguaglianze negli stati valgono perché valgono alcune regole di

assorbimento:

 nil | p = p

 nil | p.nil = p.nil

 nil | nil = nil 129


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