RICERCA ITALIANA     

Programma di ricerca

AIDA - Interpretazione Astratta: Progettazione e Applicazioni

Università di riferimento

Università degli Studi di PADOVA - MATEMATICA PURA ED APPLICATA - PADOVA(PD)

Responsabile dell'Unità di ricerca

Francesco RANZATO

Descrizione

Il progetto è strutturato in WorkPackage (WP) che raggruppano aree di studio e di applicazione dell'interpretazione astratte. L'unità di ricerca di Padova contribuirà prevalentemente a WP2, WP5, WP6. Il programma delle attività è il seguente. WP2: Sicurezza Le basi di partenza del WP2 riassunte precedentemente possono condurre a vari risultati interessanti. Task PD-2.1 Il punto (Sic-1) sopra discusso indica che sarebbe interessante definire un'analisi statica del pi-calcolo che sfrutti appieno la semantica delle operazioni eseguite per inferire informazioni precise. Intendiamo seguire questa direzione di ricerca in modo da estendere allo spi-calcolo un'analisi statica precisa ed efficiente che abbiamo recentemente definito per il pi-calcolo [CFG03]. Task PD-2.2 Per quanto concerne il punto (Sic-3) intendiamo modellare esplicitamente (cioè mediante un particolare processo) il contesto peggiore di un protocollo dato. In questo modo il contesto non dovrebbe essere gestito in modo speciale nell'analisi, ma sarebbe sufficiente applicare l'analisi al protocollo assieme al suo contesto peggiore. Task PD-2.3 La modellazione esplicita del contesto peggiore permetterebbe anche di affrontare un problema spesso trascurato. Considerando i messaggi scambiati da un protocollo spesso non si considera che il contesto possa inventare messaggi propri per confondere i principali onesti. L'astrazione del punto (Sic-2) è finora ottenuta assumendo che le copie di termini prodotte dalla replicazione fossero tutte uguali o equivalentemente che avessero tutte lo stesso tipo. In questo modo si ottiene che i termini che possono venir costruiti sono regolari e quindi caratterizzabili in modo finito. Sarebbe importante definire astrazioni che garantiscano comunque la finitezza dell'analisi, ma che siano meno restrittive. Un esempio di un tale approccio è l'analisi del pi-calcolo proposta in [Fer01]. WP5: Vincoli All'interno di questo workpackage ci si propone di studiare le proprietà del framework di interpretazione astratta per vincoli soft e di valutarne l'utilità e la convenienza sia teoricamente che sperimentalmente per varie classi di vincoli soft. Una prima valutazione sperimentale su vincoli fuzzy [DFP93] ha mostrato risultati promettenti [BPR04]. Prevediamo di strutturare la ricerca nei seguenti task. Task PD-5.1 Analizzeremo la metodologia attuale per l'astrazione di vincoli soft [BCR02], studiando le relazioni con altri framework esistenti per l'astrazione di vincoli hard. L'obiettivo è quello di estendere la metodologia in [BCR02] attraverso le caratteristiche più interessanti che appiaono nei framework per l'astrazione di vincoli classici. In particolare studieremo quelle estensioni che permettano di migliorare l'efficienza di un risolutore senza perdere troppa informazione nell'astrazione. Ci si prefigge inoltre di studiare e sviluppare algoritmi per l'astrazione di vincoli soft, basati su computazioni di punto fisso. Task PD-5.2 Implementeremo e valuteremo sperimentalmente gli algoritmi sviluppati nel precedente task per varie classi di vincoli soft. Considereremo sia classi di problemi generati casualmente che problemi reali. Queste classi di vincoli conterranno vari parametri, uno dei quali sarà la struttura dei vincoli soft. Ad esempio, considereremo le classi dei vincoli fuzzy e dei vincoli Max-CSP (dove si massimizza la somma dei pesi dei vincoli), che sono quelle più diffusamente usate e le cui caratteristiche sono estremamente diverse tra loro. WP6: Verifica Automatica Task PD-6.1 Quando una specifica f non è valida su un modello M, un algoritmo di verifica basato su model checking produce un controesempio alla validità di f su M. L'algoritmo di model checking su un modello astratto A produce quindi controesempi astratti. Un controesempio astratto per f su A può essere spurio, cioè un controesempio artificiale per f provocato dall'approssimazione del modello astratto A a cui non corrisponde alcun controesempio reale sul modello concreto M. Clarke et al. [CFHKQST03, CGJLV00, CGJLV03, CJLV02] hanno proposto una tecnica di raffinamento del modello astratto A guidata dai controesempi spuri: [CGJLV03] hanno specificato un algoritmo per testare quando un controesempio T prodotto dal model checker per una specifica f su un modello astratto classico A -- una partizione degli stati del sistema -- è spurio ed un algoritmo di raffinamento del modello astratto A che elimina il controesempio spurio T. Questa metodologia di raffinamento basata su controesempi è completa per un frammento del linguaggio ACTL*. Clarke et al. hanno dimostrato sperimentalmente l'efficacia di questa tecnica di raffinamento su casi di studio complessi. In questo task ci si propone di sfruttare l'approccio generico in [RT04a] per generalizzare la metodologia di raffinamento guidata dai controesempi a modelli astratti generali -- non necessariamente partizioni -- specificati mediante interpretazione astratta e a generici linguaggi induttivi (possibilmente diversi dal frammento di ACTL* in [CGJLV03]). In particolare, ci si prefigge di introdurre una nozione di conotroesempio spurio per modelli astratti generici e quindi un algoritmo che testa se un tale controesempio è spurio. Task PD-6.2 L'algoritmo di Paige-Tarjan [PT87] consiste nell'iterare la seguente operazione: una partizione degli stati corrente Q è rimpiazzata da una partizione raffinata Q' ottenuta da Q sostituendo un blocco B di Q in una coppia di sottoblocchi B1 e B2. Nella terminologia dell'interpretazione astratta questa operazione può essere vista come una "compressione" del dominio astratto corrente rispetto all'unione insiemistica [RT04b]. L'algoritmo generalizzato di Paige-Tarjan [RT04b] per raffinare modelli astratti per la preservazione forte per qualche linguaggio L è basato sull'esistenza di compressori di domini astratti. Sfortunatamente, i compressori raramente esistono. Tuttavia è possibile elevare le tecniche in [GRS00] per raffinare domini astratti per renderli completi ad un ordine superiore e renderle quindi applicabili per trasformare operatori di semplificazione in compressori. Questo task si pone l'obiettivo di usare questa metodologia per definire nuovi operatori di compressione (possibilmente diversi dalla compressione per l'unione insiemistica à la Paige-Tarjan) che possono essere integrati nello schema di algoritmo generalizzato di Paige-Tarjan [RT04b]. Task PD-6.3 Le tecniche precedentemente discusse ottengono la proprietà di preservazione forte del model checking astratto per un linguaggio L raffinando il modello astratto. Questo task si prefigge invece di affrontare il problema sotto una diversa prospettiva. Sia A un modello astratto rispetto ad un modello concreto M che non preserva fortemente un linguaggio L. Supponiamo che L sia un linguaggio definito induttivamente, cioè generato chiudendo le proposizione atomiche per un insieme Op di operatori logici/temporali (ad esempio AND, EX, AX, etc.). Gli operatori che generano un linguaggio possono essere comparati rispetto alla loro precisione: se f1:Pow(State)^n Pow(State) e f2:Pow(State)^m Pow(State) sono le interpretazioni semantiche sugli stati di due operatori logici/temporali allora f1 f2 può essere definito ad esempio puntualmente. L'idea è quindi di modificare sistematicamente (raffinare o semplificare) gli operatori in Op del linguaggio L per ottenere un linguaggio L' tale che il model checking astratto su A preservi fortemente L'. Usando i risultati in [RT04a] questo obiettivo si traduce nel seguente problema generale di interpretazione astratta: dato un dominio astratto A ed una operazione semantica f si tratta di raffinare/semplificare f in modo minimale a f' -- ad esempio rispetto all'ordinamento puntuale tra operazioni -- affinché A diventi completo per f'. Dalla prospettiva del model checking astratto un tale metodo permetterebbe di modificare in modo minimale il linguaggio invece che il modello astratto per ottenere la preservazione forte.