13-Verifica-I

Lezione 13. Verifica (I)
•
•
•
•



Generalità; verification & validation
Algoritmi di analisi per modelli a stati finiti
Reachability analysis
•

[S2001, Cap. 19]
[GMJ91, Cap. 6]
[R85, Cap. 6]
Articoli citati in queste diapositive, e appunti
limiti e possibili soluzioni
Algoritmi e complessità di problemi per reti di Petri
•
•
boudedness, reachability in P/T nets e Time PN’s
analisi degli invarianti
[R85] W. Reisig, Petri Nets - An Introduction, EATCS Monographs on Theoretical Computer Science,
Vol. 4, Springer-Verlag, 1985.
Slide 1
Verification and Validation (V&V)

[S2001] Verification and Validation (V&V)
•

‘checking processes which ensure that software
conforms to its specification (at each phase in the
development) and meets the needs of the software
customer’.
[Boehm’79]
•
•
Verification: "Are we building the product right”?
Validation: "Are we building the right product”?
Slide 2
Dynamic V&V and static verification

Dynamic V & V
•
•

Concerned with exercising and observing product
behaviour (testing)
…and also executable formal specifications
Static verification
•
Concerned with analysis of the static system
representation to discover problems
Slide 3
Verifica/validazione statica/dinamica
Statica
Dinamica
Verifica
Validazione
*
*
*
Slide 4
Static
verification
Requirements
specification
High-level
design
Formal
specification
Detailed
design
Program
Dynamic
validation
Prototype
and verification
[Sommerville]
Slide 5
Molteplicità di tecniche di verifica

Nelle diverse fasi del ciclo di sviluppo, il sistema è rappresentato con
diversi modelli e linguaggi:
•
Requirements def. and spec., software spec.
» (specifiche informali in linguaggio naturale)
» specifiche semi-formali: Entity-Relation, Data Flow...
» specifiche formali: FSM’s, Petri nets, Basic LOTOS...
•
Design
» specifiche formali: Ext. FSM’s, PrT nets, Full LOTOS, UML...
•
Implementation
» Codice Fortran, C, C++, Java…

Ad ogni modello e linguaggio corrispondono spesso piu’ tecniche
(statiche e dinamiche) di verifica
Slide 6
Panoramica di tecniche di verifica

Modelli a stati finiti
•
•

•
algoritmi di verifica di
proprietà decidibili:
boundedness...
Analisi di invarianti
Algebre di processo (LOTOS)
•

•
Specifiche in Petri Nets o Algebre di
Processo possono essere riconducibili a
FSM, ed ereditarne le tecniche di analisi
Esecuzione simbolica (*)
Analisi statica
Theorem proving (*), manuale o
automatico
Testing (*)
» in the small, in the large

Altre rappresentazioni, come ER, DFD,
UML, architetture a oggetti…, si prestano a
tecniche di analisi ‘superficiale’
(sintattica).

Molte tecniche (*) sono
‘trasversali’, cioè applicabili a
piu’ modelli
Verifica di equivalenze (e
preordini), tramite
» algoritmi di partition refinement
» assiomatizzazioni e sistemi di
riscrittura
Codice o pseudo-codice
•
•
•
Reachability analysis (*)
Model checking (*)
Petri Nets
•


Slide 7
Reachability analysis

Si applica a reti di (X)FSM’s, ma anche a qualunque modello il cui
comportamento è riconducibile a un sistema finito di transizioni fra stati globali
(ad esempio, per classi di Petri nets, sotto-insiemi di LOTOS…)

In una rete di n XFSM’s (X1, …, Xn) lo stato globale è una matrice n x n:
X1
X1
X2
Xn
X2
s1 q12
q21 s2
...
...
qn1 qn2
...
...
Xn
q1n
q2n
sj è lo stato di Xj,
comprendente i valori delle
sue variabili locali
qhk e’ il contenuto
della coda Xh-->Xk
sn
Slide 8


Si ha una transizione globale, fra due stati globali, quando qualche macchina Xi
compie (atomicamente) una transizione locale.
Nello stato globale di arrivo sono in generale modificati:
•
•

si
qhi per un qualche h (input); qik per un qualche k (output)
Per rendere finito il grafo globale si considerano:
•
•
variabili locali e messaggi a valori finiti
code FIFO di capacita limitata

Il grafo globale finito (GG) viene costruito con l’algoritmo ovvio, chiamato
global state exploration, reachability analisys, perturbation technique, …

Ai fini della analisi del GG è conveniente calcolarne le componenti fortemente
connesse (strongly connected components - SCC).
Slide 9
Tipiche proprietà verificabili con reachability analysis

Unspecified reception
•

Deadlock statico
•

un ciclo di transizioni la cui esecuzione (se iterata indefinitamente)
rappresenta mancanza di ‘progresso’ del sistema
SCC senza transizioni verso altre SCC
•

un nodo di GG senza transizioni in uscita. In assenza di unspecified
receptions, cio’ implica code vuote.
Cicli improduttivi (deadlock dinamico)
•

incapacità, da parte di una XFSM, di ricevere il messaggio disponibile in
testa a una sua coda in input
generalizzazione di ciclo improduttivo
Stati (globali o locali) desiderabili ma non raggiungibili a partire dallo
stato iniziale
Slide 10
Alcune applicazioni significative di reachability analysis

Analisi di protocolli CCITT X.21, X.25, IBM/SNA (System Network
Architecture) - Data Flow Control layer, IBM Token-ring protocols.
•

[IBM Zurigo, C. West, P. Zafiropulo, H. Rudin1978…]
Analisi di protocolli:
•
•
•
•
•
alternating-bit,
sliding window,
ISO-OSI architecture/layer ‘transport’, ‘session’,
su specifiche in Estelle, SDL -innumerevoli articoli in serie conferenze IFIP WG6.1


PSTV - Protocol Specification, Testing, and Verification, dal 1981; e
FORTE - Formal description Techniques for distributed systems and
communication protocols, dal 1988.
Slide 11
Limite di reachability analysis: esplosione combinatoria...


...dovuta al prodotto degli spazi degli stati delle singole
macchine, e degli spazi dei valori delle singole code
...aggravata dall’ordinamento totale di eventi anche non
correlati causalmente:
•
•
•
a; stop ||| b; stop ||| c; stop =========>
a; b; c; stop [] a; c; b; stop [] b; a; c; stop [] … [] c; b; a; stop
cioè 8 stati:
1
2
a
c
b
c
a
b
a
b
c
c
b
a
8
Slide 12
Rimedi alla esplosione combinatoria




Ulteriori restrizioni su stati e canali (debole)
Rappresentazione e manipolazione dello stato globale con
strutture dati ed algoritmi efficienti (hash tables, bit-based
state encoding…)
Trattazione diretta di ordinamenti parziali degli eventi
Rappresentazione simbolica di grandi insiemi di stati
•

tutti quelli che soddisfano una formula, p. es. una disuguaglianza
Uso di BDD’s (Binary Decision Diagrams - Bryant 1986)
•
•
rappresentazione canonica di formule booleane basata su grafi, che
consente una efficiente implementazione di op. booleane (/\, \/, ¬),
verifica di soddisfacibilità, e di equivalenza fra formule.
Usati per verificare (model checking) modelli a 10120 stati!
Slide 13
Verifica di proprietà specifiche di Reti di Petri

Place/Transition Petri nets (P/T net) N=(S, T, A, W, M0),
•
•
•
•
•

M [t > M’
•

nel marking M la transizione t è abilitata, e la sua esecuzione porta
al marking M’
[M >
•

S = Places,
T = Transitions,
A = Arcs (A  PT  TP)
W = Weight (W: A -> Nat\{0}) (quanti token alla volta)
M0 = marking iniziale (Marking: S -> Nat)
insieme dei marking raggiungibili dal marking M
GG(N)
•
Grafo globale, con nodi [M0 > e transizioni tipo M [t > M’
Slide 14
Verifica di boundedness

Boundedness:
•
 K Nat:

•

 M in [M0>, p in S: M(p) < K
ovviamente una P/T net N è bounded sse GG(N) è finito
Boundedness per P/T nets è una proprietà decidibile -•
•
•
cioè esiste un algoritmo che decide sempre, e in un numero finito di
passi, se una generica rete P/T e’ bounded
… ma provare a costruire direttamente GG(N) non è una buona
idea: quando fermarsi?
È necessario introdurre un nuovo tipo di grafo globale:……...
Slide 15

Coverability graph CG(N)
•
•
simile a GG(N), ma con marking ‘estesi’:
Marking (esteso): S -> Nat  {}
»  etichetta un posto ‘divergente’, nel quale i token possono crescere
illimitatamente
•
•
M < M’ (M’ copre M) se per ogni p in S, M’(p) > M(p),
con  > n per ogni n in Nat.
In CG(N) ogni nodo è un marking reale di N oppure un
marking esteso che copre dei marking reali di N.
Slide 16
In GG(N): Marking M1=(4, 2, 3, 8) e M2=(6, 2, 3, 8), con M2  [M1>, implicano
M3=(8, 2, 3, 8); M4=(10, 2, 3, 8), …..
==> in CG(N): Marking M=(, 2, 3, 8)
9
8
8
8
Tokens
7
6
6
5
4
4
3
3
2
3
2
2
1
0
1
2
3
4
Posti
Il marking esteso M rappresenta in CG(N) una serie infinita e crescente di marking in GG(N)
Slide 17

Def. - Dati due marking estesi M1 e M2:
» M1 # M2
se
 (M1 > M2) e  ( M2 > M1)
» (M1 ed M2 sono ‘inconfrontabili’)

Per la precedente costruzione, i marking del CG(N) sono inconfrontabili
a due a due

Th.1 - Il coverability graph CG(N) di una P/T net N è sempre finito

Dimostrazione (cenno)
•
La dimostrazione, per induzione, si basa sul fatto che non possono esistere
infiniti marking estesi che siano inconfrontabili a due a due.
Slide 18
•
•
•
Nel caso di due soli posti, si assuma per assurdo un insieme infinito MM di
marking a due a due inconfrontabili.
Sia M=(h, k) in MM un marking di riferimento, con h , k  (deve
esistere…)
L’insieme di tutti gli altri marking in MM, di tipo M’(x, y), è bipartito in:
» MMh: i marking che hanno x<h
» MMk: i marking che hanno y<k
•
•
•
•
e uno dei due sottoinsiemi deve essere infinito, poniamo MMh.
Ripartire MMh in classi MMh(0), MMh(1), … MMh(h-1), ciascuna con la
prima componente x fissa:
ancora, uno degli h sottoinsiemi deve essere infinito, poniamo MMh(1)
ma ciò è impossibile, perche i suoi elementi sarebbero tutti confrontabili fra
loro, essendo (1, y1), (1, y2), … []
Slide 19

Th.2 - Una P/T net N è bounded (e il suo GG(N) è finito) sse CG(N) non
contiene alcun nodo con una componente 

Dimostrazione
•
Immediata conseguenza della definizione di CG(N). []
Slide 20
Coverability - Simultaneously unbounded

Coverability
•
•
un generico marking M è copribile se esiste in GG(N) un marking
M’ tale che M < M’
Decidibile
» Cercare in CG(N) un nodo M’’ tale che M < M’’…

Insieme di posti simultaneously unbounded
•
•
un generico insieme P’  S di posti è simultaneously unbounded se
 i  Nat,  un marking Mi in GG(N) tale che  p  P’: Mi(p) > i
Decidibile
» Cercare in CG(N) un nodo M’ tale che  p  P’: M’(p) = 
Slide 21
Reachable transition

Sia t una generica transizione ed M un generico marking
t è M-dead se  M’  [M>, t non è abilitata da M’

Reachable transition

•
•
una generica transizione t è una reachable transition se non è M0dead
Decidibile
» Cercare in CG(N) un arco di tipo M--t-->M’

Le proprietà viste fin qui sono desumibili dalla ispezione di CG(N); tuttavia la costruzione
di questo grafo è poco pratica
•
•
si dimostra che la sua dimensione puo’ crescere, rispetto alla dimensione della rete, piu’
rapidamente di qualunque funzione primitiva ricorsiva.
Si dimostra anche che la complessità di alcuni di questi problemi è di fatto inferiore a quella
della costruzione di CG(N), e cio’ apre la strada ad algoritmi di analisi piu’ efficienti.
Slide 22
Reachable marking (‘Reachability’)

Reachable marking
•

un generico marking M è reachable se M  [M0>
Questo problema, aperto nel 1969 [KM69], non è
banalmente risolvibile per ispezione di CG(N).
• Decidibile
» La soluzione, ottenuta dopo 13 anni (!), è dovuta a Kosaraju [K82],
con correzione di H. J. Muller (82), precedenti tentativi e contributi di
J. Van Leeuwen (‘74), G. S. Sacerdote e R. L. Tenney (‘77), J. Hopcroft
e J. J. Pansiot (‘79), E. W. Mayr (‘81)...


[KM69] R. M. Karp, R. E. Miller, ‘Parallel Program Schemata’, Journal of Computer and System Sciences, 3 (1969), pp.
147, 195 (introduce Vector Addition Systems, un modello equivalente alle reti di Petri)
[K82] S. R. Kosaraju, ‘Decidability of Reachability in Vector Addition Systems’, Proceedings of Fourteenth Annual ACM
Symposium on Theory of Computing, 1982, pp. 267-281.
Slide 23
Liveness

Live transition
•
una transizione t è M-live se
»  M’  [M>: t non è M’-dead (dunque  un M’’  [M’>, tale che M’’
abilita t)
» (M-live non è la negazione di M-dead !)

Live net
•
una P/T net N è live se ogni transizione è M0-live
» Decidibile [Lipton ‘76]
Slide 24
Verifica di proprietà di Time Petri Nets

Time Petri Nets (Merlin’76) hanno maggior potenza
espressiva delle P/T nets
•


infatti possono simulare le Turing Machines
Conseguentemente sono meno analizzabili.
Ad esempio, le proprietà:
• reachability
• boundedness
• diventano indecidibili [JLL77]
•
[JLL77] N. D. Jones, L. H. Landweber, Y. E. Lien, Complexity of some problems in Petri Nets,
Theoretical Computer Science 4, (1977), 277-299.
Slide 25
Analisi degli S-invarianti per Reti di Petri

Place/Transition Petri nets (P/T net) N=(SN, TN, AN, WN, MN),
•
•
•
•
•

[R85, Cap. 6]
SN = Places,
TN = Transitions,
AN = Arcs (A  PT  TP)
WN = Weight (W: A -> Nat\{0}) (quanti token alla volta)
MN = marking iniziale (Marking: SN -> Nat)
Rappresentazione algebrica lineare di P/T nets
•
•
per ogni t  TN definiamo il vettore t : SN --> Int:
t(s) =
»
»
»
»
•
•
W(t, s)
- W(s, t)
W(t, s) - W(s, t)
0
sse
sse
sse
altrimenti
s  t* \ *t
s  *t \ t*
s  *t  t*
(*t = posti in output da t)
(t* = posti in input di t)
La matrice N: SN  TN --> Int è definita come: N(s, t) = t(s)
dunque i vettori t sono le colonne di N.
» N(s, t) descrive il cambio del marking di s quando t viene eseguita
Slide 26




Ogni marking è rappresentato da un vettore a |SN| elementi
Se la rete soddisfa alcune semplici proprietà (‘pura’, cioè senza coppie di
archi a loop, e ‘contact-free’...)
… allora il comportamento della rete è completamente determinato dalla
matrice N e il vettore MN
La firing rule diventa:
•
•
se t è M-abilitata, allora:
M [t> M’
sse
M + t = M’
Slide 27

Sia S  SN un insieme di posti la cui somma di token non varia con
l’esecuzione della transizione t. Allora:
•  s *t  S W(s, t) =  s t*  S W(t, s)
• … che, in base alla definizione del vettore t diventa
•  s *t  S t(s) = - s t*  S t(s)
cioè
•  s *t  S t(s) +  s t*  S t(s) = 0
cioè
•  s (*t  t*)  S t(s) = 0
cioè
•  s S t(s) = 0
• rimpiazzando S con il suo vettore caratteristico cs (a |SN| componenti):
•  s SN t(s) * cs (s) = 0, cioè
t * cs = 0
• … e se il numero di token in S non cambia per alcuna transizione, cio’
vale per tutte le transizioni, cioè
• N’ * cs = 0
(N’è la matrice trasposta di N: N’(x, y) = N(y, x))
Slide 28

S-invariant
•
Un vettore inv:SN-->Int è un S-invariante di N sse N’*inv = 0

Lemma. Sia inv un invariante, M ed M’ due marking, t una transizione Mabilitata, con M [t> M’. Allora: M*inv = M’*inv.
Dim. M’*inv = (M + t )* inv [M [t> M’ sse M + t = M’ (slide 28)]
= M* inv + t * inv
[distributività]
= M* inv
[N’*inv = 0 => t * inv = 0, essendo N = (t1, t2, …)]

Lemma



•
Siano i1 e i2 due S-invarianti di N, e z un intero. Allora:
» i1 + i2
è un S-invariante
» z*i1 è un S-invariante
Slide 29
Verifica di sistema ad accesso controllato
La conoscenza degli invarianti di una rete puo’ rivelare alcune
interessanti proprietà del sistema modellato. Esempio:
N processi accedono un buffer in lettura o scrittura
Se nessun processo sta scrivendo, fino a k < n processi possono leggere;
ma la scrittura è consentita solo se nessuno sta già leggendo o scrivendo



k
k
s4
t5
k
s5
t2
s2
s0
t4
n
s3
t3
t1
t0
s1
s0 = processi inattivi
s1 = processi pronti a leggere
s2 = processi che leggono
s3 = processi pronti a scrivere
s4 = processi che scrivono
s5 = sincronizzazione
Slide 30
k
k
s4
t5
k
s5
t0 t1 t2 t3 t4 t5 i1 i2 MN
t2
s2
s0
t4
n
t1
s3
t3
s1
t0
s0
s1
s2
s3
s4
s5
-1
1 -1
1 -1
1 -1
Si verifica che:
N’ * i1 =
N’ * i2 =
1
1
-1
1
n
1
1
N
0
0
0
0
0
0
1
-1
1
1 -1
1
-k
k
1
k
1
k
invarianti
0
0
0
0
0
0
Slide 31
k
k
s4
t5
k
s0 = processi inattivi
s1 = processi pronti a leggere
s2 = processi che leggono
s3 = processi pronti a scrivere
s4 = processi che scrivono
s5 = sincronizzazione
s5
t2
s2
s0
t4
n
Invariante i2 (0,0,1,0,k,1)
t1
s3
t3
t0
s1
Invariante i1 (1,1,1,1,1,0)
 M  [MN>
M * i1 =  i = 0,4 M(si) =
MN * i1 =  i = 0,4 MN(si) = n
Interpretazione
s0-s4 sono i posti dei processi; dunque
i processi rimangono costanti,
e ciascuno è sempre in uno degli ‘stati’ s0-s4
 M  [MN>
M(s2) + k*M(s4) + M(s5) =
MN(s2) + k* MN(s4) + MN(s5) = k
Interpretazione
- s4 contiene sempre al piu’ un token: c’è un
solo scrivente alla volta.
- Quando s4 ha un token, s2 e s5 sono vuoti:
mentre uno scrive, nessuno legge.
- s2 ha al piu’ k token: al piu’ k processi
leggono concorrentemente
Slide 32

La conoscenza degli invarianti puo’ aiutare nella
dimostrazione di varie altre proprietà, per esempio liveness
[R85, pag. 83]
Slide 33