|
costruzioni termomeccaniche
il sacro fuoco dell’innovazione
Tecniche di Verifica
I Metodi Formali
Tecniche di Verifica
I Metodi Formali
Nel processo di sviluppo dei prodotti diminuiscono gli errori e cresce l’affidabilità
 Antonella Santone
RCOST - Research Centre on Software Technology - Università degli Studi del Sannio
santone@unisannio.it
La verifica di correttezza del software è un problema affrontato sin dagli albori dell'informatica. Qualunque programmatore ha senz'altro sperimentato la frustrazione di molti fallimenti, prima di riuscire a scrivere un programma che funzioni. Si inizia, di solito, con un errore di sintassi (ad esempio la mancanza di un punto e virgola o di una parentesi graffa) segnalato dal compilatore. Quando finalmente si riesce a eliminare ogni errore sintattico, ecco che sopraggiunge un altro tipo di frustrazione: mentre si esegue il programma per la prima volta, l'esecuzione si arresta improvvisamente e il calcolatore comunica un messaggio di errore (questo nuovo tipo è conosciuto come errore a tempo di esecuzione). Dopo molte correzioni, il programma può finalmente essere eseguito senza errori e restituire un risultato. Ma chi ci garantisce che il risultato è quello corretto? La soluzione fornita dal programma è davvero quella al problema che si sta cercando di risolvere? Per rispondere affermativamente a queste domande, tradizionalmente si è utilizzata una tecnica nota come testing, che consiste nell'eseguire un programma ripetutamente su campioni diversi di dati. Per comprendere meglio questa tecnica pensiamo a quello che succede quando, ad esempio, si collaudano ponti, dighe, case, automobili o un qualsiasi altro manufatto. Tipicamente, essi sono provati in diverse condizioni di funzionamento e, se la prova ha esito positivo, ne viene autorizzato l'uso normale. Possiamo pertanto vedere la tecnica del testing come il collaudo del software. Più precisamente i metodi di verifica basati sul testing provano il comportamento corretto del sistema solamente su un sottoinsieme delle possibili computazioni. Un errore del sistema potrebbe quindi annidarsi proprio in uno dei comportamenti che non è stato verificato. Questo tipo di tecnica, pertanto, può dimostrare solo la presenza e non l'assenza di errori nel software. A sostegno di questa tesi viene fatto osservare che in prodotti dell'ingegneria tradizionale è relativamente facile estrapolare il comportamento di un sistema sulla base di un certo numero di esperimenti grazie alla fondamentale proprietà di continuità dei sistemi stessi: se si carica un ponte con 100 tonnellate, non sussistono dubbi sulla sua capacità di sostenere un peso di 99 tonnellate. Nel caso del software, che è tipicamente un prodotto non continuo, può darsi che un programma che produce un risultato corretto in corrispondenza di un valore di ingresso 100, cagioni effetti disastrosi se il dato di ingresso è 99. Esistono, però, sistemi critici nei quali un errore è inaccettabile. Si pensi a un sistema di controllo del traffico aereo o ferroviario, sistemi militari, o a un'applicazione in campo biomedico. Inoltre, esistono sistemi in cui un errore comporterebbe perdite economiche ingenti, si consideri, per esempio, il commercio elettronico o i sistemi bancari. Pertanto i metodi tradizionali basati sul testing risultano inadatti. In quest'ultimo ventennio si è assistito a un'evoluzione significativa dello sviluppo di teorie che mirano a superare i limiti del testing attraverso l'uso di metodologie formali. Le tecniche di verifica formale sono sicuramente molto affidabili in quanto eseguono verifiche di tipo matematico. Più precisamente queste tecniche permettono l'esplorazione esaustiva di tutti i possibili comportamenti di un sistema.
Sia "S" un sistema (un programma, un protocollo di comunicazione, un sistema concorrente, eccetera), di cui si vuole verificarne la correttezza. Per poter utilizzare una tecnica basata sui metodi formali occorre:
- descrivere "S" mediante un rigoroso linguaggio matematico che eviti tutte le ambiguità che possono presentarsi usando invece una descrizione informale, basata ad esempio sulla lingua italiana;
- formalizzare la proprietà che il sistema deve soddisfare. Anche per esprimere la proprietà si ricorre all'utilizzo di un linguaggio formale, che può essere o meno lo stesso linguaggio matematico usato per descrivere il sistema.
A questo punto sia il sistema sia la proprietà richiesta, entrambi descritti formalmente, vengono elaborati da opportuni strumenti che restituiscono due possibili risposte: vero se il sistema soddisfa la proprietà, falso in caso contrario. La verifica formale, pertanto, garantisce che un sistema è corretto, invece il testing può semplicemente mostrare che il sistema non è corretto. Queste tecniche formali possiedono importanti vantaggi: sono completamente automatiche e, in caso di fallimento della verifica, forniscono un contro-esempio, cioè danno il comportamento del sistema che ha generato l'errore. Il contro-esempio è molto utile perché può essere usato per localizzare e correggere l'errore. Aspetti così vantaggiosi possono, dunque, permettere alla verifica formale di rimpiazzare il ruolo che il testing ha avuto per così tanti anni nel mondo dell'industria. Come esempio di applicazione dei metodi formali, riportiamo il caso dell'incidente di lancio di Ariane 5 dell'European Space Agency nel giugno 1996, 500 milioni di dollari andati in fumo in pochi secondi. L'esplosione era dovuta al riuso di una routine; con i metodi formali l'errore sarebbe stato riconosciuto e forse non sarebbe addirittura stato introdotto. Sfortunatamente la verifica formale ha anche diversi svantaggi che ne limitano, a volte, l'applicazione a sistemi della vita reale. Uno dei maggiori è noto come l'esplosione degli stati: nel descrivere formalmente il sistema da verificare, dovendo considerare tutte le possibili computazioni, si ottengono spesso rappresentazioni di dimensioni tanto grandi da rendere difficile, se non addirittura impossibile, l'utilizzo di tecniche basate sui metodi formali. Di recente sono stati sviluppati diversi approcci che permettono di combattere l'esplosione degli stati e alcuni ricercatori di RCOST stanno lavorando in questa direzione ottenendo buoni risultati. Un altro problema che impedisce l'uso di metodi formali in un contesto industriale è la necessità di avere ingegneri del software con una notevole esperienza nel campo dei metodi formali. Tale esperienza è di rado presente in ingegneri del software che lavorano nel mondo dell'industria. Recentemente la ricerca sui metodi formali ha posto un'enfasi maggiore sullo sviluppo di strumenti user-friendly. Tecniche sofisticate basate su metodi formali sono state inglobate all'interno di strumenti automatici dotati di interfacce grafiche ad alto livello. L'utente progetta o verifica il sistema usando il linguaggio visuale del quale ha maggiore familiarità senza essere consapevole che il progetto del sistema e la specifica delle proprietà sono tradotte automaticamente in una notazione formale ed elaborati internamente da procedura di verifica formale. Tutti questi progressi fanno ben sperare che tecniche basate sui metodi formali possano essere utilizzate in ambito industriale. Inoltre, il recente sviluppo di standard internazionali e il fatto che queste tecniche stiano cominciando ad essere adottate da governi e organizzazioni, come requisito fondamentale, ha spinto le industrie produttrici di software e hardware a integrare i metodi formali nel processo di sviluppo dei prodotti per ottenere una sempre più alta qualità e affidabilità.
|
