Elementi di Software Dependability

  Appunti del Corso di Informatica Industriale 2 Umberto Monile

Indice

I IndiceIndice1. 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à ......................................................................................112. Ridondanza............................................................................................................................................1313Ridondanza ................................ ................................ ...... 13 2.1 Duplicazione e Confronto............................................................. 132.2 Duplicazione Riconfigurabile........................................................ 142.3 Modello NMR .............................................................................. 162.3.1 NMR Riconfigurabile ..........................................................................173. Rilevazione & Correzione d'Errore ........................................2121................................ .... 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...........................................................................................31II 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 )...............................48m 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 ....................................................594. Algoritmi distribuiti ..................................................................................6161................................ ......................... 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.............................794.10 Guasti software su un sistema distribuiti ................................... 82III Indice5. Logicaogica............................................................................................................................................................8686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*........................................ 1056. 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 ................................. 1127. 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 ................................................................................ 1197.4.4 Complessità temporale Model Checking LTL................................... 120IV Indice8. 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) ...................................... 131V

Modellazione Markoviana

1. Modellazione Markoviana degli Attributi di Dependability

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 MaintainabilitySecurity e viene aggiunto ottenendo quindi: RAMS = (RReliability, Availability, Maintainability, Safety)

La manuu tenibilità misura la facilità con la quale un sistema può essere riparato manuna volta manifestatosi il fallimento. 1 Modellazione Markoviana

Le minacce (impedimentiimpedimenti) che possono violare la dependability di un sistema impedimenti sono classificate in:

• Faultguasti ( ): è il difetto fisico o malfunzionamento che avviene in qualche componente.
• Errorerrori ( ): è il comportamento scorretto causato dal fault.
• Failurefallimento ( ): è l'incapacità del sistema a realizzare il suo servizio.

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

• Fault preventionPrevenzione dai guasti ( ): come possono essere prevenute le occorrenze di guasti;
• Fault toleranceTolleranza ai guasti ( ): come garantire un servizio che si mantenga conforme alle specifiche, nonostante i guasti;
• Fault removalEliminazione del guasto ( ): come ridurre l'occorrenza (numero, gravità) dei guasti;
• Fault forecastingPredizione 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 0t.    tR( 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 FailureDefiniamo 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) GUASTOO FA 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 11-p 1O Fp

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 POP   tR( t) e3 Modellazione Markoviana

La probabilità che da OP si passi in F è :     (t t)R (t t) e                     t 2p 1 1 1 e 1 1 ( t) ( t) ......... ttR (t) e

Il sistema può essere modellato come segue:1-∆t 1 - tR(t) = eO 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. M1M V2M3Figura 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 M2100 110F MF M F M11 3F M F M F M2 3 1000 010 011 111F M2F M F M3 2001 101F M1

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- ∆t1-2 ∆t ∆t100 110∆t ∆t ∆t1-2 ∆t 11- ∆t1-3 ∆t ∆t ∆t000 010 011 111∆t 1- ∆t1-2 ∆t ∆t∆t ∆t001 101∆t5 Modellazione Markovia