Convalida e Verifica - unige.itenrico/IngegneriaDelSoftware... · 2010. 9. 9. · Convalida e...

Convalida e Verifica

Enrico Giunchiglia Ingegneria del Software II 2

Convalida e Verifica   Convalida: attività volta ad assicurare che il SW sia

conforme ai requisiti dell’utente.   Verifica: attività volta ad assicurare che il SW sia conforme

alle specifiche dell’analista.   Goal: determinare anomalie/errori/malfunzionamenti nel SW

al fine di prevenire possibili guasti.   Strumenti: (non in contrapposizione ma complementari):

  Testing: basato su “analisi dinamica” del codice.   Metodi Formali: basato su “analisi statica” del codice.


  Anomalie: difetti nel sistema   Errori: stati difettosi del sistema   Malfunzionamenti: comportamenti errati

visibili   Guasti (primari): malfunzionamenti che

comportano interventi non programmati


Testing


Testing

“Il processo di valutazione di un sistema attraverso strumenti manuali o automatici col fine di determinare se il sistema soddisfa i requisiti specificati oppure se il suo comportamento attuale differisce da quello atteso”

(IEEE Std 829-1983, Standard for Software Test Documentation)


Tipologie di Testing

  Unit Testing,   Test di Integrazione,   Test di Sistema,   Test di Regressione,   Test di Accettazione (Alpha Testing),   Beta Testing.


Unit Testing   Attività volta a determinare la correttezza e

completezza (rispetto ai requisiti) di un programma visto come singolo modulo.

  Composto dalle seguenti attività (IEEE Std 1008-1987, Standard for Software Unit Testing):

1.  Pianificazione dell’approccio, risorse e tempistica, 2.  Individuazione delle caratteristiche da testare, 3.  Determinazione dell’insieme di test, 4.  Esecuzione dei Test, 5.  Verifica se altri altri test sono necessari, 6.  Valutazione dei risultati.


Determinazione dell’insieme di test

  Un programma P è una funzione da un insieme di dati D (Dominio) in un insieme di dati R (Codominio).

  Si consideri un programma P : D -> R.


  Un test T per P è un sottoinsieme di D.   Dato d ∈ D, P(d) è corretto (ok(P, d)) se soddisfa le

specifiche, non corretto altrimenti.   P è corretto in T (ok(P, T)) se per ogni t ∈ T, si ha

ok(P, t).   P è corretto (ok(P)) se P è corretto in D.   Un test T è ideale se la correttezza di P in T implica

la correttezza di P. (Da questo segue che il test D è ideale).


  Un Criterio di Selezione C per P è un insieme di sottoinsiemi di D.

  Un test T è selezionato da un criterio di selezione C se   Se ogni dato di test appartiene a qualche insieme nel criterio

(per ogni t ∈ T esiste c ∈ C t.c. t ∈ c), e   A ogni insieme nel criterio corrisponde almeno un dato di test

(per ogni c ∈ C esiste t ∈ T t.c. t ∈ c).   Esempio:

  Si consideri un programma P : IN → {Y,N}, e il criterio di selezione {{t | t pari}, {0}, {t | t primo}, {t | t > 1000}}.

  Tale criterio ad es. seleziona i test {6,8,0,7,37,1001}, {0,7,1002}.


  Un criterio di selezione C è affidabile se comunque presi T1 e T2 selezionati da C, si ha

ok(P, T1) ⇔ ok(P, T2).

  Un criterio di selezione C è valido se ¬ok(P) ⇒ ∃t.(selezionato(t,C) ∧ ¬ok(P, t))


Esempio

  Per tale programma, il criterio di selezione:   {{0}, {0,2}} è affidabile ma non valido,   {{0, 1},{2, 3, 4}} è valido ma non affidabile,   {{t | t > 3}, {t | t dispari}} è valido e affidabile.


Teorema (Goodenough, Gerhart) affidabile(C, P) ∧ valido(C, P) ∧ selezionato(C, T) ∧ ok(P, T) ⇒ ok(P)

Teorema (Howden): Non esiste un algoritmo che, dato un programma arbitrario P, generi un test ideale finito, e cioè un test finito definito da un criterio affidabile e valido.


  L'aver dimostrato che un certo criterio di selezione di test soddisfa particolari proprietà di affidabilità e validità per il programma inizialmente in esame, non garantisce nulla sulle proprietà godute dallo stesso criterio di selezione di test una volta che il programma in esame viene modificato


  I test generabili da {{0}, {0,2}} che {{0, 1},{2, 3, 4}} diventano test ideali

  {{t | t > 3}, {t | t dispari}} diventa valido (seleziona almeno un test che contiene un numero diverso da 5 e quindi rileva il malfunzionamento), ma non più affidabile


Tipologie di Testing Due criteri fondamentali:   Test funzionale o White Box Testing: basato sul

programma, indipendente dalle specifiche.   Test strutturale o Black Box Testing: basato sulle

specifiche del programma, indipendente dal programma stesso.

Questi due criteri sono complementari da loro e ognuno può rilevare malfunzionamenti non rivelabili con l’altro.


Testing Framework


Strumenti per testing basati su UML, C/C++


White Box Testing

Il White Box Testing è basato sulla nozione di copertura, i.e. sull’esecuzione di elementi del grafo di controllo di un programma.


Grafo di controllo di un programma

A ogni programma imperativo si può associare un grafo di controllo definito nel seguente modo:

  Un comando di assegnamento o di ingresso/uscita può essere rappresentato da un solo nodo nel grafo di controllo


  if cond then S1 else S2


  while cond do S:


  S1; S2


Esempio di grafo di un programma


Grafo di controllo di un programma sequenziale (contd)

  Il grafo corrispondente ad un programma può essere modificato a seconda dell'uso che se ne intende fare

  Possono essere sia eliminati che aggiunti nodi ed archi


Esempio: Se si e` interessati solo ai comandi che comportano più alternative nel flusso di controllo i nodi corrispondenti a sequenze di ingressi/uscite ed assegnamenti possono essere collassati:


Esempio: Rappresentazione delle diverse azioni che corrispondono all'assegnamento (R1,...,R4, registri):


Grado di copertura

Ad ogni test T basato sulla nozione di copertura è associabile una misura del grado di copertura dato da:

numero di elementi coperti da T numero totale di elementi copribili


Teorema (Weyuker): Dato un programma P, l’esistenza di un dato di test tale da causare l’esecuzione

  di una particolare istruzione di P, oppure   di una particolare condizione di P, oppure   di un particolare cammino di P, oppure   di ogni istruzione di P, oppure   di ogni condizione di P, oppure   di ogni cammino di P non è decidibile.


Criterio di copertura dei comandi (Statement test)

  Un test T soddisfa il criterio di copertura dei comandi se e solo se ogni comando eseguibile del programma è eseguito per almeno un dato di test in T.

  Nel grafo di controllo del programma, ogni nodo corrispondente ad un comando eseguibile deve essere percorso almeno una volta

  Misura di copertura C : numero di comandi eseguiti

numero totale di comandi eseguibili


  Esempio: Si consideri il seguente programma


  Il test S = {(x = 20, y = 30)}, causa l'esecuzione di tutti i comandi del programma: soddisfa il criterio di copertura dei comandi (la copertura assicurata da S è 100%)

  Il malfunzionamento (divisione per zero), che si verifica quando il comando alla linea 8 viene eseguito con valore zero per la variabile x non è rilevato dal test S

  Il test S non comporta l'esecuzione del programma per tutti i valori delle decisioni: la decisione alla linea 7 (x>0) dà valore vero per tutti i dati di test contenuti in S


Criterio di copertura delle decisioni (Branch test)

  Un test T soddisfa il criterio di copertura delle decisioni se e solo se ogni arco del grafo di controllo del programma è percorso almeno una volta

  Misura di copertura C : numero di archi percorsi

numero totale di archi percorribili   Ovviamente, se un test soddisfa il branch test

allora soddisfa anche il statement test, ma non è detto il viceversa.


  Il test S = {(x = 20, y = 30)} non soddisfa il criterio di copertura delle decisioni: l'arco (6, 8) non viene mai percorso

  Il test D = {(x = 20, y = 30), (x = 0, y = 30)} soddisfa il criterio di copertura delle decisioni, in quanto causa la percorrenza di tutti gli archi almeno una volta, e permette di rilevare il malfunzionamento causato dalla divisione per zero alla linea 8


  Esempio: Si consideri il seguente programma


  Il test {(x = 5, y = 5),(x = 5, y = -5)} soddisfa il criterio di copertura delle decisioni, ma non rileva un malfunzionamento causato da una divisione per zero sia alla linea 7 che alla linea 8

  La decisione alla linea 7 può essere posta a vero ed a falso agendo unicamente su una sola delle due condizioni in or nella decisione


Criterio di copertura delle condizioni (Condition testing)

  Un test T soddisfa il criterio di copertura delle condizioni se e solo se ogni singola sotto-condizione che compare nelle decisioni del programma assume il valore vero e falso per un qualche dato di test in T.


  Il test C = {(x = 0, y = -5), (x = 5, y = 5)} soddisfa il criterio di copertura delle condizioni, infatti:   per il dato (x = 0, y = -5) la condizione (x = 0) vale

vero e la condizione (y > 0) vale falso,   per il dato (x = 5, y = 5) la condizione (x = 0) vale

falso e la condizione (y > 0) vale vero   Il test C rileva il malfunzionamento causato

dall'anomalia alla linea 7, ma non quello causato dall'anomalia alla linea 8

  Il test C non soddisfa il criterio di copertura delle decisioni, infatti per entrambi i dati del test C la decisione di linea 7 vale vero


Criterio di copertura delle condizioni e delle decisioni

  Un test T soddisfa il criterio di copertura delle condizioni e delle decisioni se e solo se ogni decisione vale sia vero che falso ed ogni singola sotto-condizione che compare nelle decisioni del programma vale sia vero che falso per diversi dati di test in T

  Il criterio di copertura delle decisioni e delle condizioni contiene sia il criterio di copertura delle condizioni che il criterio di copertura delle decisioni


  Il test C = {(x = 5, y = -5), (x = 0, y = -5), (x = 5, y = 5)} soddisfa il criterio di copertura delle condizioni e delle decisioni

  Il test C rileva il malfunzionamento causato dall'anomalia alla linea 7, e anche quello causato dall'anomalia alla linea 8


Altri criteri di selezione

  Modified Condition/Decision Coverage (MC/DC)   Criterio di copertura dei cammini   Criterio di n-copertura dei cicli   Criteri di selezione DF


Criterio di copertura dei cammini (Path test)

  Un test T soddisfa il criterio di copertura dei cammini se e solo se ogni cammino nel programma viene percorso per almeno un dato di test in T

  Misura di copertura C : numero di cammini percorsi

numero totale di cammini percorribili   Il numero di cammini eseguibili può essere infinito,

rendendo tale criterio non applicabile   Per limitare il numero di cammini si fissa il numero

massimo di percorrenze di ciascun ciclo


Criterio di n-copertura dei cicli

  Un test T soddisfa il criterio di n-copertura dei cicli se e solo se ogni cammino contenente un numero di iterazioni di ogni ciclo non superiore ad n è eseguito per almeno un dato di test in T


Criteri di selezione Data Flow

  Determinano la significatività dei cammini in un programma a partire dall'analisi di flusso delle variabili

  Selezione di un cammino basata sul numero di sequenze definizione/uso delle variabili

  Un ciclo viene ripetuto un numero maggiore di volte solo se ciò permette di eseguire sequenze di definizione/uso non ancora esaminate


Esempio: gcd

  Variabili x ed y definite (linea 5) e usate (linee 6 e 7), sufficienti test selezionati da criteri di 0-copertura dei cammini

  Variabili a e b : definizione di a di linea 6 usata nelle linee 8, 10, 11, 12 e 14; definizione di a di linea 11 (nodo 11') usata in 8, 10, 11, 12; definizione di b di linea 7 usata nelle linee 8, 10, 11 e 12;

  definizione di b di linea 12 (nodo 12') usata nelle linee 8, 10, 11, 12.


Esempio: gcd

  Obiettivo: determinare il numero minimo di iterazioni richieste affinché tutte le sequenze definizione/uso per le variabili a e b siano esercitate almeno una volta

  Dati di test che non causano alcuna iterazione del ciclo while (es. (x = 5, y = 5)) non sono sufficienti


Esempio: gcd

  Dati di test che causano un'iterazione del ciclo while (es. (x = 10, y = 5)) permettono di esercitare tutti gli usi delle variabili a e b che possono seguire le definizioni alle linee 6 e 7 rispettivamente, ma non gli usi dei valori definiti dai comandi alle linee 11 (nodo 11') e 12 (nodo 12')


Esempio: gcd

  Dati di test che causano due iterazioni del ciclo while (es. (x =15, y = 5)) permettono invece di testare tutte le sequenze definizione/uso delle variabili a e b, e quindi permettono un'analisi completa per il criterio scelto


Esempio: gcd

  Dati di test che richiedono piu` di due di iterazioni dei ciclo while (es. (x =20, y = 5)) non sono necessari al fine di esercitare sequenze di definizione/uso non esaminabili con due sole iterazioni.


  Sia x una variabile del programma P.   Il cammino (i, n1, .., nm, j) nel grafo corrispondente al

programma P è un cammino libero da definizioni rispetto alla variabile x dal nodo i al nodo j se e solo se la variabile x non appartiene a nessuno degli insiemi def associati ai nodi i, n1, ..,nm, j

  Per ogni nodo i e ogni variabile x appartenente all'insieme def associato al nodo i, si definisce l'insieme du(x, i) come l'insieme di tutti i nodi j tali che esiste un cammino libero da definizioni rispetto alla variabile x dal nodo i al nodo j e x è usata nel nodo j


nodo def use du(x) du(y) du(a) du(b)

5 x,y 6 7

6 a x 8,10,11,12,14

7 b y 8,10,11,12

8 a,b

10 a,b

11 a,b

11’ a 8,10,11,12,14

12 a,b

12’ b 8,10,11,12

14 a


Criterio copertura delle definizioni   Un test T soddisfa il criterio di copertura delle definizioni

se e solo se per ogni nodo i ed ogni variabile x appartenente all'insieme def(i), T include un cammino libero-da-definizioni dal nodo i ad almeno un elemento di du(i, x)

  Esempio: Per il programma gcd il criterio seleziona test che causano al più un'iterazione del ciclo while

  Il criterio non richiede che per ogni definizione siano raggiunti tutti gli usi che possono fare riferimento alla stessa definizione

  Per la definizione di a corrispondente al nodo 11', il criterio è soddisfatto (uso di a al nodo 8)


Criterio di copertura di tutti gli usi

  Un test T soddisfa il criterio di copertura tutti gli usi se e solo se per ogni nodo i ed ogni variabile x appartenente all'insieme def(i), T include un cammino libero-da definizioni dal nodo i ad ogni elemento di du(i, x) .


Criterio copertura dei cammini du

  Un test T soddisfa il criterio di copertura dei cammini du se e solo se per ogni nodo i ed ogni variabile x appartenente all'insieme def(i), T include tutti i cammini non contenenti cicli e liberi-da-definizioni dal nodo i ad ogni elemento di du(i, x)


Black Box Testing

Basati sulle specifiche del programma. Tre principi utili:

  per ogni variabile di input che assume valori in un intervallo, testare almeno un valore al di sotto, uno al di sopra e uno nell’intervallo (per la robustezza).

  test di frontiera (boundary testing): testare i valori di frontiera di ogni variabile (usualmente rilevano più errori di altri).


Test di Integrazione Dato un programma composto da piu’ moduli, si

devono testare:   i singoli moduli, secondo le tecniche già illustrate

con eventuale creazione di moduli di simulazione.   le interazioni fra i moduli, secondo due tecniche:

  big bang test: tutti i moduli vengono integrati e il sistema viene testato come unità,

  incremental test: i moduli vengono integrati e testati via via che sono prodotti (necessita di stub/drivers).


Test di Sistema Il test di sistema è volto a testare particolari

proprietà globali del sistema, fra cui:   test di stress: proprietà del sistema in

condizioni di sovraccarico,   test di robustezza: proprietà del sistema se i

dati non sono corretti,   test di sicurezza: proprietà di sicurezza del

sistema.


Test di Regressione Il test di regressione considera il caso che si produca

una nuova versione di un programma.

Teorema: Non è possibile stabilire l’equivalenza di due programmi.

=>si verifica la compatibilità della nuova versione rispetto alla precedente attraverso (i) l’esecuzione dei due programmi sugli stessi dati (eventualmente convertiti) e (ii) il successivo confronto dei risultati.


Test di Accettazione (Alpha testing)   Fase finale del processo di testing. Il sistema

è testato su insieme di dati forniti dall’utente. In casi limite, potrebbe essere una versione “golden” del programma che si sa essere corretta (cfr regression testing). Svolto presso la sede del produttore.


Beta testing   Il sistema è fornito ad alcuni utenti potenziali

che accettano di usare e il sistema e di riportarne gli eventuali problemi.

  E’ possibile che il processo di Beta testing comporti la modifica del sistema e il rilascio di nuove versioni da sottoporre nuovamente al Beta testing.


Conclusioni sul Testing

  Il testing è il metodo più usato per determinare malfunzionamenti dei programmi

  Il test di un programma può rilevare la presenza di malfunzionamenti, ma mai dimostrarne l’assenza (tesi di Dijkstra)

  Un insieme di test fallisce quando non rileva errori


Metodi Formali


Metodi Formali Basati sulla specifica formale dei requisiti. La

specifica formale richiede un linguaggio con sintassi e semantica formalmente definiti.

=> le specifiche formali coinvolgono entità matematiche e pertanto possono essere analizzate (in modo automatico o manuale) con strumenti rigorosi.


Vantaggi dei metodi formali   Le specifiche in linguaggio naturale sono spesso

  inconsistenti,   ambigue,   difficili da seguire,

  Le specifiche formali   forzano a pensare più a fondo sul significato della

specifica scritta,   possono essere usate per provare la correttezza del

programma,   possono essere usate per generare dei dati di test.


Limiti dei metodi formali   scrivere una specifica formale è come scrivere un

programma:   è possibile introdurre errori,   non si è comunque sicuri di catturare il comportamento “inteso” del

programma,

  fare prove di correttezza è un processo lungo e difficile:   su carta, è facile introdurre errori,   su calcolatore, chi assicura che (il programma usato) sia corretto?

  il testing è fatto sul codice oggetto. La verifica di correttezza sul codice sorgente. Il compilatore è corretto?


Perchè i metodi formali non sono largamente diffusi

  non è chiaro che il costo relativamente alto dello sviluppo di specifiche formali riduca i costi totali di sviluppo,

  richiedono competenze relativamente complesse e incontrano resistenze da parte dei software engineers,

  è improbabile che gli utenti che commissionano il SW siano familiari con tali metodi e quindi difficilmente finanziano attività sulle quali non possono direttamente intervenire,

  alcuni sistemi non si prestano bene all’utilizzo di tali metodi.


Livello di utilizzo

Il documento “Requirements and Technical Concepts for Aviation (RTCA)” (DO-178B in USA, EUROCADE ED-12B in Europa) prevede tre livelli di applicazione:

  Livello 1 : specifiche formali del sistema, con eventuale uso di differenti formalismi e notazioni;

  Livello 2 : specifica formale del sistema in un linguaggio fissato. Verifica della correttezza del sistema su carta;

  Livello 3 : la correttezza della dimostrazione è verificata da un proof checker automatico.


Tipologia degli strumenti


Livello di supporto


Alcune Applicazioni

  SACEM, sistema di segnalazione ferroviaria (B method),   TCAS, sistema di controllo e “collision

avoidance” (nessun metodo specifico),   IBM’s CICS - sistema transazionale di controllo delle

informazioni (Z method),   Hardware (e.g. Microprocessore LSI Logic inc. FM9001

(NQTHM)),   Software (e.g. linguaggio C (CBMC)),   Protocolli di comunicazione (e.g. IEEE standard for

Futurebus+ (SMV)).


Metodi Formali Model Checking


Model checkers   Cosa sono: tools per l’analisi esaustiva dello

spazio degli stati di un sistema   Funzionalità:

  rappresentazione dello spazio degli stati del sistema (es. automa a stati finiti)

  descrizione delle proprietà da verificare (es. non esiste stato in cui ...)

  analisi dello spazio degli stati rispetto alle proprietà (“model checking”)


Caratteristiche:   Completamente basati su metodi formali (es. logica

temporale, teoria degli automi)   Focus sull’automazione (“push button technology”)   Analisi esaustiva dello spazio degli stati.   In caso la proprietà non sia verificata, forniscono un

controesempio.   Il sistema deve essere a stato finito e non parametrico

(es. 5 processori, non un numero qualunque n di processori)


Sistemi:   sviluppati in ambito accademico (NuSMV, UV, ...)   in-house (Siemens, Motorola, AT&T, Intel, ...)   commercializzati (CheckOff, FormalCheck, …)


Il problema principale:   complessità computazionale dovuta alla

esplosione del numero degli stati (100 variabili di stato → 10exp(30) stati) (“state explosion problem”):   Assumendo anche un solo bit per ogni stato,

10exp(30) bit = 10exp(20) Gbit   Assumendo che per esplorare uno stato ci voglia

1ns, 10exp(30)ns > 10exp(12) anni


Elementi caratterizzanti di ogni sistema:   tecnica di espansione degli stati,   linguaggio di specifica dell’automa,   metodo per caratterizzazione stati iniziali,   linguaggio di specifica delle proprietà da

verificare.


Tecniche di espansione degli stati

“On the fly” (e.g. SPIN):   Gli stati sono rappresentati tramite vettori (es. bit vectors se variabili Booleane)   funzione di transizione genera stati successivi che sono analizzati

immediatamente, prima di generare ulteriori stati.   Utilizzo di tecniche di compressione degli stati e di control flow analysis per

riduzione delle possibili esecuzioni   Può dare risultati anche se lo spazio esplode.

“Symbolic Moded Checking” - Off-line (e.g. NuSMV):   Sistema a stati generato a priori dell’analisi, con diverse tecniche:

  Basate su OBDD: Possibile esplosione in spazio, nel qual caso nessuna analisi possibile. Se non esplode in spazio, efficiente in tempo (lineare).

  Basate su SAT: Non esplode in spazio, ma analisi possibile solo per “bug finding”. Esistono estensioni anche per il problema della verifica.


Linguaggi di specifica proprietà

  Tipicamente logica temporale (e.g. CTL, LTL, µcalcolo)

  Proprieta’ sulla storia degli stati attraversati. Es:   “Non esiste uno stato raggiungibile in cui la

condizione COND è vera”   “Se la variabile COND1 assume il valore 1, allora

deve esistere uno stato in cui COND2 vale 0”.


Linguaggi di specifica dell’automa

  Diverse possibilità, in funzione delle caratteristiche dei sistemi da modellare. Es.:   VHDL, System C: hardware, sistemi sincroni   CSP, Promela: protocolli, sistemi asincroni   BPEL: web services   C, …


Automi a stati finiti

  Un automa a stati finiti è una una 5-tupla < ∑,S,I,t,F>:   ∑ è l’alfabeto di input   S è l’insieme degli stati   I⊆S e’ l’insieme degli stati iniziali   t: S x I → 2S è la funzione di transizione   F⊆S e’ l’insieme degli stati finali


Automi su parole finite

  Dato un automa A=< ∑,S,I,t,F>:   L’input di A e’ una stringa in ∑*, i.e., è una sequenza a =

a0, a1, … an, con ai∈ ∑   Una esecuzione dell’input s è una sequenza di stati

s0,s1,s2, … sn, tale che   s0 ∈ I   si+1 ∈ t(si,ai)

  Una esecuzione s0,s1,s2, … sn è accettata se sn ∈ F   Il linguaggio riconosciuto da A è l’insieme degli input di A

per cui esiste una esecuzione accettata da A


Automi su parole infinite (ω-automi)

  Dato un automa A=< ∑,S,I,t,F>:   L’input di A e’ una stringa infinita in ∑ω, i.e., è una

sequenza a = a0, a1, a2 … con ai∈ ∑   Una esecuzione dell’input s è una sequenza infinita di

stati E=s0,s1,s2, … , tale che   s0 ∈ I   si+1 ∈ t(si,ai)

  Sia E=s0,s1,s2, … , una esecuzione, ed Inf(E) = {s : s = si per un numero infinito di i}. E è accettata se Inf(E)∩F≠{}.

  Il linguaggio riconosciuto da A è l’insieme degli input di A per cui esiste una esecuzione accettata da A


Rappresentazione simbolica del sistema (Symbolic model checking)

  Indipendentemente dal linguaggio di alto livello utilizzato per modellare il sistema, al sistema corrisponde un automa a stati finiti, di cui si vuole caratterizzare la relazione di transizione.

  La relazione di transizione coinvolge lo stato corrente del sistema e lo stato futuro del sistema stesso.

IDEA :   il sistema sia descritto da n variabili Booleane di stato v1,v2,...,vn   v=(v1,…, vn) sia il vettore di variabili di stato che rappresenta lo stato

corrente e v’=(v1’ ,…,vn’) rappresenti lo stato futuro   la relazione di transizione del sistema concorrente può essere

rappresentata come una formula booleana R(v,v’)


Esempio #include

void frullatore () { bool a; /* non si sa se il tasto e‘ premuto */ bool c; /* il motore e‘ disattivato */ do cin >> a; /* il tasto e‘ premuto? */ while (a) /* se il tasto e‘ premuto */ {c = 1; /* attiva il motore */ cin >> a;} /* il tasto e‘ premuto? */ c = 0; /* il motore viene disattivato */ while (1); /* ripetere all’infinito */ }


Etichettazione #include void frullatore ()

{ 0 bool a; /* non si sa se il tasto e‘ premuto */ bool c = 0; /* il motore e‘ disattivato */ do 1 cin >> a; /* il tasto e‘ premuto? */ 2 while (a) /* se il tasto e‘ premuto */ 3 {c = 1; /* attiva il motore */ 4 cin >> a;} /* il tasto e‘ premuto? */ 5 c = 0; /* il motore viene disattivato */ 6 while (1); /* ripetere all’infinito */ 7 }


Funzione di transizione

(pc=0) ^ (pc’=1) ^ (c’=0) v (pc=1) ^ (pc’=2) ^ (c’=c) v (pc=2) ^ (a ^ (pc’ =3) v ¬a ^ (pc’=5)) ^(c’=c)^(a’=a) v (pc=3) ^ (pc’ = 4) ^ (c’ = 1) ^ (a’ = a) v (pc=4) ^ (pc’ = 2) ^ (c’ = c) v (pc=5) ^ (pc’ = 6) ^ (c’ = 0) ^ (a’ = a) v (pc=6) ^ (T ^ (pc’=1) v ¬T ^ (pc’=7)) ^ (a’=a) ^ (c’=c) v (pc=7) ^ (pc’=7) ^ (a’=a) ^ (c’=c)


Etichettazione 2 #include void frullatore ()

{ 0 bool a; /* non si sa se il tasto e‘ premuto */ bool c = 0; /* il motore e‘ disattivato */ do 1 cin >> a; /* il tasto e‘ premuto? */ 2 while (a) /* se il tasto e‘ premuto */ 3 {c = 1; /* attiva il motore */ cin >> a;} /* il tasto e‘ premuto? */ 4 c = 0; /* il motore viene disattivato */ 5 while (1); /* ripetere all’infinito */ 6 }


Funzione di transizione 2

(pc=0) ^ (pc’=1) ^ (c’=0) v (pc=1) ^ (pc’=2) ^ (c’=c) v (pc=2) ^ (a ^ (pc’ =3) v ¬a ^ (pc’=5)) ^(c’=c)^(a’=a) v (pc=3) ^ (pc’ = 2) ^ (c’ = c) v (pc=4) ^ (pc’ = 6) ^ (c’ = 0) ^ (a’ = a) v (pc=5) ^ (T ^ (pc’=1) v ¬T ^ (pc’=7)) ^ (a’=a) ^ (c’=c) v (pc=6) ^ (pc’=7) ^ (a’=a) ^ (c’=c)


Codifiche simboliche: Esempio

00 01

10 11

000 001 010 011

100 101 110 111

Counter N bit ⇒ 2N nodi TN ⇒ O(N) simboli


Rappresentazione (estensionale) del sistema come struttura di Kripke

  Estensionalmente, il modo più intuitivo per rappresentare le possibili evoluzioni del sistema è tramite un albero infinito, in cui   I nodi rappresentano i possibili stati assunti dal sistema,   Gli archi le transizioni da uno stato ad un altro,   Gli stati iniziali corrispondono alle radici dell’albero.

  Formalmente, tale rappresentazione è una Struttura di Kripke.   Il problema della verifica di una proprietà di un sistema

corrisponde quindi al problema di stabilirne la verità sulla struttura di Kripke corrispondente al sistema.


Strutture di Kripke   Una Struttura di Kripke M è una tripla , in

cui:   S, è un insieme, che rappresenta gli stati,   R, è una relazione binaria su S, che rappresenta le

possibili transizioni da stato a stato   L, è una funzione che associa a ogni stato in S, una

funzione di interpretazione del linguaggio.

  Le strutture di Kripke modellano accuratamente il sistema, ma manca la caratterizzazione degli stati iniziali e delle proprietà.


Altre rappresentazioni e loro relazione

  Le rappresentazioni simboliche e quelle nel formalismo iniziale (es. C) sono rappresentazioni (esponenzialmente più) compatte dell’automa, le cui evoluzioni corrispondono a una struttura di Kripke

  Altre rappresentazioni sono possibili. Es: grafo I cui nodi sono gli stati del sistema e gli archi rappresentano le transizioni. Tale rappresentazione a grafo è comunque estensionale, e non è quindi necessariamente “compatta”.

  Le rappresentazioni compatte sono quelle difatto utilizzate dai sistemi di verifica automatica


Rappresentazione degli stati iniziali

  Gli stati iniziali sono rappresentabili tramite una formula Init nel linguaggio del sistema.

  Nel caso il linguaggio sia proposizionale, uno stato corrisponde a una interpretazione, e gli stati iniziali sono quelli che soddisfano Init


Linguaggio di specifica proprietà   Stesso linguaggio di specifica del sistema (e.g.

MURphi):   Proprieta’ sui singoli stati, confronto 2 stati, ... (Es:

non esiste stato in cui x = 1, in ogni coppia di stati x y…)

  Linguaggio di specifica più espressivo (e.g. SMV):   tipicamente logica temporale (e.g. CTL, LTL), µcalcolo;   proprieta’ sulla storia degli stati attraversati   Es: “se la variabile COND1 assume il valore 1, allora non

esisterà mai uno stato in cui COND2 vale 0”).


Linear Temporal Logic: Sintassi

  Sintassi LTL:   Ogni proposizione atomica p è una formula LTL.   Se f e g sono formule LTL, ¬f, f ^ g, Xf, fUg sono

formule LTL.

  Abbreviazioni (oltre alle standard proposizionali):   Fg = trueUg = ¬G¬g   Gf = ¬[trueU¬f] = ¬F¬f


Linear Temporal Logic: Semantica Si considerano strutture di Kripke. Ci si limita a percorsi infiniti,

corrispondenti ad automi con funzione di transizione totale. Intuitivamente:   In uno stato s la formula Xf è vera se f è vera nello stato

successivo nel percorso considerato.   In uno stato s la formula fUg è vera se esiste uno stato

futuro in cui g è vera, e in tutti i stati precedenti f è vera.   In uno stato s la formula Ff è vera se esiste uno stato nel

futuro in cui f è vera.   In uno stato s la formula Gf è vera se per tutti gli stati nel

futuro f è vera.


LTL: specifica di proprietà

Esempi:   “Non esiste uno stato raggiungibile in cui la condizione

COND è vera”: G¬COND   “Se la variabile COND1 assume il valore 1, allora deve

esistere uno stato in cui COND2 vale 0”: G(COND1⇒F¬COND2)

  “A ogni messaggio spedito deve corrispondere una risposta”: G(Sent ⇒ F Ack)

  “Ogni messaggio spedito deve ricevere Ack in 3 unità di tempo”: G(Sent ⇒ (XAck ∨ XXAck ∨ XXXAck))


Safety Properties   Le più usate in ambito industriale   Rappresentano invarianti del sistema   Il problema della verifica di una safety property f

corrisponde al seguente problema di raggiungibilità: “Esiste una sequenza di stati che porta da uno stato iniziale a uno stato in cui è falso f?”. In LTL corrisponde a verificare se “F not f” e’ vero nel modello.

  Un problema di (symbolic) reachability nelle variabili x corrisponde a una tripla

  Problema PSPAZIO completo (rimane in PSPAZIO se F(x) e’

una generica formula LTL).


Symbolic Model checking of safety properties, or Symbolic reachability

Due possibilità:   Unbounded Symbolic model checking (OBDD)   Bounded Symbolic model checking (SAT)


Unbounded Symbolic Reachability

Data una funzione di transizione T(x,x’), assumiamo di poter computare efficentemente le funzioni

FWD(x) = ∃y (S(y) ∧ T(y,x)) BWD(x) = ∃y (S(y) ∧ T(x,y))


Unbounded Symb. Reachability Basato su Ordered Binary Decision Diagrams (OBDDs), usati

per rappresentare   La funzione di transizione T(x,x’) del sistema   Gli stati Ri(x) raggiungibili in i-passi a partire dagli stati iniziali o finali

OBDDs   La computazione di FWD(x) e BWD(x) è efficente (polinomiale nella

dimensione delle formule in input)   Ma la dimensione di T(x,x’) e Ri(x) può essere esponenziale nel

numero di variabili   Il limite “pratico” corrente è 500 variabili di stato   Possibilità di tornare un controesempio nel caso di “bug”


Initial States Buggy States

Simulation Trace Verified fully for k=3

Falsified at k=4


Unb. Forward Reachability: Algo S0(x) = R0(x) = I(x) i=0 1: if SAT(Si(x) ∧ F(x)) then else (Si+1(x) = ∃x’(Si(x’) ∧ T(x’,x))) Ri+1(x) = Ri(x) ∨ Si+1(x) if SAT(Ri+1(x) ∧ ¬ Ri(x)) then i=i+1; goto 1 else exit: .


Initial States Buggy States

Simulation Trace Verified fully for k=3

Falsified at k=4


Unb. Backward Reachability: Algo S0(x) = R0(x) = F(x) i=0 1: if SAT(Si(x) ∧ I(x)) then else (Si+1(x) = ∃x’(Si(x’) ∧ T(x,x’))) Ri+1(x) = Ri(x) ∨ Si+1(x) if SAT(Ri+1(x) ∧ ¬ Ri(x)) then i=i+1; goto 1 else exit: .


Bounded Symbolic Reachability

  I path lunghi k (>=0) corrispondono agli assegnamenti che soddisfano la formula

R(x0,…,xk) = T(x0,x1) ∧ T(x1,x2) ∧ … ∧ T(xk-1,xk)   Esiste un percorso lungo k da uno stato iniziale a

uno stato finale se e solo se la formula I(x0) ∧ R(x0,…,xk) ∧ F(xk)

è soddisfacibile


B. Symbolic Reachability: Algo

k=0 1: if SAT(I(x0) ∧ R(x0,…,xk) ∧ F(xk)) then else k=k+1 if () then else goto 1.


B. symbolic reachability: Esempio

00 01

10 11

Modulo 4 counter (bugged)

10

00

Initial state s10, final state s00

R(x1,x2,x3) = 0 for all values of x1,x2,x3 ⇒ s00 is unreachable from s10


Bounded Symb. Reachability Basato su algoritmi per ragionamento proposizionale (SAT-

solvers), usati per determinare   La soddisfacibilità di I(x0) ∧ R(x0,…,xk) ∧ F(xk)   (Eventualmente) la verità della condizione di terminazione

SAT-solvers   Determinare la sodd. di I(x0) ∧ R(x0,…,xk) ∧ F(xk) è un problema

NP-completo   La dimensione di I(x0) ∧ R(x0,…,xk) ∧ F(xk) cresce linearmente con

k, ma k può essere esponenziale nel numero di variabili   Esistono SAT-solvers altamente efficenti (cfr. SAT competition)   Possibilità di tornare un controesempio nel caso di “bug”


Il problema della raggiungibilità da un punto di vista computazionale

  Due risorse: TIME (omesso) e SPACE   P = polinomiale, EXP = esponenziale   N = non-deterministico   co = complemento

NP co-NP P PSPACE EXP

Bounded symbolic reachability and SAT Symbolic reachability and Q-SAT

Reachability


Metodi Formali Model Checking

Research @ STAR Lab


QBF4MC: Overview

  Formal methods in industry   Circuit descriptions (logic and control)   Requirements (properties to be verified)

  Model Checking (MC) of hardware   Model M, property P: M satisfies P?

  Established methodologies   Unbounded Symbolic MC (OBDDs)   Bounded Symbolic MC (SAT)


QBF4MC: Problem statement

  OBDDs suffer capacity problems   Current limit is O(2N) sized SAT encoding


QBF4MC: Goals

  Develop an alternative based on QBF   Same expressive power as OBDDs   Space is not critical as in SAT

  Make it competitive w.r.t. OBDDs and SAT   Deploy QBF-based encodings on the field

  Debugging: an encoding of bound k is compressed by folding it down to o(log2k) length

  Full verification: the space induced by N variables can be fully explored using O(N) QBF encodings OK!


QBF4MC: Issues   Relative youngness of QBF techniques   Complexity of QBF reasoning

  QBF reasoning is PSPACE-hard   Folding introduces universal variables

  Need for general purpose techniques   Search strategies, simplification, backtracking, ...

  Need for domain specific techniques   Domain knowledge, structural information, circuit-based

reasoning, ...


QBF4MC: Status   Some general purpose techniques established

  Backjumping (IJCAI’01)   Learning (AAAI’02)   Efficient implementations (SAT’03, SAT’04)

  Assessment on available QBF instances   Ayari/Basin: property verification   Scholl/Becker: implementation refinement   Mneimneh/Sakallah: vertex eccentricity

  QBF comparative evaluation   QBFLib


Estensione dei diagrammi di flusso: schemi di trasformazione

  Estensione dei diagr. di flusso per rappresentare aspetti temporali e di sincronizzazione

trasformazioni di dati

trasformazionei di controllo

flusso di dati

discreti

flussi di controllo

segnale

continui

attivazione

disattivazione

(linee tratteggiate)


Modelli Entità-Relazioni

  Usati per descrivere la struttura logica dei dati processati dal sistema

  Rappresentano esplicitamente le entità del sistema, gli attributi di ogni entità, e le relazioni tra entità

  Usati molto nella progettazione di database. Possono essere facilmente implementati usando database relazionali


Notazione per i modelli ER

< nome > una entità

< nome >

< input card. >

< output card. >

una relazione tra entià. La cardinalità di input è il numero di istanze di entità in input. La cardinalità di output è il numero di istanze di entità in output

< nome > un attributo di entità o di relazione

una relazione di ereditarietà. Un’entità eredita gli attributi delle entità in relazione con essa. La freccia indica “ è sottotipo”


Modelli entità-relazioni

Dirigenti a capo di Dipartimenti

partecipa

Progetti

Assegnato

Impiegati

cognome nome

stipendio

data durata

1 n

1

n 1

n

Personale


Esempio (ER per requisito sw)


Modelli ad oggetti

  Il sistema è descritto in termini di classi di oggetti   Una classe astrae una serie di oggetti con attributi e

servizi (operazioni) comuni.   I modelli ad oggetti possono essere di diverso tipo:

  Modello di ereditarietà (statico)   Modello di aggregazione (statico)   Modello dei servizi (dinamico)


Incapsulamento

  I dati e le operazioni che operano su questi dati sono impacchettati in una stessa classe

  I dettagli sull’implementazione di un servizio sono nascosti all’utente del servizio

  Previene l’accesso non autorizzato ai dati di un oggetto.


Modelli ad oggetti


Ereditarietà

  Organizza le classi gerarchicamente   Le classi in alto riflettono caratteristiche comuni a

tutte le classi sottostanti   Le classi ereditano attributi e servizi da una o più

superclassi.   Le classi possono essere specializzate


Gerarchia della classe biblioteca

Catalogue numberAcquisition dateCostTypeStatusNumber of copies

Library item

Acquire ()Catalogue ()Dispose ()Issue ()Return ()

AuthorEditionPublication dateISBN

Book

YearIssue

Magazine

DirectorDate of releaseDistributor

Film

VersionPlatform

Computerprogram

TitlePublisher

Published item

TitleMedium

Recorded item


Gerarchia della classe utente

NameAddressPhoneRegistration #

Library user

Register ()De-register ()

Affiliation

Reader

Items on loanMax. loans

Borrower

DepartmentDepartment phone

Staff

Major subjectHome address

Student

Tecniche di Specifica dei Requisiti

Linguaggi Formali di Specifica

Tecniche di Specifica dei Requisiti

Altre Tecniche


Linguaggi di Descrizione di Programmi (PDL)

Basati su linguaggi di programmazione esistenti (come JAVA, ADA…), eventualmente arricchiti con costrutti ulteriori di alto livello.   Es.: Concurrent Sequential Pascal

Convalida e Verifica - unige.itenrico/IngegneriaDelSoftware... · 2010. 9. 9. · Convalida e...

Documents

Transcript of Convalida e Verifica - unige.itenrico/IngegneriaDelSoftware... · 2010. 9. 9. · Convalida e...