Un software a prova di errore

    Il Premio Turing, il più prestigioso riconoscimento scientifico nell’ambito della computer science, è stato assegnato ad Amir Pnueli, matematico israeliano dell’Istituto Weizmann. Pnueli ritirerà il premio in California soltanto nel marzo 1997, ma è già noto ciò che ha spinto la Association for Computing Machinery a insignirlo del riconoscimento. Lo studioso ha sviluppato un metodo, apparentemente infallibile, per costruire programmi a prova di errore. Come fa? Semplice, almeno a dirsi: Pnueli traduce nel linguaggio della logica temporale, una particolare branca della logica matematica, i compiti che vengono richiesti al programma. Poi applica alcuni teoremi in grado, a sua detta, di rivelare se un software con quelle caratteristiche si comporterà come si deve in tutte le occasioni. E’ facile intuire la portata della sua invenzione: in un’epoca in cui sistemi computerizzati sempre più complessi controllano dalle telecomunicazioni agli apparati medici, dai sistemi di guida di aerei e missili alle centrali nucleari, gli errori nel software possono causare disastri tanto in termini economici che di vite umane.Incuriositi dall’uomo che sembra saper rendere infallibili i computer, abbiamo raggiunto Amir Pnueli e lo abbiamo intervistato.

    Professor Pnueli, è stato detto che il suo metodo è in grado di verificare l’affidabilità e la correttezza di un programma “prima ancora che esso venga scritto”. Come è possibile?

    Nei progetti in cui sono coinvolti grossi programmi e molte componenti, lo sviluppo del sistema computerizzato procede per diversi stadi. In una prima fase occorre scrivere semplicemente quali sono le caratteristiche che il sistema deve soddisfare. Successivamente si costruisce una specifica del sistema, un oggetto formale con un significato ben definito che fa da prototipo per il programma. Nel terzo stadio si lavora alla progettazione dettagliata del software, e solo in ultimo si passa alla scrittura del codice, ovvero la programmazione in senso stretto. Il metodo al quale io lavoro, chiamato della “verifica formale”, permette di stabilire la correttezza degli oggetti su cui si lavora a tutti gli stadi della progettazione.

    Si tratta cioè di rivelare gli errori durante la progettazione di un sistema?

    Esatto. Il nome del gioco è “rivelazione precoce” degli errori. Quanto prima questi vengono trovati, tanto meno costoso sarà eliminarli. E’ un fatto tristemente noto che l’eliminazione di un errore tipico, se esso viene scoperto in una fase molto precoce della progettazione, costa una cifra dell’ordine dei 50 dollari. Lo stesso errore, se non rivelato, in una fase successiva si paga ben più caro: fino a diverse decine di migliaia di dollari. E se l’errore si propaga sino al prodotto finale può causare a una compagnia danni fin quasi a cinquecento milioni di dollari, per non parlare degli incidenti che possono causare la perdita di vite umane.

    Ma come si possono costruire programmi a prova di errore?

    Il metodo attualmente utilizzato per il controllo dei sistemi è quello di fare dei test. Si tratta di fornire diversi dati di ingresso al sistema, dopo che esso è stato costruito, ed esaminare se le risposte sono quelle che ci aspettiamo. Il problema insito in tale metodo è che, tranne nei casi banali, i dati di ingresso, ovvero le situazioni possibili in cui si può trovare il programma, sono praticamente infinite: non si può verificarle tutte. Si può solo sperare di avere una “copertura rappresentativa”, ma è sempre possibile aver tralasciato un test critico, aver ignorato un errore, magari quello che farà cadere l’aeroplano su cui volate!

    E il suo metodo della verifica formale, professor Pnueli, riesce ad aggirare il problema? Può prevedere, per ogni programma, le infinite situazioni a rischio?

    In un certo senso, sì. Il mio metodo consiste nell’applicare teoremi matematici per stabilire se un sistema si comporta correttamente in tutte le situazioni possibili. A essere onesti, c’è da dire che noi analizziamo soltanto la logica matematica del programma stesso. Anziché verificare a posteriori le risposte di un programma, se ne analizza la logica prima che esso sia stato materialmente scritto. Credo che tale metodo di verifica formale sia sostanzialmente migliore dei test sui programmi e un giorno li sostituirà interamente. Tuttavia è chiaro che se un software lavora su un computer difettoso, o se comanda le operazioni di un macchinario guasto, può sbagliare anche se era stato dichiarato a prova di errore.

    LASCIA UN COMMENTO

    Please enter your comment!
    Please enter your name here