Model Checking
Model Checking
E’ una tecnica per la verifica automatica di software e
di sistemi reattivi
Consiste nel verificare alcune proprietà, espresse in
logiche temporali, di un modello del sistema.
La base dei modelli operazionali sui quali si applica
questa tecnica sono gli automi
Tino Cortesi
Tecniche di Analisi di Programmi
2
Automi
Un automa è una rappresentazione di un sistema:
l’evoluzione da uno stato all’altro del sistema è legata
all’applicazione di transizioni.
Esempio:
Un orologio digitale può essere rappresentato da un automa
in cui ogni stato rappresenta l’ora e minuto corrente. Ci
possono essere quindi 24x60=1440 possibili stati
. . .
Tino Cortesi
11.12
11.13
Tecniche di Analisi di Programmi
11.14
. . .
3
Rappresentazione di un automa
Un automa viene rappresentato denotando con cerchi
gli stati del sistema e con frecce le transizioni da uno
stato all’altro
Esempio
Un “contatore modulo 3” può essere rappresentato in
forma completa dal seguente automa
inc
dec
0
dec
inc
Tino Cortesi
1
dec
2
Tecniche di Analisi di Programmi
inc
4
Automi finiti ed infiniti
L’orologio digitale può essere visto come un contatore modulo
1440.
Abbiamo visto che il “contatore modulo 3” ha tre stati
Una variabile intera può essere modellata con un automa che ha
un numero infinito di stati (uno per ogni possibile valore) e
avente una transizione per ognuna delle operazioni elementari
(incremento, decremento, cambio di segno, ecc.)
Anche se esistono tecniche di model checking che si applicano a
classi ristrette di automi con numero infinito di stati, il model
checking si applica usualmente a sistemi rappresentabili come
automi a stati finiti.
Tino Cortesi
Tecniche di Analisi di Programmi
5
Digicode
Supponiamo di voler modellare un luchetto a
combinazione, con sole tre chiavi A,B,C. Il luchetto si
apre solo quando la combinazione ABA viene inserita.
Questo sistema può essere rappresentato con un
automa con 4 stati e 9 transizioni.
Tino Cortesi
Tecniche di Analisi di Programmi
6
Digicode
B,C
1
A
B
A
2
A
3
4
C
B,C
Tino Cortesi
Tecniche di Analisi di Programmi
7
Esecuzioni
Una esecuzione è una sequenza di stati che descrive una
possibile evoluzione del sistema
Ad es. 1121, 12234, 112312234 sono esecuzioni del
digicode
Le possibili esecuzioni del digicode sono
1
11,12
111,112,121,122,123
1111,1112,1121,1122,1123,1211,1212,1221,1222,1223,1231,1234
…
Queste possono essere organizzate sotto forma di albero
Tino Cortesi
Tecniche di Analisi di Programmi
8
Albero delle esecuzioni
1
1
1
1
Tino Cortesi
2
2
2
1
2
2
1
3
1
2
Tecniche di Analisi di Programmi
1
2
3
3
1
4
9
Proprietà
Il nostro obiettivo è verificare proprietà del sistema, o meglio
verificare proprietà del modello del sistema
Associamo quindi ad ogni stato dell’automa delle proprietà
elementari che sappiamo essere soddisfatte in quello stato
Ad esempio la proprietà “il luchetto è aperto” vale nello stato 4,
ma non vale negli stati 1,2 e 3.
Ma vorremmo dimostrare di più. Ad esempio:
Se il luchetto si apre, allora le ultime lettere digitate sono
ABA, in questo ordine
Digitando una qualsiasi sequenza che termini con ABA si
apre il luchetto
Tino Cortesi
Tecniche di Analisi di Programmi
10
Proposizione atomiche
Per distinguere proprietà elementari da proprietà più complesse,
parliamo di proposizione atomiche per denotare proprietà che sono
vere o false in un dato stato.
Nell’esempio del digicode, possiamo definire come proprietà
elementari:
PA : è stato appena digitato un A
PB : è stato appena digitato un B
PC : è stato appena digitato un C
pred2 : lo stato precedente è il 2
pred3 : lo stato precedente è il 3
Tino Cortesi
Tecniche di Analisi di Programmi
11
Automa con proposizioni atomiche
B,C
A
1
2
PA
A
B
3
pred2
PB
A
4
pred3
PA
C
B,C
Tino Cortesi
Tecniche di Analisi di Programmi
12
B,C
A
1
2
PA
A
B
3
pred2
PB
A
4
pred3
PA
C
B,C
Dimostriamo che se il luchetto si apre, allora le ultime lettere digitate
sono ABA, in questo ordine
Consideriamo un’esecuzione che apre il luchetto, cioè che finisce sullo
stato 4
Poiché in 4 vale pred3, l’esecuzione deve finire con 34
Ma in 3 vale pred2. quindi l’esecuzione deve finire con 234.
In 2 e 4 vale PA, ed in 3 vale PB . quindi le ultime tre lettere digitate
devono essere ABA.
Tino Cortesi
Tecniche di Analisi di Programmi
13
Automi
Dato un insieme di proposizioni elementari Pi, un automa è una
tupla A =<Q,E,T,q0,l> in cui:
Q è un insieme finito di stati
E è un insieme finito di etichette di transizioni
T  Q x E x Q è un insieme di transizioni
q0 è lo stato iniziale
l è la funzione che associa ad ogni stato di Q l’insieme delle
proprietà elementari che sono vere in quello stato
Tino Cortesi
Tecniche di Analisi di Programmi
14
L’automa digicode
B,C
A
1
2
PA
A
B
3
pred2
PB
A
4
pred3
PA
C
B,C
Q= {1,2,3,4}
E={A,B,C}
q0 = 1
l = { 1a, 2a {PA},3a {PB, pred2}, 4a {PA,pred3} }
T={ (1,A,2),(1,B,1),(1,C,1),(2,A,2),(2,B,3),(2,C,1),
(3,A,4),(3,B,1),(3,C,1) }
Tino Cortesi
Tecniche di Analisi di Programmi
15
Paths, Esecuzioni, Stati raggiungibili
Un path in un automa A è una sequenza s, finita o infinita, di
transizioni (qi, ei, q’i) di A tale che per ogni i q’i= qi+1.
La lunghezza di un path è il numero (potenzialmente infinito) di
transizioni del path
Una esecuzione parziale è un path che parte dallo stato iniziale
Una esecuzione completa è un’esecuzione che non può essere
estesa
Uno stato è raggiungibile se esiste almeno un’esecuzione
parziale (quindi che parte dallo stato iniziale) in cui esso appare.
Tino Cortesi
Tecniche di Analisi di Programmi
16
PRINTER MANAGER
W= wait
P = print
R = rest
0
RA RB
endB
endA
reqA
6
PA RB
begA
reqB
1
2
WA RB
RA WB
reqB
endB
4
WA PB
begB
reqA
3
WA WB
7
RA PB
endA
5
PA WB
reqA
reqB
Tino Cortesi
begA
begB
Tecniche di Analisi di Programmi
17
Proprietà che vorremmo verificare sul Printer Manager
In ogni esecuzione, ogni stato in cui vale PA è preceduto da uno stato
in cui vale WA
Questa si può verificare! (… anche a mano)
In ogni esecuzione ogni stato in cui vale WA è seguito (non
necessariamente subito) da uno stato in cui vale PA.
Questa non vale! E le tecniche di model checking in questo caso
ci forniscono un controesempio…
Tino Cortesi
Tecniche di Analisi di Programmi
18
IL PRINTER MANAGER
NON E’ FAIR
0
RA RB
endB
endA
reqA
6
PA RB
begA
reqB
1
2
WA RB
RA WB
reqB
endB
4
WA PB
begB
reqA
3
WA WB
begA
begB
7
RA PB
endA
5
PA WB
reqA
reqB
Controesempio: 0 1 3 4 1 3 4 1 3 4 1 3 4 1 3 4 1 3 4 …
Tino Cortesi
Tecniche di Analisi di Programmi
19
Automi con variabili
Quando si vuole modellare un sistema, dobbiamo considerare
anche variabili legate agli stati
Se programma = controllo + dati
la coppia <stati, transizioni> rappresenta il controllo
Le variabili rappresentano dati
Esempio: Nel sistema di “apertura luchetto”, se volessimo
contare il numero di errori fatti dall’utente e volessimo tollerare
al massimo 3 errori, dovremo introdurre una variabile intera ctr
con valore iniziale 0, per accumulare il numero degli errori
Tino Cortesi
Tecniche di Analisi di Programmi
20
Interazione variabili-automa
L’automa interagisce con le variabili in due modi:
Assegnamento: una transizione può modificare il valore di
una o più variabili
Guardia: una transizione può essere determinata da una
condizione sulle variabili: una transizione non può avvenire
finché non vale una certa condizione sulle variabili.
Tino Cortesi
Tecniche di Analisi di Programmi
21
int ctr;
if ctr<3
B,C
ctr++
ctr=0
if ctr<3
A
ctr++
A
1
if ctr<3
C
ctr++
if ctr=3
B,C
ctr++
Tino Cortesi
if ctr<3
B,C
ctr++
B
2
if ctr=3
A,C
ctr++
3
A
4
if ctr=3
B,C
ctr++
err
Tecniche di Analisi di Programmi
22
Unfolding
Per applicare le tecniche di model checking è spesso necessario
fare l’unfolding di automi con variabili in uno state graph in cui
appaiono solo le possibili transizioni
In questi casi si parla più propriamente di sistema di transizioni
(transition system)
Gli stati di un unfolded automa sono chiamati stati globali
Tino Cortesi
Tecniche di Analisi di Programmi
23
1
ctr=0
A
2
ctr=0
A
B
3
ctr=0
A
4
ctr=0
3
ctr=1
A
4
ctr=1
3
ctr=2
A
4
ctr=2
3
ctr=3
A
4
ctr=3
B,C
B,C
1
ctr=1
A
A
B,C
1
ctr=2
A
2
ctr=2
A
B,C
1
ctr=3
2
ctr=1
A
2
ctr=3
B
B,C
B
B,C
B
err
ctr=4
Tino Cortesi
Tecniche di Analisi di Programmi
24
Sincronizzazione
Quando si ha a che fare con sistemi reali, questi sono composti
da sottosistemi o moduli.
Un automa globale si ottiene dalla cooperazione e
sincronizzazione degli automi che corrispondono alle
sottocomponenti del sistema
La situazione più semplice è quando le sottocomponenti non
interagiscono tra di loro. In questo caso l’automa globale è
ottenuto facendo il prodotto cartesiano degli automi che
rappresentano le componenti. Ad esempio, per modellare un
sistema costituito da un contatore modulo 2, un contatore
modulo 3 ed un contatore modulo 4, costruiremo un automa
con 2x3x4 stati.
Tino Cortesi
Tecniche di Analisi di Programmi
25
1,0,3
0,0,3
1,1,3
0,1,3
1,0,2
0,0,2
1,1,2
1,0,1
Tino Cortesi
1,2,2
0,2,2
1,1,1
0,1,1
1,0,0
0,0,0
0,2,3
0,1,2
0,0,1
1,2,3
1,2,1
0,2,1
1,1,0
0,1,0
Tecniche di Analisi di Programmi
1,2,0
0,2,0
26
Sincronizzazione mediante
scambio di messaggi
Distinguiamo tra le etichette delle transizioni quelle associate
all’emissione di un messaggio !m e quelle associate alla
ricezione di un messaggio ?m
Nel prodotto sincronizzato saranno permesse solo le transizioni
in cui una data emissione è eseguita contemporaneamente alla
corrispondente ricezione
Tino Cortesi
Tecniche di Analisi di Programmi
27
Ascensore: la cabina
?down
?up
?up
?down
Tino Cortesi
2
1
0
?up
?down
Tecniche di Analisi di Programmi
28
Ascensore: la i-esima porta
?open_i
?close
?open_i
Open
Closed
?close_i
Tino Cortesi
Tecniche di Analisi di Programmi
29
Ascensore: il controller
!close_2
free2
on2
2->0
!close_1
free1
!up
!down
!open_2
!down
on1
free0
!up
!close_0
!down
!open_1
0->2
on0
!open_0
Tino Cortesi
Tecniche di Analisi di Programmi
30
Ascensore: l’automa prodotto
L’automa che modella l’ascensore si può quindi ottener come
prodotto sincronizzato di questi 5 automi (3 porte, cabina,
controller)
Uno stato dell’automa risultante avrà quindi 5 componenti,
corrispondenti allo stato della porta 0, porta 1, porta 2, cabina e
controller
I vincoli di sincronizzazione riducono le possibili transizioni alle
emissioni sincronizzate con ricezioni si messaggi espresse da:
Sync={ (?open0,-,-,-,!open0),
(-,?open1,-,-,!open1),
(-,-,?open2,-,!open2),
(-,-,-,?down,!down),
Tino Cortesi
Tecniche di Analisi di Programmi
(?close0,-,-,-,!close0),
(-,?close1,-,-,!close1),
(-,-,?close2,-,!close2),
(-,-,-,?up,!up) }
31
Proprietà verificabili (1)
La porta di un certo piano non si apre se la cabina è ad un
piano diverso
Per la porta 0 questa si traduce nel fatto che ogni stato che ha
Open come prima componente ha 0 come quarta componente
Questa proprietà si può esprimere usando proposizioni atomiche
Idem per le altre porte
Tino Cortesi
Tecniche di Analisi di Programmi
32
Proprietà verificabili (2)
La cabina non si muove se una delle porte è aperte
Provare questa proprietà è più delicato: dobbiamo provare che
in ogni esecuzione, uno stato in cui una delle prime 3
componenti è Open non può essere seguito immediatamente da
uno stato in cui la quarta componente è diversa
Una proprietà di questo tipo può essere verificata
automaticamente da un model checker
Tino Cortesi
Tecniche di Analisi di Programmi
33
Sincronizzazione
con variabili condivise
Un altro modo per permettere la comunicazione tra sottosistemi
è quello di lasciarli condividere alcune variabili
Ad esempio, se vogliamo migliorare l’automa della stampante
unfair descritta precedentemente, possiamo introdurre una
variabile turn che indichi quale dei due utenti ha diritto di
stampare
Tino Cortesi
Tecniche di Analisi di Programmi
34
Utente A ed utente B
If turn=A printA
x
y
turn=B
If turn=B printB
z
t
turn=A
Tino Cortesi
Tecniche di Analisi di Programmi
35
Stampante: automa globale
L’automa globale che descrive il sistema includendo sia l’utente
A che l’utente B può essere costruito da questi due automi e dal
valore della variabile condivisa turn
x,z,A
printA
turn=A
x,t,B
Tino Cortesi
y,z,A
turn=B
printB
Tecniche di Analisi di Programmi
x,z,B
36
Osservate che…
Questo protocollo garantisce che non si raggiunga mai lo stato
(y,t,-)
Garantisce che non possa mai essere usata la stampante
contemporaneamente
Ma impedisce anche che ci possano essere due stampe
consecutive da parte dello stesso utente!!!
Tino Cortesi
Tecniche di Analisi di Programmi
37