LastMile - Narrowing the Usability Gap of Software Verification

Con la crescita inarrestabile delle applicazioni del software, diventa sempre più impellente la necessità di verificarlo per accertarsi che i programmi sviluppati non abbiano errori o imperfezioni che ne rendono l’utilizzo difficile o insicuro. L’informatica ha fatto progressi notevoli nel campo dell’analisi e verifica formale del software; le tecniche sviluppate in questa area sono finalmente diventate applicabili a software di dimensioni e complessità realistiche. Ciononostante, la tecnologia di sviluppo del software (dai linguaggi agli strumenti di programmazione) è anch’essa in continua evoluzione. Pertanto, passare dall’invenzione di una nuova tecnica di verifica alla sua applicazione alle ultime versioni di un software spesso richiede uno sforzo oneroso e altamente specializzato.

Il progetto LastMile ha come obiettivo primario lo sviluppo di tecniche, metodi, e strumenti di verifica formale che siano più facilmente applicabili a software realistico e combinabili con altre tecniche simili. Questo obiettivo vuole colmare il cosiddetto “ultimo miglio” (“last mile”) che tuttora separa le tecniche di verifica sviluppate in ambito di ricerca e le pratiche comuni di sviluppo del software.

Uno dei modi chiave per colmare questo divario è lo sviluppo di adeguati linguaggi intermedi, che permettano di formulare e implementare le tecniche di verifica formale in maniera in buona parte indipendente dai dettagli del linguaggio usato per sviluppare il software da analizzare. In questo modo, ogni evoluzione o cambiamento sui due fronti (linguaggi di programmazione e tecniche di verifica) potrà essere più facilmente riconciliato ed integrato, senza richiedere uno sforzo straordinario di adattamento.

I risultati del progetto LastMile hanno il potenziale di rendere l’analisi formale del software più facile da implementare ed applicare in contesti realistici. Questo può contribuire allo sviluppo di software di qualità migliore e con meno errori, con benefici di lungo termine per tutti gli sviluppatori e utenti di software in senso lato.