Lezione 15. Verifica (II)
•
•
•
•



[GJM91, Cap. 6]
[BB87]
[P93]
Appunti
1. Verifica di equivalenze per algebre di processo
2. Dimostrazione di correttezza di programmi
3. Esecuzione simbolica
[P93] V. R. Pratt, ‘Logics of Programs’, in A. Ralston, E. D. Reilly (Eds.) Encyclopedia of
Computer Science, IEEE Press, 1993 -- pp. 791
Slide 1
1. Verifica di equivalenze per algebre di processo

La natura algebrica di questi linguaggi offre
maggior varietà di strumenti di analisi rispetto ai
modelli a stati finiti
•
manipolazione e trasformazione di espressioni
algebriche mediante leggi algebriche e assiomatizzazioni
di relazioni
•
manipolazione diretta di Labelled Transition Systems
derivati dalla semantica formale
Slide 2


Tipico problema di verifica per specifiche LOTOS:
verifica di equivalenza osservazionale fra specifiche
sintatticamente diverse.
Esempio dall’architettura OSI:
a
b
UpperService
P Entity
P Entity
c
d
LowerService
hide c, d in
((P[a, c] ||| P[b, d]) |[c, d]| LowerService[c, d])

UpperService[a, b]
?
Slide 3
Equivalenza osservazionale



Un pianista (= osservatore) prova un tasto alla volta…
… che risulta premibile o bloccato in base alla partitura precedentemente inserita
Bechstain  Bluthner se nessun pianista cieco li può distinguere
Bluthner
Bechstain
do
mi


do
sol
mi
do
sol
La classica equivalenza fra automi (come riconoscitori di linguaggi) è inadeguata: la
musica possibile sui due strumenti è la stessa: {-, do, do-mi, do-sol}…
… ma i comportamenti rispetto a deadlock sono diversi: do-mi può fallire sul
Bluthner, non sul Bechstain
Slide 4
mi
do
2
4
mi
1
i
i
3
sol
7
--- (1 ... n ) --->
(1)---(do, mi)--->(4)
(1)---(i, do)--->(5)
(1)------>(1)
Action sequence:
•
•
•

8
5
do

6
Observable action sequence: === (a1 ... an ) ==>
•
•
•
•
[k  Gates i]
[ak  Gates]
(1)==(do, mi)==>(4)
(1)==(do, mi)==>(8)
(1)====>(1)
(1)====>(3)
Slide 5

Una relazione R fra stati di un LTS è una weak
bisumulation se:
•
 (p, q) R,  s Gates*
»
»
»
»
»

 p’ tale che p==s==>p’
( q’ tale che q==s==>q’ /\ (p’, q’)  R)
/\
 q’ tale che q==s==>q’
( p’ tale che p==s==>p’ /\ (p’, q’)  R)
p e q sono observation equivalent (p  q) se
•
 una weak bisimulation R tale che
» (p, q)  R
Slide 6
Due LTS equivalenti e la loro bisimulazione
P
Q
a
b
a
c
i
c
Bisimulazione R
a
b
i
c
PQ
Slide 7

L’equivalenza fra stati di LTS ne induce una fra espressioni di algebre di
processo

Una congruenza è una equivalenza preservata quando si rimpiazza una
sotto-espressione con un’altra sotto-espressione equivalente.
Formalmente:

Un contesto, denotato ‘C[ ]’, è una espressione in cui una sottoespressione è rimpiazzata da un ‘segna-posto’ (‘[ ]’)

B1 observation congruent B2 (B1 c B2) se per ogni contesto C[ ]:
•
C[B1]  C[B2] (che implica C[B1] c C[B2]…)
Slide 8
Se
Allora
c
c
Slide 9
Leggi della congruenza osservazionale

Per CCS o Basic LOTOS non è possibile fornire una assiomatizzazione
di c [M84]

Invece, per ‘finitary LOTOS’ (e, analog., f. CCS), comprendente solo
action prefix, choice, stop l’assiomatizzazione è possibile, mediante il
sistema completo e consistente di leggi [HM85]:
•
•
•
•
•
•
(a1)
(a1)
(a3)
(a4)
(a5)
(a6)
B [] (C [] D)
B [] C
B [] B
B [] stop
B [] i; B
 (B [] i; C)
=
=
=
=
=
=
(B [] C) [] D
C [] B
B
B
i; B
 (B [] C) [] ; C
[M84] R. Milner, Lectures on a Calculus for Communicating Systems, in International Summer School ‘Control
Flow and Data Flow: Concepts of Distributed Programming’, Munich, Germany, July 31-August 12, 1984.
[HM85] M. Hennessy, R. Milner, ‘Algebraic Laws for Nondeterminism and Concurrency’, Journal of the ACM,
Slide 10
Vol. 32, No. 1, Jan. 1985.
(a5)
(a6)
c
i
i


c
B

i
B
B
B
B
C
C
Esercizio: Dimostrare la legge (a7): a; i; B = a; B
a; i; B = a; (B [] i; B)
= a; (B [] B) [] a; B
= a; B [] a; B
= a; B
[a5]
[a6]
[a3]
[a3]
Slide 11
Esercizio di verifica di equivalenza
Max3[in1, in2, in3, out] :=
in1;
(in2; in3; out; stop
[] in3; in2; out; stop
)
[] in2;
(in1; in3; out; stop
[] in3; in1; out; stop
)
[] in3;
(in1; in2; stop
[] in2; in1; stop
)
in2
Max3-composto[in1, in2, in3, out] :=
hide mid in
Max2[in1; in2; mid]
|[mid]|
Max2[in3; mid; out]
where
Max2[in1; in2; out] :=
in1; in2; out
[]
in2; in1; out
in3
in2
in1
Max3
out
in1
Max2
in3
mid
Max2
out
Per verificare Max3  Max3-composto:
1. Costruire i due alberi T3 e T3-composto
2. Collassare 6 sottoalberi di T3-composto usando (a7)
3. Collassare 2 nuovi sottoalberi, usando (a5)
4. Collassare 2 nuovi sottoalberi, usando (a7), ottenendo T3.
Slide 12
2. Dimostrazione di correttezza di programmi

La dimostrazione formale di correttezza di programmi si basa
sull’utilizzo di una logica per esprimere proprietà dei programmi, e di
assiomi e regole per dimostrarle.

McCarthy (1963) modella i programmi come funzioni ricorsive
(esempio: definizione di append(list1, list2)), e ne dimostra proprietà per
induzione
Floyd (1967) definisce una logica per programmi imperativi espressi
come flowchart.

•
•

Associa asserzioni logiche (tags) agli archi, che devono essere vere ogni
volta che il controllo li attraversa.
Un tagged flowchart è dimostrato corretto quando, individualmente, ogni
componente è corretta rispetto ai suoi input/output tags.
Hoare (1969) raffina la logica di Floyd, trattando programmi imperativi
in forma algebrica
Slide 13

Specifica logica (di una proprietà) del programma P
{Pre (i1, i2, …, in) }
P
{Post (o1, o2, …, om, i1, i2, …, in) }

Pre e Post sono formule logiche del primo ordine,
in cui le variabili di input/output appaiono libere
Slide 14
Esempi di specifica logica di programmi
{ z (i1 = z*i2)}
P
{o1 = i1 / i2}
{i1 > i2}
P
{i1 = i2*o1 + o2 /\ o2 > 0 /\ o2 < i2}
{true}
P
{(o= i1 \/ o = i2) /\ o > i1 /\ o > i2}
{i1 > 0 /\ i2 > 0}
P
{( z1, z2 (i1 = o * z1 /\ i2 = o * z2))
/\
 ( h ( z1, z2 (i1 = h * z1 /\ i2 = h * z2) /\ h > o))}
Slide 15
Esempio di verifica di programma - esposizione informale



Programma e
proprietà
{true}
Begin
•
•
•



Dimostrazione

o = i1 + i2 vale dopo write(x) sse
immediatamente prima vale x = i1 + i2.
Ma l’assegnamento x := a+b scrive a+b in x,
quindi

read (a); read (b);
x := a + b;
write (x)
end
{o = i1 + i2}
•
•

x = i1 + i2 vale subito dopo l’assegn. sse
a+b = i1+i2 vale subito prima.
Poiché read(a) e read(b) danno ad a e b i valori
dei due input i1 e i2, a+b = i1+i2 deve valere
prima dell’assegnamento []
Slide 16
Le regole della logica di Hoare
Applicabili a un linguaggio di programmazione con i costrutti:
- x := exp (assegnamento)
- begin a1; a2; …; an end
- if p then a1 else a2
- while p do a
3.
{p}a1{q}, {q}a2{r}
-----------------------------------{p}a1;a2{r}
p’  p, {p}a{q}, q  q’
1. -----------------------------------{p’}a{q’}
4.
{p /\ r}a1{q}, {p /\ ¬r}a2{q}
-----------------------------------{p} if r then a1 else a2 {q}
2.
{p /\ q}a{p}
5. -----------------------------------{p} while q do a {p /\ ¬q}
-----------------------------------{p[exp/x]} x := exp {p(x)}
(NB: le graffe sono usate in modo inverso rispetto a [GJM91]
Slide 17
Esempio di verifica: fattoriale di y

Programma:

i) y>0 /\ x*y!=n! x:=y*x y>0 /\ x*(y-1)!= n!
•
•

B: while y>0 do C
C: x:=y*x; y:=y-1
first: y>0 /\ x*y! = n!
==> y>0 /\ (y*x)*(y-1)! = n!
then: y>0 /\ (y*x)*(y-1)! = n! x:=y*x y>0 /\ x*(y-1)!= n!
[rule 2, substituting x for y*x]
ii) y>0 /\ x*(y-1)!= n! y:=y-1 y>0 /\ x*y!= n!
•
•

A: x:=1; B
first:
then:
y>0 /\ x*(y-1)! = n! ==> (y-1) > 0 /\ x*(y-1)! = n!
(y-1) > 0 /\ x*(y-1)! = n! y:=y-1 y>0 /\ x*y!= n!
[rule 2, substituting y for y-1]
(iii) y>0 /\ x*y!=n! C y>0 /\ x*y!= n!
[rule 3, with (i) and (ii)]
Slide 18

(Programma:

(iii) y>0 /\ x*y!=n! C y>0 /\ x*y!= n!
(iv) y>0 /\ y=n /\ x=1 B x= n!

•
•
•
•
•
•
•
•

B: while y>0 do C
C: x:=y*x; y:=y-1)
y >0 /\ y=n /\ x=1 ==> p
(let p = y >0 /\ x*y! = n!)
Let q = y > 0
then:
(iii) becomes:
q /\ p C p
which yields:
p while q do C p /\ ¬q
[by rule 5]
that is
p B p /\ ¬q
p /\ ¬q = y >0 /\ x*y! = n! /\ y < 0 ==> y=0 /\ x=n! ==> x=n!
In conclusion: y >0 /\ y=n /\ x=1 ==> p, p B p /\ ¬q, p /\ ¬q ==> x=n!,
thus (iv)
[by rule 1]
(v) y>0 /\ y=n x := 1 y>0 /\ y=n /\ x=1
•

A: x:=1; B
since p x := 1 p /\ x=1
(vi) y>0 /\ y=n A x=n!
[by rule 2]
[rule 3 to (v) and (iv)] []
Slide 19
3. Esecuzione simbolica


Una tecnica a metà fra analisi di correttezza (statica) e testing (dinamica)
Si consideri questo programma P, e il suo grafo control-flow annotato
1. x := y + 2;
2. if [x > a] then
3.
a := a + 2;
else
4.
y := x + 3;
endif;
5. x := x + a + y.
3
y := x + 3
4
1
x := y + 2
x:= x + a + y
[x > a]
2
a := a + 2
Esecuzione simbolica: si associano valori iniziali simbolici alle variabili di programma (stato
simbolico iniziale), poi...:
init.
1.
2.
3.
4.
5.
[Y+2<A]
x X
y Y
a A
Y+2
2*Y+A+7
Y+5
Slide 20

L’esecuzione simbolica ha prodotto la tripla:
•
[a = A, y = Y+5, x = 2*Y+A+7],
stato simbolico finale (SSfin)
» (assegnamento di espressioni simboliche, contenenti variabili simboliche (maiuscole),
alle variabili di P (minuscole).
•
<1, 3, 4>,
execution path
» cammino lungo il control flow graph di P
•
[Y+2<A]
path condition
» predicato sulle variabili simboliche che garantisce la eseguibilità del path



L’altra tripla possibile è
< [a = A+2, y = Y, x = 2*Y+A+4], <1, 2, 4>, [Y+2>A] >
La corrispondenza biunivoca fra execution path e path condition cade per i linguaggi
nondeterministici
Slide 21




input e output file sono trattati come sequenze (i1, i2,…) e (o1, o2, …) di var. di
programma. Inizialmente: i1 = I1, i2 = I2, … o1 = nil, o2 = nil, …
Il primo Read (x) viene interpretato come x := i1, dunque la sua esecuzione
simbolica produce: x = ValSimb(i1) = I1
Il primo Write (E) viene interpretato come o1 := E, dunque la sua esecuzione
simbolica produce: o1 = ValSimb(E) (in termini dello stato simbolico corrente)
Quando si incontra nel programma una condizione cond, come in
•
•

if cond then S1 else S2 endif
while cond Loop
… si considera ValSimb(cond):
•
•
se il risultato è TRUE o FALSE indipendentemente dai valori delle variabili
simboliche, si procede secondo il ramo corrispondente
se no, si sceglie nondeterministicamente TRUE (risp. FALSE), e si aggiorna la path
condition PC: PC := PC /\ ValSimb(cond) (resp. PC := PC /\ ¬ValSimb(cond) )
Slide 22
Verifica tramite esecuzione simbolica

In generale, per ogni programma P si hanno molte, o infinite triple

P programma
inp = (inp1, ..., inpn)
tupla di variabili in input per P
I
= (I1, ..., In)
una corrispondente tupla di variabili simboliche
out = (out1, ..., outn)
tupla di variabili in output per P
<
Per verificare {Pre(inp)}P{Post(out)} con esecuzione simbolica:
calcolare tutte le triple (SSFini, ExecPathi, PathCondi(I)). Per ogni i:






•
•
•
•

usare sempre la stessa Path Condition iniziale: Pre(I)
assumendo SSFini = (out1= Exp1i(I)), ..., (outn = Expni(I))
e definendo il predicato PEi come: PEi(I) = Post(Exp1i(I)/out1, ..., Expni(I)/outn)
verificare che PathCondi(I) ==> PEi(I)
(Trattazione semplificata, senza rappresentazione delle variabili interne di P.)
Slide 23
Backward symbolic execution (of protocols) [G. Holzmann, PSTV IV, 1985]

E’ una variante di reachability analysis: dato uno stato finale indesiderabile Sx,
calcola transizioni a ritroso fino, possibilmente, a S0

Il sistema distribuito -- un protocollo -- viene descritto con un linguaggio simile
al CSP di Hoare:
•
•
•
•
•
•
•
•
qname !mname
qname ?mname
qname
v1 := v2
v++
v-[v1 R v2]
output; appende mess. mname in coda a qname
input; eseguibile se mess. mname è correntemente in cima a
(con cancellazione)
assegnamento v1 è una var., v2 è una var. o una costante
incrementa di 1 la variabile v
decrementa di 1 la variabile v
condizione, dove R è =, , , , <=, >=; eseguibile se i due
operandi (var. o costanti) sono in relazione R
I do loops (do…od), sono interrotti dal comando break. Skip è il comando vuoto.
::
individua scelte non deterministiche
Slide 24
Esempio - Protocollo con memoria condivisa (M, N)
Slide 25





Due processi A e B condividono le code A (verso A) e B (verso B).
Il processo A si rifornisce dalla coda TOB di messaggi che vorrebbe mandare al
processo B attraverso la coda B. B si comporta simmetricamente.
La variabile condivisa N è incrementata dal processo A quando un messaggio è
appeso alla coda B, ed è decrementata dal processo B quando un messaggio viene
cancellato.
Simmetricamente, la variabile condivisa M è incrementata dal processo B quando
un messaggio è appeso alla coda A (verso A), ed è decrementata dal processo A
quando un messaggio viene cancellato.
Il protocollo forza ciascun processo a ritardare il trasferimento di messaggi verso
l’altro quando le code sono sature (2 messaggi)
Slide 26

Vogliamo verificare se dallo stato globale iniziale S1:
•
•
•

N = 0,
M=0
TOB = (msg, msg), TOA = (msg, msg)
A = ( ),
B=()
...si puo’ arrivare allo stato di deadlock S2:
•
•
•
N = 2,
TOB = ( ),
A = (msg, msg ),
M=2
TOA = ( )
B = (msg, msg)

Anziché esplorare tutti i cammini da S1 fino a trovare eventualmente S2, si puo’
partire da S2 e vedere se S1 è raggiungibile a ritroso.

Inoltre, la esecuzione a ritroso (inversa) della specifica originale equivale a una
esecuzione diretta della specifica inversa così costruita:
Slide 27





Scambiare send con receive
(? con !)
Scambiare incrementi con decrementi
(++ con --)
Invertire il flusso di controllo
Scambiare condizioni con assegnamenti
(= con :=)
ma usando anche assegnamenti con range di valori (tipico della esecuzione
simbolica):
•
•
•
Condizione
Assegnamento
------------------------------------------[N > 5]
==>
N := (>5)
•
[N  2]
==>
N := 2
La specifica originale del processo A è convertita in una tabella a stati,
che viene invertita ed eseguita in maniera diretta, a partire dallo stato S2.
Slide 28
La specifica originale del processo A è convertita nella tabella a stati:
Forward table for process A
State/actions TOB ?msg [N = 2]
N++
B !msg
[N  2]
0
1
1
1
2
2
3
3
0
4
A ?msg
4
M--
0
La specifica inversa è rappresentata da questa tabella;
la sottolineatura distingue i nuovi elementi dai vecchi
State/actions TOB !msg
0
1
0
2
3
4
Backward table for process A
N := 2
N-B ?msg
N := 2
3
1
1
2
A !msg
M++
4
0
Slide 29

Effettivamente si scopre che, attraverso un doppio ciclo nel grafo degli stati
globali, il deadlock è raggiungibile.

La tecnica di esplorazione viene detta simbolica perché
•
viene concettualmente esplorato il programma, visto come lista di
statements
•
lo stato è la posizione nel programma, ma puo’ essere parzialmente
identificato anche da predicati sui valori di alcune variabili (come M ed
N), che ne ‘sfuocano’ la rappresentazione.

Sfortunatamente la esecuzione inversa non è sempre vantaggiosa rispetto a quella
diretta [cfr. Holzmann 85]

Un piu’ recente approccio alla interpretazione simbolica a ritroso, chiamato
Compositional backward technique, è descritto in [Staunstrup+, IEEE Computer,
Maggio 2000]
Slide 30