Galileo Giornale di scienza e problemi globali

22 Maggio 2012 | ultimo aggiornamento circa 6 ore fa
Temi tecnologia

Un software a prova di errore

0
di Yurij Castelfranchi | Pubblicato il 23 Novembre 1996 00:00

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.

tags: hi tech

Leggi anche

Commenti lascia un commento

Nessun commento, per ora.

Lascia un commento

Oggi su Galileo

Sondaggio

Mentre la Fisica è alle prese con la caccia al Bosone di Higgs, la rivista Nature si chiede quale scoperta nel campo della Biologia potrebbe essere pari a quella della mitica Particella di Dio. Secondo voi, quale di queste scoperte sarebbe paragonabile, per importanza a quella della particella mancante del Modello Standard?

risultati

Segui Galileo su

Galileo Servizi Editoriali

Parole per la scienza

Galileo servizi editoriali è un service giornalistico che realizza inchieste per le principali testate italiane, sviluppa progetti di comunicazione per le aziende e gli enti di ricerca, produce formazione universitaria, organizza mostre, eventi, conferenze, realizza pubblicazioni su carta e siti web. vai al sito di Galileo Servizi Editoriali

Partners