RICERCA ITALIANA     

Programma di ricerca

AIDA2007 - Interpretazione Astratta: Progettazione e Applicazioni

Università di riferimento

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

Responsabile dell'Unità di ricerca

Francesco Ranzato

Descrizione

Il piano dei lavori di questa proposta di progetto AIDA2007 è strutturata nei seguenti quattro WorkPackages (WPs):

WP1: Progettazione di Interpretazioni Astratte
WP2: Analisi Statica mediante Interpretazione Astratta
WP3: Protezione del Codice mediante Interpretazione Astratta
WP4: Verifica di Sistemi mediante Interpretazione Astratta

Mentre il WP1 si focalizza su aspetti relativi alla progettazione di una qualsiasi interpretazione astratta -- quali domani astratti, semantiche astratte, trasformazioni di domini astratti, etc. -- i WPs 2, 3 e 4 trattano le applicazioni dell'interpretazione astratta a tre specifiche aree di interesse. L'unità di ricerca di Padova contribuirà ai workpackages WP1, WP2 e WP4 lavorando sui seguenti task:

WP1: Progettazione di Interpretazioni Astratte

Task PD-1.1: Domini astratti per il model checking

L'approccio standard all'abstract model checking prevede l'uso di un sistema di transizione astratta, ovvero uno spazio degli stati astratti A e una relazione di transizione definita su A. Ad un tale spazio degli stati astratti corrisponde una partizione dello spazio degli stati concreti, e tali partizioni possono essere formalizzate come particolari domini astratti [RT07a]. Più in generale, un framework di abstract model checking può essere definito a partire da generici domini astratti [DGG97, Gan07, RT07a]. La classe dei domini astratti disgiuntivi risulta essere particolarmente utile nell'abstract model checking. I domini astratti disgiuntivi possono essere usati sia in predicate abstraction [MFHRS06] che negli algoritmi di raffinamento per la costruzione di domini astratti strongly preserving [RT07b]. Inoltre, essi ammettono una rappresentazione particolarmente efficiente che si basa sulla proprietà che l'approssimazione di un qualsiasi insieme di stati S si può ottenere mediante l'unione delle approssimazioni degli insiemi singoletto { s} in S. Come ulteriore utile proprietà, i domini astratti disgiuntivi possono essere usati sia come una sovra-approssimazione che come una sotto-approssimazione. Ci si propone di studiare se e come la classe dei domini astratti disgiuntivi possa essere utile in altre applicazioni, in particolare per gli algoritmi di raffinamento di astrazioni. Inoltre, prevediamo di studiare nuove classi di domini astratti che possano essere utilmente usati nell'abstract model checking. Poiché i domini astratti disgiuntivi possono essere caratterizzati come domini astratti che sono completi per l'unione di insieme di stati, intendiamo analizzare delle classi di domini astratti completi, ad esempio domini astratti che siano completi per altri connettivi logici/temporali.

WP2: Analisi Statica mediante Interpretazione Astratta

L'unità di ricerca di Padova è interessata allo studio di tecniche di analisi statica per modelli causali di sistemi concorrenti e distribuiti.

Task PD-2.1: Semantiche causali di sistemi concorrenti e distribuiti

In letteratura possono essere distinte due classi di modelli di concorrenza: nella prima classe di modelli, l'esecuzione indipendente di due processi è modellata specificando i possibili interleaving delle loro azioni; nella seconda classe, le relazioni di causalità tra le azioni di un sistema sono rappresentate esplicitamente. Ci si riferisce ai modelli della seconda classe come a modelli "true-concurrent", perché essi considerano la nozione di concorrenza -- oppure la nozione complementare di causalità -- come fondamentale. Ci si propone di studiare delle semantiche causali di sistemi concorrenti specificati come processi del pi-calculus. Possiamo trovare in letteratura numerose formalizzazioni del concetto di "true-concurrency". Tra queste, le strutture ad eventi sono particolarmente adatte per i tradizionali calcoli di processo come CCS e CSP. Le strutture ad eventi intuitivamente sono in grado di rappresentare fedelmente sia la causalità che la concorrenza semplicemente mediante un ordine parziale ed una relazione binaria irriflessiva. Il punto chiave della generalità e dell'applicabilità di tale modello sta nella composizionalità dell'operatore di composizione parallela: il comportamento della composizione parallela di due strutture ad eventi E1 e E2 è determinato dai comportamenti delle due strutture E1 e E2. Naturalmente, la composizionalità è una proprietà molto interessante in quanto permette di specificare e analizzare modularmente i sistemi concorrenti.

Abbiamo sviluppato in [CVY07] una semantica composizionale basata su strutture ad eventi per l'internal pi-calculus, che cattura le caratteristiche essenziali delle dipendenze causali generate dal "name passing" sia sincrono che asincrono. Intendiamo estendere questo approccio al "free name passing" con lo scopo di ottenere una semantica denotazionale fully abstract per il full pi-calculus. Siamo inoltre interessati allo studio di semantiche composizionali simili per linguaggi imperativi multithreaded che, se comparate alle algebre di processi, si focalizzeranno sullo stato piuttosto che sul controllo di un thread.

Task PD-2.2: Analisi statica di proprietà causali

Siamo interessati allo studio di tecniche di analisi statica per proprietà causali di processi concorrenti che si baseranno sui modelli "true-concurrent" dei sistemi concorrenti e distribuiti. I lavori [BS95, DP99, Cas95] rappresentano dei risultati preliminari verso questo obiettivo: dimostrano come le equivalenze comportamentali possano essere usate per catturare le dipendenze tra azioni di processi, sia in termini della loro struttura spaziale che delle loro capacità di comunicazione. Tuttavia, le equivalenze comportamentali studiate in questi lavori sono definite su labelled transition systems generalizzati. In questo progetti, ci proponiamo invece di studiare la causalità e la distribuzione spaziale dei processi che possono essere osservate tramite un modello di struttura ad eventi. Infatti, in un tale modello è possibile sfruttare il fatto che attraverso la rappresentazione esplicita di links causali, si ottiene anche una rappresentazione della struttura di scelta del sistema, esibendo dove le decisioni tra strade alternative di azioni sono intraprese.

La letteratura propone diverse nozioni di equivalenza su strutture ad eventi. Alcune di loro preservano l'action refinement e quindi possono essere usate per specificare modularmente sistemi concorrenti. Inoltre, il lavoro [Pin93] introduce un legame tra l'equivalenza comportamentale "history preserving" su strutture ad eventi e la logica di Milner arricchita con una modalità temporale di past-tense. A partire da questi lavori, ci si propone di studiare le caratterizzazioni logiche delle equivalenze su strutture ad eventi, ed in particolare le relazioni tra l'osservazione di distribuzione esprimibile mediante logiche spaziali per il pi-calculus e quella esprimibile tramite strutture ad eventi.

Intendiamo infine studiare il problema del model checking su strutture ad eventi. Si tratta di un problema intrinsecamente ostico, poiché in generale le strutture ad eventi sono modelli infiniti anche per processi con un numero finito di stati. Il lavoro [Pen97] fornisce un metodo per costruire delle rappresentazioni finite di una sottoclasse di strutture ad eventi che sfruttano delle tecniche di partial-order reduction. Siamo interessati ad investigare se e come l'approccio dell'interpretazione astratta al model checking possa essere applicato all'abstract model checking di strutture ad eventi.

WP4: Verifica di sistemi mediante interpretazione astratta

Task PD-4.1: Algoritmi di raffinamento di astrazioni

Quando una specifica di correttezza f non è valida su un dato modello di sistema M, un algoritmo di model checking produce in output un controesempio alla validità di f su M. Un 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 che scaturisce dall'approssimazione codificata nel modello astratto A e non corrisponde ad alcun controesempio reale sul modello concreto M. In un tale contesto, la tecnica dei raffinamenti di astrazioni guidati da controesempi (CEGAR, dall'inglese CounterExample-Guided Abstraction Refinement), inizialmente proposta dal gruppo di ricerca di E. Clarke [CGJLV03], è divenuta un approccio molto popolare ed effettivo per la progettazione di model checkers. L'idea di base della tecnica CEGAR è la seguente: se l'abstract model checker ritorna “YES” allora il sistema M soddisfa la specifica f; altrimenti, l'abstract model checker ritorna un controesempio astratto acex alla validità di f su A, che viene quindi analizzato per determinare se acex corrisponda ad un controesempio reale o meno; se si determina che corrisponde ad un controesempio reale allora si ritorna la risposta “NO”, altrimenti il modello astratto A deve essere raffinato con l'obiettivo di rimuovere quel controesempio spurio acex. I model checker basati su tale paradigma CEGAR considerano come controesempi dei cammini di stati astratti, ovvero cammini in un sistema di transizione astratto definito da uno spazio degli stati astratti e da una relazione di transizione astratta. Recentemente, Cousot, Ganty e Raskin [CGR07, Gan07] hanno introdotto un algoritmo di raffinamento di astrazioni -- nel seguito chiamato CGR -- che è guidato da punti fissi astratti piuttosto che da controesempi astratti. L'algoritmo CGR ha diverse caratteristiche innovative piuttosto interessanti. (1) CGR mantiene e raffina domini astratti generici che sono definiti nel framework standard dell'interpretazione astratta, in contrasto con la maggior parte degli algoritmi basati sul paradigma CEGAR che considerano come modelli astratti delle partizioni dello spazio degli stati. (2) Il raffinamento del dominio astratto corrente A è guidato dal punto fisso astratto calcolato dentro A e non da un cammino che funge da controesempio. (3) L'algoritmo CGR calcola sovra-approssimazioni sia di minimi punti fissi che di massimi punti fissi, e queste due analisi astratte sono rese sinergiche l'un l'altra.

Ci si si propone di investigare se e come l'approccio generale dell'interpretazione astratta possa essere applicato nel contesto dei raffinamenti di modelli astratti guidati da controesempi. In particolare, ci si pone l'obiettivo di generalizzare la metodologia di raffinamento guidata da controesempi a generici modelli astratti specificati tramite interpretazione astratta, ovvero modelli che non sono necessariamente partizione dello spazio degli stati, ed a generici linguaggi di specifica. Intendiamo inoltre studiare il ruolo dei domini astratti completi negli algoritmi di raffinamento di astrazioni. È noto che la completezza dei domini astratti ha delle relazioni precise con la proprietà per un modello astratto di essere strongly preserving [RT07a]. Inoltre, qualsiasi dominio astratto può sempre essere costruttivamente raffinato in modo minimale per diventare completo [GRS00]. Vogliamo quindi indagare se i raffinamenti di completezza possano essere utili per progettare o migliorare gli algoritmi di raffinamento di astrazioni, in particolare nel caso degli algoritmi guidati da punti fissi come l'algoritmo CGR.

Task PD-4.2: Trasformazioni di linguaggi

Si consideri un dato modello astratto A che non sia strongly preserving per un linguaggio L. Si assuma che L sia un linguaggio definito induttivamente, cioè L è generato chiudendo le proposizioni atomiche per applicazioni di un insieme Op di operatori logico/temporali (e.g. AND, EX, AX, etc.). Gli operatori che generano qualche linguaggio possono essere comparati mediante una relazione di ordine parziale, ad esempio mediante l'ordine di precisione relativa nel senso dell'interpretazione astratta. Pianifichiamo di studiare il problema di modificare sistematicamente, attraverso raffinamenti o semplificazioni minimali, gli operatori in Op che definiscono il linguaggio L con lo scopo di ottenere un linguaggio trasformato L' che sia tale che l'abstract model checking su A sia strongly preserving per L'. Ciò permetterebbe quindi di modificare in modo minimale il linguaggio di specifica L invece del modello astratto A per ottenere strong preservation. Intendiamo affrontare questa tipologia di problemi usando tipiche tecniche di interpretazione astratta, in particolare raffinamenti e semplificazioni di domini astratti. Come applicazione particolarmente rilevante, ci proponiamo di studiare come un tale metodo possa essere usato nel contesto del problema "branching vs linear" nel potere espressivo dei linguaggi temporali. Infatti, Maidl [Mai00] ha individuato un sotto-linguaggio LTL_det del linguaggio lineare LTL che caratterizza esattamente il potere espressivo branching di ACTL, ovvero le formule di ACTL che possono essere espresse linearmente in LTL. Questo problema può essere riformulato in termini di interpretazione astratta per mezzo dei domini astratti completi. Il nostro obiettivo è quindi quello di trasformare sistematicamente LTL in un sotto-linguaggio massimale L' che caratterizza il potere espressivo branching di ACTL.

Task PD-4.3: Algoritmi di calcolo di equivalenze comportamentali

Come abbiamo visto in precedenza, la proprietà di strong preservation viene raggiunta attraverso qualche azione di raffinamento di un modello astratto iniziale semplice. È possibile scegliere tra due diversi metodi di raffinamento: un modello astratto A è raffinato per ottenere o (1) strong preservation per tutte le formule di qualche linguaggio L o (2) strong preservation per una specifica formula f. La maggior parte dei raffinamenti di modelli astratti per ottenere strong preservation rispetto ad un intero linguaggio sono riconducibili al calcolo di qualche equivalenza comportamentale del modello astratto [Gla01], ad esempio l'equivalenza di bisimulazione per il mu-calculus e CTL* [BCG88], l'equivalenza di simulazione per ACTL* [GL94] e la bisimulazione branching per CTL*-X [DV95]. Pertanto, gli algoritmi che calcolano tali equivalenze comportamentali, e.g. tra termini di qualche algebra di processi, possono anche essere usati per ridurre in modo massimale lo spazio degli stati concreti di un dato modello di sistema mantenendo la proprietà di strong preservation per un corrispondente linguaggio. Abbiamo recentemente individuato un nuovo algoritmo di calcolo dell'equivalenza di simulazione [RT07b] che migliora la complessità di tempo sinora conosciuta. Questa procedura è stata ottenuta come una modifica di un algoritmo di calcolo della equivalenza di simulazione proposto da Henzinger, Henzinger e Kopke [HHK95] e si appoggia su tipici strumenti dell'interpretazione astratta come i raffinamenti di domini astratti e i domini astratti disgiuntivi. Una valutazione sperimentale ha inoltre dimostrato l'effettività pratica di questo algoritmo. Ci proponiamo di investigare se (1) questo algoritmo ammetta una versione simbolica efficiente basata su BDDs e se (2) le tecniche usate per definire questo nuovo algoritmo per l'equivalenza di simulazione possano essere generalizzate ed adattate per altre equivalenze comportamentali come la bisimulazione branching [DV95].