RICERCA ITALIANA     

AIDA2007 - Interpretazione Astratta: Progettazione e Applicazioni

Università degli Studi di Padova

Abstract

Le scienze e tecnologie informatiche devono affrontare la grande sfida di sviluppare metodologie, tecnologie e strumenti adatti alla specifica dei requisiti, alla progettazione di architetture, all’implementazione, alla verifica e al test, all’utilizzo, al mantenimento e alla protezione sia durante il funzionamento che nell’evoluzione di software che sia componibile, affidabile, flessibile, scalabile e robusto. Avanzamenti ed innovazioni scientifiche sono necessari per mantenere e per guadagnare porzioni di mercato. L’astrazione, come formalizzata dall’ interpretazione astratta, è indispensabile nei processi di sviluppo, integrazione, verifica, analisi, testing e protezione del codice. Lo scopo del progetto AIDA2007 –- che è la continuazione del progetto AIDA2004 che raggiunse pienamente gli obiettivi – è di rafforzare la ricerca italiana nell’ambito dell’interpretazione astratta, promuovendo l’interpretazione astratta come tecnologia per la costruzione di sistemi software affidabili. L’interpretazione astratta rappresenta la teoria di base per la progettazione di metodologie e per la costruzione di strumenti in grado si assicurare l’interoperabilità, la composizionalità, la scalabilità, l’affidabilità, la robustezza, la sicurezza e l’auto-adattamento del software. Si è dimostrato come l'interpretazione astratta sia una tecnologia fondamentale per software sequenziale, parallelo (sincrono e asincrono), a vincoli, distribuito e mobile che si trova in >>>

Coordinatore Scientifico del Programma di Ricerca

Francesco Ranzato Università degli Studi di PADOVA

Obiettivo del Programma di Ricerca

Lo straordinario sviluppo delle tecnologie hardware e software è all'origine della moderna società dell'informazione e della comunicazione. Promotrici della più grande rivoluzione economica e culturale del secolo scorso, tali tecnologie rappresentano tuttavia il tallone d'Achille della nostra società, perché sia in campo software che hardware requisiti quali affidabilità e sicurezza sono difficili da garantire. Ciò motiva la crescente importanza ed il costo assunti dalla validazione di software e hardware. Gli strumenti tradizionali di validazione hanno tuttavia una scalabilità ridotta e costi sempre maggiori, sono spesso inefficienti, vengono rilasciati lentamente e non garantiscono una qualità ottimale.

L' Interpretazione Astratta è un metodo generale, sia teorico che pratico, per approssimare la semantica del comportamento di un sistema di calcolo. Gli strumenti di validazione del software -- come analisi statica, model checking, type and effect system -- rivelano aspetti unificanti se riformulati in termini di interpretazione astratta. Tali strumenti descrivono in modo sicuro ma approssimato il comportamento di un sistema di calcolo astraendone sistematicamente la semantica, il modello o il programma. L'interpretazione astratta non solo formalizza queste astrazioni, ma ne permette pure il raffinamento e la combinazione, e si pone altresì come base per la modellazione di strumenti per la verifica di tali proprietà a vari >>>

Risultati parziali attesi

L'intento della proposta di progetto AIDA2007 è l'avanzamento dello stato dell'arte sull'interpretazione astratta (IA), sia dal punto di vista fondazionale, che da quello applicativo. Ciò avverrà tramite lo studio di specifici "Task" all'interno dei quattro WP che costituiscono AIDA2007. Vengono descritti nel seguito i risultati attesi da ogni singolo Task.

WP1: Progettazione di Interpretazioni Astratte

- Task PD-1.1: Domini astratti per il model checking
I domini astratti disgiuntivi risultano molto utili nel model checking astratto, e.g. nella predicate abstraction [MFHRS06] e negli algoritmi per il calcolo di equivalenze comportamentali [RT07b]. Intendiamo studiare come questi domini possano essere usati negli algoritmi di abstraction refinement. Poiché i domini astratti disgiuntivi sono caratterizzabili in termini di domini astratti completi per l'unione di insiemi, ci attendiamo di caratterizzare anche classi di domini astratti completi che possano essere vantaggiose per l'abstract model checking, e.g. domini astratti completi per qualche operatore temporale.

- Task PR-1.1: Domini astratti per l'analisi dei puntatori e dell'aliasing in programmi C e Java
L'approccio di [EGH94] alla stack pointer analysis di programmi C permette di definire un'analisi dipendente dal contesto e/o dal flusso capace di catturare l'aliasing sia >>>

Durata

24 mesi

Base di partenza scientifica nazionale o internazionale

L' interpretazione astratta è una ben nota teoria generale ed unificante per l'approssimazione della semantica formale di sistemi computazionali. Inventata da Cousot e Cousot [CC77, CC79] alla fine degli anni '70 come framewok unificante per progettare e validare analisi statiche di programmi, l'interpretazione astratta ha guadagnato sempre maggiore popolarità come metodologia generale per la descrizione e la formalizazione di computazioni approssimate in aree molto diverse dell'informatica come l'analisi statica di programmi, la trasformazione di programmi, la verifica di sistemi e programmi via model checking, i sistemi di tipi, l'analisi di sistemi mobili e distribuiti, la sicurezza, il constraint solving, etc. Come notevole recente esempio di applicazione dell'interpretazione astratta, ASTRÉE (http://www.astree.ens.fr/) è un analizzatore statico di programmi strettamente basato sulla teoria dell'interpretazione astratta che è riuscito a verificare formalmente l'assenza di errori a run-time nel software di controllo volo primario del sistema fly-by-wire dell'Airbus A340 (132,000 linee di codice C piuttosto peculiare). Ci stiamo avvicinando al punto in cui verranno inseriti analizzatori statici basati su interpretazione astratta negli ambienti di sviluppo dei principali linguaggi imperativi.

Gli obiettivi del progetto AIDA2007 sono strutturati in quattro WorkPackage (WP) che si focalizzano su >>>