Anteprima
Vedrai una selezione di 29 pagine su 136
Elementi di Software Dependability Pag. 1 Elementi di Software Dependability Pag. 2
Anteprima di 29 pagg. su 136.
Scarica il documento per vederlo tutto.
Scarica
Elementi di Software Dependability Pag. 6
Anteprima di 29 pagg. su 136.
Scarica il documento per vederlo tutto.
Scarica
Elementi di Software Dependability Pag. 11
Anteprima di 29 pagg. su 136.
Scarica il documento per vederlo tutto.
Scarica
Elementi di Software Dependability Pag. 16
Anteprima di 29 pagg. su 136.
Scarica il documento per vederlo tutto.
Scarica
Elementi di Software Dependability Pag. 21
Anteprima di 29 pagg. su 136.
Scarica il documento per vederlo tutto.
Scarica
Elementi di Software Dependability Pag. 26
Anteprima di 29 pagg. su 136.
Scarica il documento per vederlo tutto.
Scarica
Elementi di Software Dependability Pag. 31
Anteprima di 29 pagg. su 136.
Scarica il documento per vederlo tutto.
Scarica
Elementi di Software Dependability Pag. 36
Anteprima di 29 pagg. su 136.
Scarica il documento per vederlo tutto.
Scarica
Elementi di Software Dependability Pag. 41
Anteprima di 29 pagg. su 136.
Scarica il documento per vederlo tutto.
Scarica
Elementi di Software Dependability Pag. 46
Anteprima di 29 pagg. su 136.
Scarica il documento per vederlo tutto.
Scarica
Elementi di Software Dependability Pag. 51
Anteprima di 29 pagg. su 136.
Scarica il documento per vederlo tutto.
Scarica
Elementi di Software Dependability Pag. 56
Anteprima di 29 pagg. su 136.
Scarica il documento per vederlo tutto.
Scarica
Elementi di Software Dependability Pag. 61
Anteprima di 29 pagg. su 136.
Scarica il documento per vederlo tutto.
Scarica
Elementi di Software Dependability Pag. 66
Anteprima di 29 pagg. su 136.
Scarica il documento per vederlo tutto.
Scarica
Elementi di Software Dependability Pag. 71
Anteprima di 29 pagg. su 136.
Scarica il documento per vederlo tutto.
Scarica
Elementi di Software Dependability Pag. 76
Anteprima di 29 pagg. su 136.
Scarica il documento per vederlo tutto.
Scarica
Elementi di Software Dependability Pag. 81
Anteprima di 29 pagg. su 136.
Scarica il documento per vederlo tutto.
Scarica
Elementi di Software Dependability Pag. 86
Anteprima di 29 pagg. su 136.
Scarica il documento per vederlo tutto.
Scarica
Elementi di Software Dependability Pag. 91
Anteprima di 29 pagg. su 136.
Scarica il documento per vederlo tutto.
Scarica
Elementi di Software Dependability Pag. 96
Anteprima di 29 pagg. su 136.
Scarica il documento per vederlo tutto.
Scarica
Elementi di Software Dependability Pag. 101
Anteprima di 29 pagg. su 136.
Scarica il documento per vederlo tutto.
Scarica
Elementi di Software Dependability Pag. 106
Anteprima di 29 pagg. su 136.
Scarica il documento per vederlo tutto.
Scarica
Elementi di Software Dependability Pag. 111
Anteprima di 29 pagg. su 136.
Scarica il documento per vederlo tutto.
Scarica
Elementi di Software Dependability Pag. 116
Anteprima di 29 pagg. su 136.
Scarica il documento per vederlo tutto.
Scarica
Elementi di Software Dependability Pag. 121
Anteprima di 29 pagg. su 136.
Scarica il documento per vederlo tutto.
Scarica
Elementi di Software Dependability Pag. 126
Anteprima di 29 pagg. su 136.
Scarica il documento per vederlo tutto.
Scarica
Elementi di Software Dependability Pag. 131
Anteprima di 29 pagg. su 136.
Scarica il documento per vederlo tutto.
Scarica
Elementi di Software Dependability Pag. 136
1 su 136
D/illustrazione/soddisfatti o rimborsati
Disdici quando
vuoi
Acquista con carta
o PayPal
Scarica i documenti
tutte le volte che vuoi
Estratto del documento

L'OBDD: una rappresentazione canonica di una funzione booleana

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 OBDD: 110 Model Checking CTL

Se usiamo un ordine a < a < b < b per il comparatore, otteniamo il seguente OBDD: 6 .2.1.1.1 Logica operazionale OBDD:.2.1

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(a,b,c,d) = g(a,b,c,d)
  = (f(a,b,c,d) ∧ g(a,b,c,d)) ∨ (f(a,b,c,d) ∧ g(a,b,c,d))
  = f(a,b,c,d) ∧ g(a,b,c,d) ∧ f(a,b,c,d) ∧ g(a,b,c,d)
  = f(a,b,c,d) ∧ g(a,b,c,d)

Divide il problema in due sottoproblemi. Questo significa 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.

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

Per definizione:

  • a : f f f
  • aaa: sostituire tutti i nodi con il sotto-albero sinistro.
  • f (a, b, c, d) a a: sostituire tutti i 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 ,...v1 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 ndove v, v, v, ..., v rappresenta lo stato attuale e v', v', v', ..., v' rappresenta1 2 3 n 1 2 3 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 utilizzandoOBDDs: U UEFp = Lfp .p EX dove Lfp (minimo punto fisso).Introducendo le variabili di stato e la relazione di transizione otteniamo: v’  U UEFp = Lfp .p(v) [T(v,v’) (v’)]A questo punto si calcola la sequenza:U U U (v), (v), (v),0 1 2fino alla sua convergenza. ULa convergenza può essere rilevata dato che gli stati (v) sono rappresentatiicome OBDDs. 113

Automi di Büchi & Model Checking LTL7. Automi di Büchi & ModelChecking LTL7.1 Problema del Model CheckingDato un modello M, uno stato s ed una proprietà espressa con una formula LTL, determinare se M, s |=Soddisfacibilità formule LTL Model Checking per LTLDecidibile decidibileIl Model Checking LTL è basato su una variante degli automi a stati finiti,chiamati Automi di Büchi7.2 Automama a stati finitiAutoDefinizione:: Un Automa a stati finiti etichettato (LFSA) è una tuplaDefinizione,(,

S, S , F, L):0 è un alfabeto di simboli.

S è un insieme finito di stati.

ΔS S è l'insieme di stati iniziali.

∃ : 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

  1. ∀ a ∈ Λ, |{s ∈ S | L(s) = a}| ≤ 1
  2. ∀ a ∈ Λ, ∀ s ∈ S, |{s' ∈ S | L(s') = a}| ≤ 1

Automi di Büchi & Model Checking LTL

Esempi determinismo

Esempi di non determinismo

7.2.1 Linguaggio accettato

Definizione: Un run per un LFSA è una sequenza finita = s0 s1 ... sn tale che

  1. s0 ∈ Λ
  2. ∀ i ∈ [0, n-1], ∃ si+1 ∈ S tale che ∃ a ∈ Λ, L(si+1) = a
  3. ∃ n ∈ N, ∃ s ∈ S tale che L(s) ∈ F

Definizione: Un run è detto accepting se sn ∈ F

Definizione: Una parola w = a0 a1 ... an è accettata se esiste un accepting run = s0 s1 ... sn : ∀ i ∈ [0, n], L(si) = ai

i i i :(

Definizione: Se si indica con l'insieme di tutte le possibili parole finite sul linguaggio accettato dall'LFSA A è:

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: Un run per un LBA è una sequenza infinita = s s . . . tale che

Defin 0 1   is S e s s 000 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 un0 1accepting run  i   )= s s . . . tale che L(s ) = ai 0 (a0 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 }  116Automi di Büchi & Model Checking LTLEsempio:: Linguaggio accettato (a c)Esempio7.3.2 Equivalenza ed EspressivitàD efinizione: Due automi A e A sono equivalenti se accettano lo stesso1 2linguaggio. 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 LTL7.4.1 Idee alla base del Model Checking LTL Modifichiamo la funzione di

etichettatura degli stati in modo da considerare insiemi di simboli L : S2

Una parola w = a1a2...è accettata da un LBA sse esiste un run = s1s2... tale che a L(si) = {0, 1} per ogni i

Consideriamo L = {0, 1}, così gli stati saranno etichettati con insiemi di insiemi di proposizioni atomiche.

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 la formula.

Esempio: corrispondente a <p>7.4.2 Codifica delle formule proposizionali

Gli insiemi di insiemi di proposizioni atomiche codificano le formule proposizionali:

Se AP1, AP2, ..., APn sono gli insiemi di proposizioni atomiche, allora ogni APi codifica la formula <pi>

L'insieme {AP1, AP2, ..., APn} per m ≥ 1 e 0 ≤ k ≤ n codifica la formula <pk> per ogni j ≤ k ≤ m

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

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

{(p), (q), (p, q)}

s : (q0)

s : (p1Formula LTL:
3 =p) 3 =q)]G[(q U (pStati formule proposizionali = Formule LTLTransizioni comportamento temporale118Automi di Büchi & Model Checking LTL7 .4.3 Model CheckingModel Checking (primo approccio)Il metodo più semplice è quello di verificare che tutti i comportamenti delsistema siano desiderabili:
  1. Costruire l’LBA per = A∈
  2. Costruire l’LBA per il modello del sistema Asys∈
  3. Verificare se (A∈) (A∈)5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5
    5 stati (c > 1) Model Checking (terzo approccio) AInfine, 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)sysIl terzo passo dell’algoritmo è decidibile in tempo lineare.119Automi di Büchi & Model Checking LTL7 .4.44 Complessitàomple

Dettagli
Publisher
Sara F
A.A. 2012-2013
136 pagine
SSD Scienze matematiche e informatiche INF/01 Informatica
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à Università degli Studi di Firenze o del prof Monile Umberto.