Ingegneria del software: 5 maggio 2005

VERIFICA E CONVALIDA
Convalida
Confronto del software con le idee del committente
Verifica
Confronto del software con le specifiche formali. Le specifiche formali non sono (devono essere) ambigue.
(Verifica della corretteza del programma)
Sono punti di vista "volubili": é impossibile controllare tutto il software e l'utente ha sempre le idee poco chiare...
Quindi questo confronti vanno fatti durante tutto il ciclo di vita del software (non solo dopo la produzione)

I possibili problemi:
Malfunzionamento o guasto (failure)
Il programma da un risultato sbagliato (é un effetto esterno percepito dall'utente)
Es. Arian 5 (ESA 1996) viene lanciato e dopo 40 secondi esplode (percezione dell'utente)

Difetto o anomalia (fault)
E' legato al codice (non percepito dall'utente). Può originare un malfunzionamento
Può non manifestarmi come malfunzionamento se: (doppia anomalia: una elimina l'altra, si presenta su un input che non viene mai fornito)
Es. Il software di guida del satellite convertiva la velocità orizzontale da un double ad uno short e il programma é andato in overflow

Errore (error)
E' la causa di un anomalia
In genere si tratta di un errore umano (battitura, piuttosto che concettuale, padronanza del linguaggio, ecc.), ma può anche essere un bug nel compilatore
Es. Una parte di software era erditato dal lancio di Arian 4 in cui non succedeva mai che la velocità orizzontale soperasse i 16 bit signed (anzi c'era già un bel magine)

Considerazioni:
Non si era testato con la VERA traiettoria che il satellite doveva eseguire (tali dati non erano nemmeno stati forniti come specifiche)
Il meccanismo di protezione dalle eccezioni era focalizzato su errori HW e non SW

Tecniche di analisi del sw
Tecniche statiche (applicati al codice)
Metodi formali di correttezza
Analisi dataflow (analisi complessa dei dati e vedere come si incastrano tra loro)
Modelli statistici

Tecniche dinamiche (basate sull'esecuzione del programma)
Testing
Debugging

Principi
Sensitività: E' meglio fallire sempre che solo qualche volta (un bug che si manifesta solo in particolari condizioni é difficile da trovare)
Ridondanza: Rendere le intenzioni esplicite (usare più tecniche di convalida e verifica)
Partizionamento: Divide et impera (isolare il punto che da problemi)
Restrizione: semplificare il problema (es: usare un linguaggio fortemente tipizzato, evitare i puntatori, dichiarazione esplicita delle variabili, ecc.)
Feedback: regolazione del processo produttivo (non ripetere gli stessi errori)

Come evitare gli errori:
Prove formali: ricerca di anomalie (es. controllo delle specifiche formali)
Testing: rilevare malfunzionamenti. Tecnica ottimistica: faccio tante prove...
Debugging: Conoscendo un problema cerco l'anomalia che lo genera

DEF: Correttezza di un programma
P(d) indica l'esecuzione del programma su input d
Il programma é corretto solo se é corretto l'output di P(d) per ogni d che appartiene al dominio

Un test (T) é un sottoinsieme del dominio (D). Un elemento del test t é detto caso di test
Esecuzione del test: esecuzione del programma per tutti i t € T
Il programma passa (o supera) il test se il risultato per ogni t é corretto! Il test ha successo se viene rilevato un nuovo problema.

Criterio di selezione dei dati per il test:
Affidabilità: il criterio di scelta dei test é affidabile se per ogni t in T il passaggio del test implica che passerà per tutti gli altri t. Ovvero un elemento del test "controlla" l'altro: saputo il risultato per t so già quale deve essere il risultato per t1.
Validità: Qualora il programma non sia corretto esiste un test che ha successo (non passa)

Se un test é affidabile e valido e il test viene passato ciò implica che il programma sia corretto

Quando trovo un bug e lo correggo non posso garantire che il programma sia corretto... Oltre al fatto che potrebbero esserci altri errori, il cambiamento che ho effettuato ha alterato il programma così come era stato testato...

Selezione dei test: Approccio White Box
White Box prevede che ho accesso al codice sorgente e ne posso indagare la struttura
In genere gli errori si annidano nel codice che viene eseguito poco (negli angoli, come la polvere!). Per questo sono nati i costrutti di gestione delle eccezioni!

Un caso di test si può considerare efficace quando:
- Esegue il comando che contiene l'errore
- L'esecuzione del comando che contiene l'errore deve portare ad uno stato scorretto
- L'output scorretto deve propagarsi fino all'uscita del codice in esame in modo da essere visibile

Il nostro test deve quindi coprire tutte le righe del programma