RICERCA ITALIANA     

AIDA - Interpretazione Astratta: Progettazione e Applicazioni

Università degli Studi di Verona

Abstract

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. <<<

Coordinatore Scientifico del Programma di Ricerca

Roberto GIACOBAZZI Università degli Studi di VERONA

Obiettivo del Programma di Ricerca

Garantire l'affidabilita' e la sicurezza dei sistemi informatici e' una sfida fondamentale per le societa' moderne. Ci affidiamo a sistemi che pervadono la vita dell'uomo e sono sempre piu' complessi; nello stesso tempo sperimentiamo, talvolta in modo spettacolare, come i metodi tradizionali di validazione, ad esempio il testing, possano fallire, nonostante il loro costo elevato, nel compito di assicurare le garanzie richieste: il fallimento di Ariane 5 nel giugno 1996 e' un esempio famoso. Questo giustifica l'interesse crescente per tecnologie flessibili e basate sulla semantica per l'analisi, la verifica e la manipolazione di programmi in ogni fase dello sviluppo dei sistemi SW. L'interpretazione astratta puo' giocare un ruolo importante in questa prospettiva. In AIDA l'interpretazione astratta verra' utilizzata come la teoria fondamentale per definire metodologie e per sviluppare strumenti che assicurino interoperabilita', composizionalita', scalabilita', affidabilita', robustezza e sicurezza del software e dei sistemi. Lo scopo iniziale del progetto AIDA e' di mobilitare, unificare, galvanizzare e rinforzare la comunita' italiana di interpretazione astratta verso un obiettivo comune: la creazione di un'unica piattaforma per la certificazione automatica tramite interpretazione astratta. L'Italia ha una comunita' attiva da tempo nell'interpretazione astratta, come e' provato dal AIDA che comprende 7 universita', piu' di 25 ricercatori permanenti coinvolti direttamente nell'interpretazione astratta, piu' di 10 esperti di altri campi come sicurezza, sistemi ibridi, model checking e concorrenza, interessati all'interpretazione astratta come teoria fondamentale per la certificazione di sistemi, e piu' di 20 tra dottorandi e post-dottorato. Inoltre, l'interesse delle industrie italiane verso l'interpretazione astratta e' in crescita, come dimostrano i recenti contratti e l'interessamento in questo progetto da parte di GlaxoSmithKilne S.p.A (GSK), CAD-IT S.p.A e CRF - FIAT.

Siamo interessati in particolare alla certificazione di flussi sicuri di informazione, robustezza e affidabilita' di sistemi complessi che coinvolgono componenti software e hanno potenzialmente un comportamento ibrido. Affronteremo questo problema raffinando l'interpretazione astratta nell'analisi statica di programmi e nella sicurezza basata sui linguaggi, integrandola con tecniche basate su vincoli e con metodi di verifica come il model checking. Questo obiettivo verra' raggiunto identificando uno schema comune nella definizione di interpretazioni astratte nei seguenti workpackages (WP), coordinati da un esperto riconosciuto del settore: WP1: Analisi statica di programmi, WP2: Sicurezza, WP3: Testing, WP4: Sistemi Ibridi, WP5: Vincoli, e WP6: Verifica automatica.

WP1: Analisi statica di programmi. Siamo interessati all'analisi del flusso dei dati o del controllo mediante interpretazione astratta, in particolare nel contesto di calcoli concorrenti e OO. In questo campo siamo interessati ad aspetti fondamentali come i metodi per la definizione di domini astratti, la semantica astratta di calcoli concorrenti e mobili, e strategie di punto fisso come widening/narrowing. L'interesse in questa fase si focalizza particolarmente su nuovi domini astratti che forniscono informazione relazionale, il cui ruolo e' cruciale nella certificazione basata sul linguaggio della sicurezza del software (WP2).

WP2: Sicurezza. In questo ambito di lavoro siamo interessati sia all'indebolimento della nozione standard di non-interferenza tramite interpretazione astratta, sia nel mettere in relazione modelli semantici (come la bisimulazione) con l'interpretazione astratta e misure quantitative riguardanti la dispersione delle informazioni. Nell'ultimo caso sarebbe particolarmente interessante derivare modelli di attaccanti ibridi, che hanno comportamenti sia continui che discreti.

WP3: Testing. Siamo interessati al riutilizzo del codice e all'analisi statica modulare applicata alla regressione del codice, in connessione con WP1 e WP5. Il test di regressione, oltre a verificare se un bug sia stato riparato, e' utilizzato anche come duale del test di integrazione: quando nuovo codice e' aggiunto al codice esistente il test di regressione verifica che il codice gia' esistente continui a funzionare correttamente, mentre il test di intergrazione verifica che il nuovo codice funzioni come richiesto. Il vantaggio dell'interpretazione astratta in questo ambito e' chiaro, essendo la composizionalita' una delle caratteristiche fondamentali delle tecniche basate sulla semantica; questo e' vero in particolare nella derivazione automatica di precondizioni per i problemi di test di regressione per la composizione di codice e per isolare vettori di test invarianti rispetto alla modifica del codice.

WP4: Sistemi Ibridi. Siamo interessati a modellare e definire tecniche di verifica per sistemi ibridi combinando vincoli e interpretazione astratta standard. In particolare ci interessa usare l'interpretazione astratta per derivare sistematicamente sistemi discreti approssimati da un sistema ibrido. Questo approccio prevede il miglioramento delle tecniche di design di domini astratti (per esempio quelle sviluppate per i domini numerici in WP1) come i modelli basati sui vincoli per gli automi a regioni e le compressioni e i raffinamenti di domini per bilanciare il fenomeno dell'esplosione degli stati e il bisogno di astrazioni che soddisfino la preservazione forte relativamente a un certo frammento di logica temporale. Questo WP e' fortemente legato a WP1, WP2, WP5 e WP6.

WP5: Vincoli. Prevediamo di studiare l'applicazione combinata di interpretazione astratta e programmazione con vincoli per l'analisi e la verifica di programmi software multithreaded. Per l'applicazione ad esempi pratici e' importante studiare come estrarre modelli astratti da programmi e come rendere composizionali le analisi. Inoltre siamo interessati ad integrare le tecniche basate sui vincoli sviluppate per domini astratti relazionali in WP1 con logiche e vincoli studiati in WP6, allo scopo di ottenere strumenti pratici per certificare sistemi complessi e, unitamente a WP4, per raffinare automi a regioni.

WP6: Verifica automatica. Siamo interessati al design sistematico di model checking astratto che verifichi la preservazione forte relativamente a certi frammenti di una logica temporale, nel contesto di strutture temporali a piu' livelli, come vincoli, metriche e periodicita'. Il nostro interesse e' volto in particolare a derivare la logica piu' forte per cui il model checking astratto relativo ad un'astrazione fissata soddisfa la preservazione forte. Inoltre cercheremo di capire il ruolo dei trasformatori di domini astratti, come il raffinamento e la compressione di astrazioni, per ottenere strumenti efficienti di verifica nel model checking astratto.

Identifichiamo un percorso comune che sara' condiviso da tutti i WP di AIDA; esso consiste nelle 5 fasi seguenti, ognuna coordinata da un esperto riconosciuto di interpretazione astratta. La sequenza delle fasi 1--5 e' l'agenda standard nelle definizione di una qualsiasi interpretazione astratta:

Fase 1: Proprieta' delle astrazioni
Fase 2: Domini astratti
Fase 3: Modelli e semantiche
Fase 4: Strategie di punto fisso e algoritmi
Fase 5: Implementazione

L'organizzazione matriciale del progetto in ambiti di lavoro (WP) e fasi assicura il corretto coordinamento tra i diversi elementi. In particolare, condividendo le stesse fasi, ogni WP beneficiera' di tecnologie comuni nel design e nell'implementazione di interpretazioni astratte. Ogni partner sara' coinvolto direttamente in WP e fasi attraverso attivita' localizzate coordinate dai responsabili di WP e dai coordinatori delle fasi.

<<<

Risultati parziali attesi

I risultati attesi in questa fase sono:
- Una ben definita algebra dei trasformatori di domini astratti, che includa le proprieta' rilevanti delle astrazioni codificate come trasformatori di domini astratti, come preservazione forte nel model checking astratto di sistemi discreti e ibridi riguardo a frammenti della logica temporale, assenza di falsi allarmi in domini astratti numerici e relazionali, e composizionalita' per il test di regressione (tutti i WP)
- Condizioni precise per l'invertibilita' di domini astratti e relativi algoritmi per invertire raffinamenti di domini astratti nel senso della compressione di domini, ovvero verso un'operazione che restituisce, quando esiste, il piu' astratto dominio che ha lo stesso raffinamento del dominio in input (WP1, WP4 e WP6)
- Estensione dell'algebra dei trasformatori di domini a strategie di punto fisso, come tecniche di widening/narrowing (WP1, WP4, e WP5)
- Una caratterizzazione delle proprieta' dei sistemi ibridi come proprieta' delle loro astrazioni (WP4)
- Una tassonomia di astrazioni nel model checking astratto sotto il requisito della preservazione forte relativamente al frammento del mu-calcolo (WP6).I risultati attesi da questa fase sono:
- Miglioramento dei domini per l'analisi attribute-independent di programmi su domini numerici (WP1)
- Miglioramento dei domini per l'analisi relazionale di programmi su domini numerici (WP1 e WP5)
- Il progetto di domini simbolici piu' precisi per l'analisi di codice OO, adeguati per la composizionalita' (WP1, WP2 e WP5)
- Il progetto sistematico di domini astratti per l'interferenza di tipi (WP1, WP2 e WP6)
- Il progetto di domini e operazioni ottimali per l'aliasing in linguaggi di programmazione dichiarativi (WP1)
- Il progetto di domini per l'approssimazioni di regioni per la discretizzazione di automi ibridi (WP4)
- Rafforzare i domini con misure quantitative (WP1 e WP2)
- Un ambiente logico per trattare astrazioni sui domini visti come come certificati, ovvero tipi (WP2).I risultati previsti per questa fase sono:
- Progetto di modelli composizionali per analisi statica e verifica in mobile ambient
- Progetto semantiche per modellare la non-interferenza astratta in calcoli concorrenti
- Progetto di semantiche per modellare la non-interferenza astratta in sistemi real-time e ibridi
- Progetto di sistemi di prova orientati alla sintassi per non-interferenza astratta
- Progetto di modelli per linguaggi multithreaded basati sui linguaggi CCP e CHRI risultati attesi in questa fase sono:

- Strategie di punto fisso avanzate per domini numerici (WP1, WP4, WP5, e WP6)
- Trattazione di poliedri NNC (WP1, WP4, e WP5)
- Analisi di escape e analisi delle classi con insiemi di vincoli (WP1 e WP5)I risultati attesi in questa fase sono:
- Una libreria general purpose di domini numerici per l'analisi relazionale e attribute-independent di programmi (WP1 and WP5)
- Un'implementazione efficiente per l'analisi di classi e la escape analisi in Julia (WP1 e WP5)
- Una valutazione sperimentale del raffinamento e della compressione del dominio astratto nel contesto dell'abstract model checking (WP6)
- Un prototipo di architettura PCC-like per la certificazione della non interferenza astratta per quanto riguarda certificati come predicate abstractions (WP2)
- Un prototipo du un program slicer parametrico che implementi i criteri dello slicing basato sulla non interferenza astratta (WP3 and WP3).
- Un prototipo di model checker per programmi concorrenti con vincoli (WP4, WP6 e WP5). <<<

Durata

24 mesi

Base di partenza scientifica nazionale o internazionale

L'interpretazione astratta e' una nota teoria per approssimare la semantica di sistemi dinamici [CC77]. Introdotta dai Cousot [CC77] come teoria adeguata sia al progetto che alla dimostrazione di correttezza di analizzatori statici di programmi, negli ultimi anni l'interpretazione astratta e' diventata molto diffusa come tecnica generale per la descrizione e la formalizzazione di computazioni astratte in diverse aree dell'informatica. In AIDA siamo interessati allo sviluppo di metodi che siano comuni alle diverse applicazioni dell'interpretazione astratta dall'analisi statica di programmi, alla sicurezza, alla verifica e al testing per sistemi discreti/ibridi.

- Progetto di domini astratti e loro applicazioni
Il successo dell'interpretazione astratta e' dato dalla semplice, ma rigorosamente definita, idea per cui la specifica del comportamento di un sistema, ad esempio un programma, a diversi livelli di astrazione, e' data da una opportuna astrazione della sua semantica formale [C76th,CC777,JN95,NNH99]. In questo progetto siamo interessati nell'uso dell'idea che sta alla base dell'interpretazione astratta, ovvero l'analisi di sistemi attraverso l'approssimazione della loro semantica, come paradigma concreto e adeguato sia per il progetto che per per la specifica di nuovi metodi di certificazione sia per componenti SW che per sistemi dinamici ibridi. Una caratteristica fondamentale dell'interpretazione astratta e' che gran parte delle proprieta' dell'analisi derivano da proprieta' del sottostante modello concreto di calcolo (semantica) e dall'astrazione, quest'ultima univocamente identificata dal dominio astratto scelto. Quindi, trasformare domini e semantiche corrisponde a trasformare analizzatori. Sono state sviluppate diversi operatori per migliorare in modo sistematico la precisione, ridurre la complessita', e rendere l'analisi modulare raffinando, semplificando e decomponendo domini. La base della teoria dei domini astratti e dei trasformatori di domini astratti e' stata stabilita dai Cousot in [CC79]. Successivamente e' stata introdotta una struttura algebrica per i trasformatori di domini astratti in [FGR96,GR97,GR98unif]. Comunque, mentre e' noto il metodo per la derivare modelli approssimati corretti e completi dalle astrazioni [CC99], non sono noti metodi analoghi per derivare trasformatori di domini. La maggior parte delle operazioni note per raffinare e semplificare i domini sono di fatto o il risultato di soluzioni a problemi specifici di raffinamento o semplificazione (complemento disgiuntivo [CC79,CC94,J92], raffinamenti di completezza e kernel [GRS00], potenza ridotta [CC79] e comlemento di Heyting [GS98]) o derivati direttamente dalla struttura del reticolo dell'interpretazione astratta (prodotto ridotto[CC79] e complemento [CFGPR97]). La completezza gioca un ruolo fondamentale nell'interpretazione astratta [BPR02], in particolare molti problemi che hanno a che fare con il raffinamento di astrazioni sono problemi di completezza. Mentre l'interpretazione astratta assicura la correttezza, la completezza richiede che, relativamente alle proprieta' espresse dal sotostante dominio concreto, non ci sia perdita di informazione durante la compuatzione astratta. E' sempre possibile ottenere astrazioni complete [GRS00] come il piu' piccolo rasffinamento e la piu' grande restrizione di completezza di un dominio astratto. Sono state introdotte due nozioni di completezza in [GQ01]: completezza forward e backward, dove la seconda coincide con la definizione classica di completezza [CC79]. Queste due definizioni corrispondo rispettivamente a richiedere che il dominio astratto includa l'immagine diretta e inversa della semantica per cui deve essere completo. Questi risultati forniscono dei trasfirmatori di domini astratti per ottenere entrambe le forme di comletezza raffinando o semplificando i domini. Comunque, per aumentare l'efficienza, spesso non e' sufficiente il disegno di un adeguato dominio astratto. L'esperienza fatta in Italia con lo sviluppo di China [BHZ02,ZHB02] e con l'attuale sviluppo della ``Parma Polyhedra Library'' [BHRZ03, BHZ03, BRZH02] ha mostrato che la creazione di un dominio astratto professionale e' un importante e complesso lavoro, che richiede complesse trasformazioni di domini e l'impegno di persone per diversi anni. Spesso vengono richieste efficienti startegie di punto fisso come le tecniche di accelerazioni di punto fisso di widening/narrowing [CC77], e spesso queste sono il valore aggiunto di molti algoritmi per l'analisi di programmi basati sull'interpretazione astratta. Questo diventa cruciale per domini relazionali, come i poliedri [CH78], dove le astrazioni forniscono approssimazioni precise delle relazioni tra le variabili di un programma. Gli sviluppi piu' recenti in questo campo portano alla ricerca di un compromesso tra precisione e complessita'. Ad esempio, gli ottagoni [Min01] offrono un esempio di astrazione relazionale semplice e computazionalmente efficiente. L'analisi relazionale ha rilevanza nell'analisi di complessita'. Questo e' un campo inesplorato, il cui obiettivo e' la derivazione di upper e lower bounds alla complessita' degli algoritmi, dei processi, delle strutture di dati e dei programmi, attraverso l'approssimazione della semantica. I risultati di tali analisi, che possono essere parzialmente o totalmente automatiche, possono essere usati per decidere se agenti mobili sono abilitati ad essere eseguiti in un dato contesto, per assistere i programmatori nello studio del comportamento dei programmi, e per guidare le applicazioni di ottimizzazioni a progarmmi [DL93].

- Sicurezza
Sistemi di tipi, analisi di dati/controllo (CFA) basati su logiche di flusso, e interpretazione astratta sono le piu' note tecniche, applicate con successo alla verifica statica di proprieta' di sicurezza di sistemi mobili e distribuiti, modellati nel calcolo degli ambienti o in qualche sua variante [LS03,MPW92], o modellati mediante calcoli orientati agli oggetti. La logica di flusso [NN02] e' basata su un'analisi con vincoli che permette di integrare lo stato dell'arte con l'interpretazione astratta e l'analisi dei flusso di dati. Nel calcolo degli agenti mobili, l'interpretazione astratta e' stata principalmente applicata in [LM04,HJNN99] per raffinare le analisi esistenti, come la CFA di [NNH99] e la logica di flusso, tutte finalizzate a certificare la sicurezza mediante analisi di flussi di dati/controllo da canali confidenziali a canali pubblici. In un sistema, l'informazione e' tipicamente protetta mediante politiche di controllo degli accessi, limitando gli accessi delle entita' (come utenti o processi) ai dati. Nella sicurezza multi-livello [BP] le entita' e i dati sono associati a livelli di sicurezza (ordinati) e nessun accesso ai dati ai piu' alti livelli e' mai possibile, anche se il proprietario dei dati volesse rivelarli. Queste rigide politiche di sicurezza sono state progettate per evitare attacchi interni dai cosi' detti cavalli di Troia, i.e., software malintenzionato che, una volta eseguito da un utente, modifica i diritti di accesso dei dati appartenenti a tale utente. Sfortunatamente, anche quando il diretto accesso ai dati e' vietato da (rigide) politiche di sicurezza puo' accadere che i dati vengano indirettamente rilasciati da cavalli di Troia che possono osservare alcuni effetti collaterali osservabili del sistema come, e.g., il load della CPU o, piu' in generale, la disponibilita' di spazio/tempo delle risorse condivise (si veda per esempio [M89]). La necessita' di controllare il flusso di informazione (sia diretto che indiretto) ha motivato Goguen e Meseguer nell'introdurre la nozione di non-interferenza [GM82]. La non-interferenza richiede che gli input confidenziali non influiscano sugli output dell'interfaccia pubblica del sistema. Se una tale proprieta' vale, si puo' concludere che nessun flusso di informazione e' mai possibile dal livello confidenziale a quello pubblico. Questo e' chiaramente una condizione troppo restrittiva, dal momento che la maggior parte delle variabli sono semanticamente dipendenti, la maggior parte dei programmi non passerebbe un rigoroso test di non-interferenza. Il problema di raffinare le politiche di sicurezza, ovvero di indebolire la non-interferenza, e' stato considerato come un obiettivo principale nella sicurezza basata sui linguaggi (si veda [SM03]). In[GM04,Low02,VS00] il problema di caratterizzare il grado di sicurezza dei programmi e'stato relazionato alla potenza dell'attaccante attivo/passivo. L'idea in [GM04] e' quella di considerare gli attaccanti come interpretazioni astratte, il cui obiettivo e' quello di rivelare proprieta' dei dati confidenziali analizzando staticamente le risorse pubbliche. Un trasformatore di domini caratterizzante il piu' potente attaccante passivo incapace di ottenere proprieta' dei dati confidenziali analizzando i dati pubblici e' stato introdotto insieme ad un trasformatore di domini che identifica la maggior quantita' possibile di informazione rilasciata da un programma sotto attacco. L'estensione della non-interferenza astratta a modelli piu' complessi di interazione, per esempio a protocolli di comunicazione, e di computazione (per esempio concorrenza e non determinismo probabilistico) e' ancora aperta. Al fine di coprire anche modelli semantici piu' complessi, le astrazioni devono essere ulteriormente raffinate. L'idea di arricchire l'interpretazione astratta con aspetti probabilistici e quantitativi e' relativamente nuova e ha un grande impatto nella sicurezzabasata sui linguaggi [SM03]. L'approccio sviluppato in [M00] consiste nell'applicazione delle tecniche basate sull'interpretazione astratta (classica) per fornire limiti superiori alla probabilita' del caso peggiore di una data proprieta' di programma, mentre in [M01] e' stata proposta una combinazione di testing casuale e interpretazione astratta per l'analisi di programmi con caratteristiche di non determinismo sia probabilistico che non probabilistico. Ulteriori tecniche sono state proposte in [DW00a,DW00b] riadattando il framework classico in un ambiente probabilistico. La non-interferenza standard e' stata anche considerata in ambienti differenti come le algebre dei processi [RS01,FG01], modelli con tempo [GLM03], protocolli crittografici [FGM00]. In [FG01] il concetto di non-interferenza in una Algebra dei Processidi Sicurezza (SPA) e' stata introdotto in termini di semantica di bisimulazione. Un sistema E e' BNDC (non deducibilita' sulla composizione basata sulla bisimulazione) se cio' che un utente ad un livello basso (pubblico) vede del sistema non e' modificato (nel senso della semantica di bisimulazione) dalla composizione di un qualunque processo a livello alto (privato) con E. Il principale vantaggio della BNDC rispetto alle proprieta' basate sulle tracce e' che esso e' potente abbastanza da rilevare flussi di informazione dovuti alla possibilita' che ha un processo ad alto livello malintenzionato, di bloccare o sbloccare un sistema. In [FG01] viene mostrato che un processo malintenzionato puo' costruire un canale di flusso dal privato al pubblico, bloccando e sbloccando adeguatamente alcuni servizi di sistema accessibili agli utenti di basso livello. Il sistema usato per costruire questi canali coperti risulta essere sicuro per proprieta' basate sulle tracce, giustificando la considerazione della bisimulazione come semantica piu' concreta.

- Interpretazione astratta e verifica da sistemi discreti a sistemi ibridi
Le astrazioni per i metodi di verifica automatica come il Model Checking, costituiscono gia' da lungo tempo un interessante tema di ricerca. L'approccio del Model Checking astratto [CGL94,CGP99] fornisce una soluzione alla delicata questione della scalabilita' del Model Checking, ed al noto problema dell'esplosione degli stati: l'idea di base e' di valutare le specifiche di correttezza di un (modello di un) sistema reattivo M su un modello astratto che approssima le proprieta' di interesse del modello concreto M. Un modello astratto A preserva fortemente un linguaggio di specifica L quando ogni formula di L e' valida nel modello astratto A se e solo se essa e' valida nel modello concreto M. Chiaramente, questa e' una proprieta' fortemente auspicabile per il Model Checking astratto, in particolare perche' essa elimina i "controesempi spuri" nella verifica astratta [CGJLV03,GQ01]. Le relazioni tra interpretazione astratta e Model Checking astratto sono state oggetto di numerosi studi [CC99, CC00, CC02, CGL94, DGG97, GQ01, GR02,LGSBB95, Ran02]. L'approccio classico al Model Checking astratto [CGL94,CGJLV03] e' basato sulla definizione di un modello astratto come una partizione dell'insieme degli stati del sistema. Studi recenti [RT04] hanno dimostrato che la preservazione forte per il Model Checking astratto classico relativamente a uno specifico modello astratto si puo' ottenere sistematicamente con trasformazioni di astrazioni. Gli autori hanno dimostrato che il problema del raffinamento minimale di un modello astratto A per ottenere le preservazione forte per qualche linguaggio di specifica L corrisponde esattamente al problema del raffinamento minimale della sottostante interpretazione astratta per ottenere la completezza rispetto agli operatori logici/temporali di L. I vincoli giocano un ruolo chiave nella verifica di sistemi a stati infiniti [Del03], in particolar modo nella verifica di protocolli di comunicazione [AB02]. In questo approccio, i vincoli sono visti come rappresentazione simbolica di "modelli astratti del sistema". L'applicazione di questa tecnologia a programmi a multiprocessi affrontata in [DRV02] richiede un passo preliminare di astrazione in cui un "modello" e' estratto dal programma, e questo passo puo' chiaramente essere formalizzato come un Interpretazione Astratta. Contrariamente al caso discreto, l'utilizzo dell'Interpretazione Astratta nell'analisi dei Sistemi Ibridi e' ancora un campo di ricerca aperto. I Sistemi Ibridi hanno ottenuto una considerevole attenzione in letteratura [MMP92,ACH+95,LSV03] dato che risultano utili per la descrizione di sistemi reali, compresi i sistemi di controllo digitali di impianti e sistemi biologici. Un sistema ibrido descrive oggetti che esibiscono sia un comportamento discreto che continuo, e.g derivanti dal campo della Control Theory [ACB+01]. C'e' un estesa letteratura riguardante i modelli per i sistemi ibridi e le relative tecniche di verifica [vedi, ad es., MMP92,ACH+95,LSV03]. Le difficolta' stanno nelle correlazioni tra comportamenti discreti e continui. In particolare, avendo a che fare con la verifica, si conosce bene come trattare sistemi discreti e continui separatamente, ma si sa poco riguardo a tecniche di verifiche ibride. La maggior parte delle tecniche esistenti riduce il problema all'analisi di sistemi completamente discreti o a quella di sistemi completamente continui. C'e' inoltre un'estesa letteratura riguardante il Model Checking di sistemi ibridi [vedi, ad es., ACH+95]. In letteratura un automa ibrido viene trasformato in un automa discreto, solitamente chiamato una automa delle regioni o automa a zone, in modo che sia preservata la validita' di formule logiche temporali. La trasformazione di automi ibridi in automi discreti non e' in generale efficace, e in effetti il Model Checking di sistemi ibridi non e' decidibile. Per questo la letteratura e' concentrata nell'identificazione di sotto-classi appropriate di automi ibridi in cui sia possibile la costruzione di automi delle regioni. La classificazione di Henzinger et al. in [HM00] introduce il concetto di sistemi di transizione simbolica per generalizzare l'idea che sta dietro gli automi delle regioni e gli automi a zone. Vengono descritte cinque classi di sistemi di transizione simbolica che sono caratterizzati in termini di operatori di chiusura appropriati e di opportune sotto-logiche che vengono preservate. <<<