Metodi formali dello sviluppo software
a.a.2013/2014
Prof. Anna Labella
12/22/2015
1
OBDD
[H-R cap.6]
Rappresentare le funzioni booleane
12/22/2015
2
Binary decision diagrams
12/22/2015
3
BDD
12/22/2015
4
BDD
12/22/2015
5
BDD

Rimuovere i terminali duplicati

Rimuovere i test ridondanti

Rimuovere i non terminali duplicati
12/22/2015
6
BDD

costanti

variabili
12/22/2015
7
BDD
Si possono sostituire terminali con non
terminali e comporre funzioni
ad es.
 nella congiunzione si sostituisce 1 con il
BDD dell’altra funzione
 nella disgiunzione si sostituisce 0 con il
BDD dell’altra funzione
 nella negazione si scambiano 1 e 0

12/22/2015
8
BDD

Soddisfacibilità: si raggiunge 1
attraverso un cammino coerente

Validità: non si raggiunge 0 attraverso
un cammino coerente
12/22/2015
9
OBDD
Equivalenza?
12/22/2015
10
OBDD
Forma normale: ordinare e poi ridurre
Il risultato è unico
12/22/2015
11
OBDD
Un esempio: la funzione parità su 4 variabili
12/22/2015
12
OBDD: l’algoritmo “reduce”
Identifica nodi uguali partendo dal basso
12/22/2015
13
OBDD: l’algoritmo “apply”
Implementa operazioni
12/22/2015
14
OBDD: l’algoritmo “restrict”
Da f a f[0/x]
12/22/2015
15
OBDD: l’algoritmo “exists”
 f = f[0/x] + f[1/x]
 f = f[0/x] . f[1/x]
12/22/2015
16
Specifica e logica


Specifica
derivata dalle
proprietà del
sistema

Sintassi

Semantica
Specifica
derivata da un
modello del
sistema
12/22/2015
17
Model Checking

automatico

Sistemi
concorrenti

Sistemi
reattivi

Aspetti
temporali

Basato su un
modello costruito col
model checking
 Verifica di
soddisfacibilità di
proprietà
 A posteriori
12/22/2015
18
State machines: Alloy

automatico

Basato su un
modello
Verifica di
proprietà
Costruisce un
contromodello


12/22/2015

Stati finiti

statico
19
Logica temporale
[H-R cap.3]
a è una costante di tipo tempo
Se c’è richiesta di stampare un file, prima o poi il file sarà stampato
12/22/2015
20
Logica temporale
Si preferiscono operatori modali
distinguendo i riferimenti temporali da quelli di dominio
12/22/2015
21
Logica temporale: sintassi
::=T
| | p | () | () | () | () |
(X) | (F) | (G) | ( U ) | ( W )
“prima o poi”
G “sempre”
U “finché”
W “finché eventualmente”
F
12/22/2015
22
Logica temporale LTL
Tempo lineare/ ramificato
Tempo discreto
12/22/2015
23
Logica temporale LTL: LTS
• L‘interpretazione è data su un sistema di transizione
M= (S, , L)
• S è un insieme di stati (nodi)
•  una relazione di accessibilità
• L un’etichettatura dei nodi con formule atomiche
Proprietà della relazione di accessibilità
12/22/2015
24
12/22/2015
25
12/22/2015
26
12/22/2015
27
Logica temporale LTL: semantica
Soddisfacibilità:
Un cammino è una successione infinita di stati in
relazione consecutiva
M,s |= se ogni cammino che parte da s soddisfa 
12/22/2015
28
Logica temporale LTL: semantica
12/22/2015
29
12/22/2015
30