Certificazione automatica di sistemi mediante interpretazione astratta (PRIN 2004)

Starting date
November 30, 2004
Duration (months)
24
Departments
Computer Science
Managers or local contacts
Giacobazzi Roberto
URL
2004013015_001
Keyword
INTERPRETAZIONE ASTRATTA;ANALISI STATICA DI PROGRAMMI;DOMINI ASTRATTI;SEMANTICA;VERIFICA DI PROGRAMMI

L'interpretazione astratta e' una teoria generale per l'approssimazione di sistemi dinamici, ampiamente utilizzata ad esempio per derivare formalmente strumenti di analisi statica e verifica di programmi a partire dalla loro semantica. In AIDA, l'interpretazione astratta e' vista come teoria fondamentale ed unificante per la progettazione di metodologie e lo sviluppo di strumenti per assicurare l'interoperabilita', la composizionalita', l'affidabilita', la robustezza, e la sicurezza di sistemi software. L'obiettivo iniziale del progetto AIDA e' di mobilitare, unificare, galvanizzare e rafforzare la comunita' italiana dell'interpretazione astratta attraverso un obiettivo comune che consiste nella realizzazione di un'unica piattaforma avanzata per la certificazione di sistemi attraverso interpretazione astratta. Siamo particolarmente interessati alla certificazione di flussi sicuri di informazione, robustezza e affidabilita' di sistemi complessi che coinvolgono componenti software e che hanno un potenziale comportamento ibrido. Affronteremo questo problema raffinando gli esistenti metodi propri dell'interpretazione astratta nell'ambito dell'analisi statica di programmi e nella sicurezza, integrandole con descrizioni basate sui vincoli di sistemi dal numero infinito di stati e metodi di verifica come il model checking. Il risultato verra' ottenuto individuando un modello comune per la progettazione dell'interpretazione astratta nell'analisi statica do programmi, nella sicurezza, nel testing, nei sistemi ibridi, nei vincoli e nella verifica automatica. L'interpretazione astratta fornisce in questo caso un framework comune, dove problemi derivanti da diversi aspetti della certificazione di sistemi, che possono essere profondamente diversi come natura e applicazione, possono essere integrati, arricchiendo di nuovi strumenti l'interpretazione astratta teorica e pratica. La certificazione automatica di sistemi sia per sistemi dinamici discreti che per sistemi ibridi rappresenta il contesto ideale sia per studiare nuovi aspetti fondamentali dell'interpretazione astratta, come la teoria dei domini, la precisione e la complessita' dell'analisi statica di programmi, sia per fornire utili strumenti per la certificazione di sistemi basati sulla semantica che possono essere direttamente utilizzati nei moderni sistemi software.

Sponsors:

Ministero dell'Istruzione dell'Università e della Ricerca
Funds: assigned and managed by the department
Syllabus: COFIN - Progetti di Ricerca di Interesse Nazionale

Project participants

Roberto Giacobazzi
Full Professor
Roberto Segala
Full Professor
Nicola Fausto Spoto
Associate Professor

Activities

Research facilities