2007 Turing Award

Sono stati resi noti i vincitori del Turing Award per il 2007: Edmund M. Clarke, E. Allen Emerson e Joseph Sifakis hanno vinto il cosiddetto Nobel dell’informatica per il loro lavoro sui metodi formali di verifica del design e dei requisiti di un sistema (hardware o software che sia). Il loro contributo in particolare ha consentito di sviluppare in modo pratico il metodo noto come Model Checking: attraverso la modellazione di un sistema concorrente in termini di formule di logica temporale, è possibile valutarne la bontà del funzionamento, ovvero è possibile determinare in modo automatico se il sistema rispetta una data specifica. I concetti chiave sono una modellazione attraverso un linguaggio che consenta di rappresentare stati temporali concorrenti, da cui è possibile derivare un albero temporale degli stati (i cui cammini di attraversamento rappresentano tutte i possibili stati in cui il sistema si verrà a trovare) e una logica temporale, detta Computational Tree Logic (CTL), che consenta di verificare delle proprietà del sistema stesso. L’applicazione pratica del Model Checking ha riscontrato successo soprattutto nel campo dell’hardware e limitatamente anche per il software (sono ad esempio note le esperienze di Nasa, Microsoft e Bell Labs).

Trovo questa notizia degna di essere menzionata per tre motivi: intanto i Turing Award sono rilevanti per chiunque si occupi di informatica, sia teorica che pratica, e poi per una volta questo premio dà un senso al termine science in Computer Science. Infine, vale la pena di ricordare che questi metodi spostano di fatto il problema dal sistema in sé verso il modello: sebbene in ambiti limitati la cosa calzi a pennello, è pur vero che la verifica formale avviene sul modello e quindi chi si occupa di verificare il modello stesso? Detto ciò, ben lungi da me sminuire i meriti di Clarke, Emerson e Sifakis.

Comments

  1. Negli approcci model-driven, il punto di partenza è appunto il modello da cui si genera codice da un lato e analisi statiche (model-checking) dall’altro.

    Nei sistemi critici, dove ci dev’essere sicurezza intrinseca dimostrabile, si fa così. Vedi ad esempio progetto ASSERT dell’ESA.

  2. Sostanzialmente si usa e si verifica il modello proprio perchè quello è il sistema, perchè non esiste iato tra i due elementi. A Londra conobbi un ricercatore italiano che periodicamente lavorava per la Nasa proprio per il Model Checking e, a parte il viaggio e il soggiorno tutto pagato in California, mi disse che si tratta di un lavoro piuttosto noioso e parecchio critico, in cui se sbagli ti fanno secco…!

  3. Fa piacere vedere che qualcuno ha vinto un riconoscimento proprio sull’argomento su cui stai strippando per passare il prossimo esame. 🙂

Policy per i commenti: Apprezzo moltissimo i vostri commenti, critiche incluse. Per evitare spam e troll, e far rimanere il discorso civile, i commenti sono moderati e prontamente approvati poco dopo il loro invio.