Elementi di Software Dependability











 



 

Appunti del Corso di

Informatica Industriale 2

 Umberto Monile



 









      



I Indice

Indice

1. Modellazione Markoviana degli Attributi di Dependability . 1 



1.1 Introduzione...................................................................................1



1.2 Valutazione degli attributi RAMS con il Metodo Markoviano .......2



1.2.1 Affidabilità...........................................................................................3 

1.2.2 Safety...................................................................................................9 

1.2.3 Manutenibilità ...................................................................................10 

1.2.4 Disponibilità ......................................................................................11

2. Ridondanza................................

................................................................

......................................

......13

13

Ridondanza ................................ ................................ ...... 13 

2.1 Duplicazione e Confronto............................................................. 13



2.2 Duplicazione Riconfigurabile........................................................ 14



2.3 Modello NMR .............................................................................. 16



2.3.1 NMR Riconfigurabile ..........................................................................17

3. Rilevazione & Correzione d'Errore ....................................

....21

21

................................ .... 21 

3.1 Introduzione................................................................................. 21



3.2 Codici di parità............................................................................ 22



3.3 Codici Overlapping Parity ........................................................... 23



3.3.1 Overlapping Parity modificato ...........................................................25



3.4 Codici di Hamming ...................................................................... 26



3.5 Codici lineari ............................................................................... 28



3.5.1 Introduzione ........................................................................................28 

3.5.2 Codifica & Decodifica .........................................................................30



3.6 Codici aritmetici .......................................................................... 31



3.6.1 Codice AN...........................................................................................31

II Indice



3.7 Codici CRC (Controllo di Ridondanza Ciclico)............................ 33



3.7.1 Codifica & Decodifica .........................................................................34



3.7.2 L'emettitore ........................................................................................37 

3.7.3 Il ricevitore..........................................................................................38 

3.7.4 Rilevazione degli Errori ......................................................................39



3.7.5 Applicazioni Pratiche..........................................................................43 

3.7.6 Codici CRC correttori.........................................................................44



3.8 Codici di Solomon........................................................................ 46



3.8.1 Introduzione ........................................................................................46 

3.8.2 L'operazione di somma nel campo esteso GF(2 )...............................48

m 

3.8.3 I polinomi primitivi.............................................................................49 

3.8.4 Codifica (da riscrive ci pensa il prof)..................................................50



3.8.5 Decodifica............................................................................................54 

3.8.6 Applicazioni dei Codici di Solomon ....................................................59

4. Algoritmi distribuiti .........................................................

.........................61

61

................................ ......................... 61 

4.1 Introduzione................................................................................. 61



4.2 Memoria Stabile........................................................................... 63



4.3 Two-Phase Commit Protocol ....................................................... 65



4.4 Linear Two-Phase Commit Protocol ............................................ 65



4.5 Considerazioni sugli Algoritmi distribuiti:.................................... 66



4.6 Paradosso dei generali bizantini ................................................... 66



4.7 Consenso Distribuito tra processi asincroni .................................. 67



4.7.1 Introduzione ........................................................................................67 

4.7.2 Chandra Toueg ...................................................................................68 

4.8 Votazione Distribuita................................................................... 74



4.8.1 Byzantine Agreement..........................................................................74



4.9 Algoritmi di Sincronizzazione in ambito distribuito. .................... 78



4.9.1 Formalismi e definizioni......................................................................78



4.9.2 Classificazione degli Algoritmi di Sincronizzazione.............................79

4.10 Guasti software su un sistema distribuiti ................................... 82

III Indice

5. Logica

ogica................................

................................................................

..............................................

..............86

86

L ogica ................................ ................................ .............. 86 

5.1 Logica delle proposizioni .............................................................. 86



5.2 Logica dei predicati del primo ordine ........................................... 87



5.3 Logica Modale.............................................................................. 89



5.4 Logica Temporale ........................................................................ 92



5.4.1 Logica temporale Lineare con numero infiniti di stati (LTL).............93 

5.4.2 Logica temporale Lineare con numero finito di stati ..........................98 

5.4.3 Logica temporale con Tempo passato .................................................99



5.4.4 Logica temporale Continua e tempo reale ..........................................99



5.4.5 Logica temporale Ramificata (CTL)................................................. 100



5.4.6 CTL*................................................................................................. 103 

5.5 Comparazione tra LTL, CTL e CTL*........................................ 105

6. Model Checking CTL .....................................................

..................... 106

................................ 106 

6.1 L’algoritmo di Checking............................................................. 106



6.2 Algoritmo del Model Checking Simbolico................................... 109



6.2.1 Ordered Binary Decision Diagrams (OBDD) ................................... 109



6.2.2 Rappresentazione delle transizioni con OBDD ................................. 112

7. Automi di Büchi & Model Checking LTL........................

........................ 114

LTL 114 

7.1 Problema del Model Checking.................................................... 114



7.2 Automa a stati finiti .................................................................. 114



7.2.1 Linguaggio accettato ......................................................................... 115



7.3 Automa di Büchi ....................................................................... 116



7.3.1 Linguaggio accettato ......................................................................... 116



7.3.2 Equivalenza ed Espressività.............................................................. 117



7.4 Model Checking LTL ................................................................. 117



7.4.1 Idee alla base del Model Checking LTL............................................ 117



7.4.2 Codifica delle formule proposizionali ................................................ 118



7.4.3 Model Checking ................................................................................ 119

7.4.4 Complessità temporale Model Checking LTL................................... 120

IV Indice

8. Algebre di Processi................................

.........................................................

......................... 121

Processi ................................ 121 

8.1 Labelled Transition System (LTS). ............................................ 122



8.2 Il Calcolo CCS ........................................................................... 126



8.2.1 Struttura Sintattica di CCS.............................................................. 127



8.2.2 Semantica Operazionale di CCS ....................................................... 128



8.3 HENNESSY MILNER LOGIC (HML) ...................................... 131

V Modellazione Markoviana

1. Modellazione Markoviana degli

Attributi

tributi di Dependability

At

1.1 Introduzione

Dependability

Definizione di : proprietà di un sistema di essere adeguato alla

dipendenza da parte di un essere umano, o di una collettività, senza il pericolo

di rischi inaccettabili.

La dependability può essere definita come la credibilità di un sistema di calcolo,

ovvero il grado di fiducia che può essere ragionevolmente riposto nei servizi che

esso offre, dove: il servizio offerto da un sistema di calcolo è rappresentato dal

suo comportamento così come viene percepito dagli utenti; l'utente, umano o

l'utente

fisico, rappresenta un sistema distinto che interagisce con il sistema di calcolo.

La dependability di un sistema di calcolo include gli attributi di affidabilità,

disponibilità, sicurezza e protezione:

Reliability Availability Safety Security

( , , , )

 Reliability (affidabilità): sistema pronto ad essere usato.

 Availability (disponibilità): sistema che fornisce continuità di servizio.

 Safety (sicurezza): assenza di conseguenze catastrofiche.

 Security (protezione): assenza di intrusioni.

In molti casi, la sicurezza (security) intesa come protezione da guasti

intenzionali, non è considerata fondamentale. Viene quindi eliminato l’attributo

Maintainability

Security e viene aggiunto ottenendo quindi:

RAMS = (R

Reliability, Availability, Maintainability, Safety)

La manu

u tenibilità misura la facilità con la quale un sistema può essere riparato

man

una volta manifestatosi il fallimento. 1 Modellazione Markoviana

Le minacce (impedimenti

impedimenti) che possono violare la dependability di un sistema

impedimenti

sono classificate in:

 fault

guasti ( ): è il difetto fisico o malfunzionamento che avviene in

qualche componente.

 error

errori ( ): è il comportamento scorretto causato dal fault.

 failure

fallimento ( ): è l'incapacità del sistema a realizzare il suo servizio.

Le tecniche (mezzi) utilizzate per difendere un sistema da tali minacce sono le

seguenti:

 fault prevention

Prevenzione dai guasti ( ): come possono essere

prevenute le occorrenze di guasti;

 fault tolerance

Tolleranza ai guasti ( ): come garantire un servizio che si

mantenga conforme alle specifiche, nonostante i guasti;

 fault removal

Eliminazione del guasto ( ): come ridurre l'occorrenza

(numero, gravità) dei guasti;

 fault forecasting

Predizione di guasti ( ): come stimare il numero, la

frequenza di incidenza, presente e futura, e le conseguenze dei guasti.

1.2 Valutazione quantitativa degli attributi RAMS

con il Metodo Markoviano

Gli Attributi RAMS possono essere valutati quantitativamente. Una valutazione

quantitativa permette di fissare dei requisiti, e di verificare se gli attributi

RAMS ottenuti per un sistema rispettano i requisiti imposti, inoltre può aiutare

la ricerca di soluzioni nel caso che i requisiti non siano soddisfatti. La

valutazione degli attributi può essere fatta tramite diversi approcci analitici,

quelli più comunemente utilizzati sono : la modellizzazione combinatoria e

quella markoviana, noi analizzeremo solo la seconda.

I processi di Markov si basano sul concetto di stato e su quello di transizione.

Lo stato rappresenta tutto ciò che deve essere conosciuto per descrivere il

sistema in un dato istante. Nel caso di modelli di dependability uno stato

rappresenta una possibile configurazione di entità sane ed entità guaste. Le

transizioni descrivono i passaggi di stato al verificarsi di un evento: guasto di

una nuova entità, riparazione di una entità guasta. Le transizioni di stato sono

caratterizzate da probabilità, come la probabilità di guasto di una entità, la

probabilità di riparazione e il fattore di copertura.

2 Modellazione Markoviana

1.2.1 Affidabilità

L’affidabilità (reliability) di un sistema è la misura del tempo continuativo in

cui viene fornito un servizio corretto.

Definizione di Distribuzione dell’Affidabilità:

La distribuzione dell’affidabilità R(t) esprime la probabilità che un componente,

correttamente funzionante al tempo t , sia correttamente funzionante al tempo

0

t.   

 t

R

( t

) e .

Il tasso di fallimento è denotato dal simbolo In generale il tasso di fallimento

(failure rate) di un sistema è il numero di fallimenti nell’unità di tempo.

Mean Time To Failure

Definiamo MTTF ( ) come il tempo medio tra l’avvio e il

guasto; è il reciproco del tasso di fallimento:

 1



MTTF 

Prendiamo la seguente catena di Markov composta da due stati: Op (operativo)

ed F (guasto)

 GUASTO

O F

A questo modello associamo la probabilità di passare da uno stato all'altro,

inoltre deve essere rispettata la proprietà della Catena di Markov ovvero che la

somma delle probabilità di tutti gli archi uscenti dal nodo è pari a 1

1-p 1

O F

p

La probabilità che al tempo t + ∆t il sistema si trovi in OP dato che era in OP

in t è data da:

    

  ( t t )

R

( t t

) e

 

P

OP   t

R

( t

) e

3 Modellazione Markoviana

La probabilità che da OP si passi in F è :

 

 



  (

t t

)

R (

t t

) e 





         

    

       

t 2

p 1 1 1 e 1 1 ( t

) ( t

) ......... t





t

R (

t

) e

Il sistema può essere modellato come segue:

1-∆t 1 - t

R(t) = e

O F

∆t

Questo appena visto è un modello semplice, ora vediamo un modello per la

determinazione dell’affidabilità di un sistema costituito da entità interconnesse

Triple Modular Redundancy

in modo TMR ( ).

Un sistema con ridondanza modulare tripla (TMR) è costituito da tre moduli

uguali che lavorano in parallelo sugli stessi dati d’ingresso e le cui uscite sono

confrontate da un elemento di comparazione (voter), la cui uscita è pari alla

maggioranza degli ingressi. M

1

M V

2

M

3

Figura 1 : TMR (ridondanza modulare tripla)

4 Modellazione Markoviana

Si può numerare ogni stato con dei numeri binari, usando una variabile

booleana per ogni modulo. F M

2

100 110

F M

F M F M

1

1 3

F M F M F M

2 3 1

000 010 011 111

F M

2

F M F M

3 2

001 101

F M

1

Come si può osservare dallo stato (0,0,0) sono possibili tre transizioni dovute al

guasto del primo, del secondo o del terzo modulo. Si può osservare che ogni

singola transizione è causata da un singolo evento.

Si può affermare che:

 Per un modello TMR, tutti gli stati con due variabili a 1 sono stati di

guasti.

 Per un sistema in parallelo (NO TMR) l’unico stato di guasto è l’ultimo

stato, quindi il sistema funziona se c’è almeno un valore 0.

 Per un sistema in serie l’unico stato funzionante è il primo (000).

Per trasformare questo modello in un modello Markoviano bisogna aggiungere le

probabilità.

Per un modello TMR si considerano tutti i moduli con lo stesso tasso di

fallimento (stesso MTTF e stesso ) 1- ∆t

1-2 ∆t ∆t

100 110

∆t ∆t ∆t

1-2 ∆t 1

1- ∆t

1-3 ∆t ∆t ∆t

000 010 011 111

∆t 1- ∆t

1-2 ∆t ∆t

∆t ∆t

001 101

∆t

5 Modellazione Markovia