In questo progetto siamo interessati alla verifica di sitemi reattivi complessi.
Questi sistemi, ampiamente diffusi, mantengono una interazione permanente
con l'ambiente esterno, rispondendo con azioni appropriate agli stimoli,
e spesso eseguono attivita' critiche quali il controllo di impianti industriali,
la gestione di transazioni finanziarie, la temporizzazione di operazioni,
la gestione di applicazioni Web e di commercio elettronico.
Con l'aumento della dipendenza della nostra societa' dai computer e dai
sistemi reattivi la loro correttezza sta diventando sempre piu' critica,
tuttavia la loro verifica di correttezza e' particolamente difficile. Infatti,
i sistemi reattivi che incontriamo in applicazioni reali sono spesso formati
da numerose sottocomponenti che interagiscono con un ambiente esterno. Inoltre
la loro specifica puo' richiedere dati di tipo eterogeneo e puo' dipendere
da parameteri che non possono essere fissati a priori. Spesso infine lo spazio
degli stati possibili puo' essere infiito.
Tutti questi aspetti sono potenziali ostacoli per ragionare su proprieta' di tali sistemi in modo completamente automatico tramite la tecnologia che abbiamo oggi a disposizione. Consideriamo come esempio concreto il noto algoritmo di mutua esclusione proposto da Szymanski in [Szy90]. In questo algoritmo ogni componente di un sistema concorrente puo' essere rappresentata tramite un processo che mantiene nel suo stato locale il suo identificatore, una variabile di stato e delle variabili booleane. Il comportamento di ogni processo puo' essere descritto quindi tramite test e assegnamenti definiti su tali variabili. Una configurazione generica del sistema prevede K processi che in parallelo eseguono lo stesso protocollo. Per convalidare tale protocollo tramite tecniche quali symbolic model checking occorre quindi fissare un valore per il parametro K, codificare il nostro modello in logica proposizionale quantificata, ed infinie esplorare l'insieme delle sue possibili esecuzioni tramite rappresentazioni simboliche dello spazio degli stati. Anche se e' stata dimostrata l'efficacia di tale metodo per valori relativamente piccoli di componenti, quest'approccio non puo' essere applicato per valori crescenti di K a causa del problema dell'esplosione degli stati. Inoltre anche se le tecniche di model checking sono molto efficaci per la ricerca di errori, non possono essere usate tuttavia per verificare la correttezza del nostro protocollo per ogni valore di K. Data la complessita' e varieta' di aspetti correlati a problemi di verifica come quello appena descritto, sembra naturale cercare nuove direzioni di ricerca prendendo inspirazione da nozioni e tecniche mutuate da vari settori dell'informatica teorica e applicata.
Sulla base di queste considerazioni, l'obiettivo scientifico di questo progetto e' l'uso della nozione di `vincolo', opportunamente supportata dalle teorie dell'interpretazione astratta e dei tipi, quale concetto fondamentale per la specifica e verifica automatica di sistemi reattivi copmplessi. A tale scopo, abbiamo individuato i seguenti specifici obbiettivi di ricerca.
I obiettivo
Il primo obiettivo del progetto e' identificare linguaggi di specifica basati su vincoli per modellare sistemi reattivi complessi e per ragionare sulle loro proprieta'. L'uso di linguaggi basati su vincoli facilita la fase di modellazione. I vincoli infatti possono essere usati per esprimere in modo dichiarativo relazioni complesse definite sui dati. Grazie alla natura logica del concetto di vincolo, viene semplificata cosi' anche la fase di ragionamento basato su logiche per verifica sulle proprieta' del sistema codificato. Inoltre l'esistenza di numerosi linguaggi logici basati su vincoli, cosi' come numerosi risolutori di vincoli per domini matematici e simbolici, semplifica la fase di implementazione di prototipi per il ragionamento automatico. Gli esempi pratici verranno selezionati in classi di applicazioni particolarmente difficili per tecniche attuali di verifica automatica, ad es. l'esempio illustrato nella sezione precedente. Piu' in dettaglio, studieremo casi pratici di sistemi aperi e distribuiti, sistemi che dipendono dal tempo, astrazioni di programmi multithreaded, transazioni per il Web, e protocolli per il commercio elettronico.
II obiettivo
Il secondo ed il terzo obiettivo sono focalizzati sullo studio della fondamenta delle tecniche di verifica basate sui vincoli. Il secondo obiettivo consiste dello studio di tecniche di verifica basate su risoluzione di vincoli. In generale il goal di un risolutore di vincoli e' di quello di verificare la soddisfacibilita' di un vincolo tramite procedure specializzate ed efficienti. L'applicazione di questo paradigma computazionale alla verifica di sistemi reattivi richiede quindi un passo preliminare per modellare sia il sistema che la proprieta' considerata nel linguaggio accettato dal risolutore. Questa fase puo' richiedere l'intervento di astrazioni e analisi statica, aspetti che motivano il bisogno di conoscenza riguardo tecniche quali interpretazione astratta e sistemi di tipi. In tale ambito stuidieremo applicazioni innovative di risolutori per vincoli aritmetici lineari (su reali ed interi) per l'analisi statica di sistemi parametrici, SAT solvers per l'analisi di protocolli di comunicazione, risolutori di vincoli soft per l'analisi di sistemi con livelli multipli di priorita', e vincoli su insiemi per l'ottimizzazione di test di equivalenza e simulazione per sistemi conconrrenti.
III obiettivo
Il terzo obiettivo e' la combinazione di tecniche basate su constraint, model checking e interpretazione astratta ai fini della verifica. Questo e' un problema attualmente in fase embrionale ma di sicuro interesse. In questo contesto i risolutori di vincoli possono essere utilizzati come sottoprocedure all'interno di algoritmi di model checking basati su computazioni di punto fisso. L'interpretazione astratta ha qui numerose ed importanti applicazioni: fornisce tecniche per progettare in modo sistematico domini astratti di vincoli, metodi per valutare la qualita' delle corrispondenti approssimazioni, e operazioni per ottenere la terminazione dell'analisi (widening e narrowing). L'interpretazione astratta ha anche un ruolo importnate quale metodo per progettare procedure di raffinamento per il model checking. Risultati ``falsi negativi'' possono essere usati iterativamente per raffinare i modelli astratti fino a che o la proprieta' e' provata o un controesempio e' trovato. E' importante anche sviluppare risolutori di vincoli e librerie per trattare efficientemente i risultati intermedi dell'analisi. A questo fine studieremo nuovi risolutori specializzati per vincoli aritmetici e la loro combinazione con risolutori esistenti quali i SAT e risolutori BDD iin modo tale da ottenere strumenti di verifica per sistemi con dati eterogenei. Infine, esploreremo tecniche di model-checking esteso per sistemi temporizzati sviluppando una gia' consolodata connessione fra verifica e teoria degli automi e estendendo questo paradigma agli automi con vincoli.
IV obiettivo
Il quarto obiettivo consiste nell'applicazione in pratica dei sistemi di tipo alla verifica di sistemi reattivi. Tipi, tipi arricchiti e annotati sono metodi tradizionali di verifica statica di programmi. Recentemente i tipi sono stati usati per garantire proprieta' critiche dei sistemi reattivi quali sicurezza, accesso controllato alle risorse, assenza di garbage o deadlock. Nonostante queste applicazioni, l'uso in pratica dei sistemi di tipo e' piuttosto limitato dato che il type checking richiede una definizione ad hoc dei tipi che dipende fortemente dal tipo di proprieta' che si vuole verificare. Anche piccoli raffinamenti nella definizione di tale proprieta' possono implicare la necessita' di una ridefinizione completa del sistema di tipi. Per applicare quindi in pratica i sistemi di tipo alla verifica di sistemi reattivi, intendiamo identificare meccanismi di strutturazione che rendano i sistemi di tipo flessibili. Questo permetterebbe di definire strumenti di verifica che potrebbero essere applicati in modo parametrico. Piu' precisamente, la correttezza del sistema di tipi dovrebbe esser provata una sola volta, per una classe (anche infinita) di proprieta' interessanti. Quindi il sistema di tipi dovrebbe essere istanziato di volta in volta a seconda della proprieta' alla quale si e' interessati, ottenendo cosi' specifici e potenti sistemi di verifica. Questo obiettivo di ricerca si avvarra' anche di tecniche di intepretazione astratta e di rappresentazione mediante vincoli di proprieta'. Da tali settori ad esempio si potranno derivare costrutti di astrazione e rappresentazione per manipolare tipi parametrici e complessi.
V obiettivo
Il quinto obiettivo infine consiste nella realizzazione degli strumenti di verifica basati sulle tecniche studiate nel progetto. In questo senso intendiamo implemntare sia specifiche librerie di risolutori di vincoli che prototipi di strumenti di verifica da testare sui casi di studio considerati nel progetto.
Modelli di specifica
I modelli per la verifica di sistemi reattivi reali proposti recentemente
sono spesso basati su estensioni delle reti di Petri [BCR01,Del00,DR00,DRV01,EN98]
o sistemi di transizione etichettati [ACJT96,FS01]. Le reti di Petri tuttavia
possono essere usate soltanto per rappresentare astrazioni di protocolli nelle
quali i componenti interni abbiano una struttura semplice, data la natura
atomica dei ``tokens''. Anche i sistemi di transizione non costituiscono un
linguaggio di specifica ``user-friendly'', dato che non forniscono primitive
di alto livello per la strutturazione di una specifica.
Un diverso formalismo di specifica e' stato proposto nel conteso della
programmazione concorrente con vincoli [Sa89a,SRP91]. Questa fornisce un
modello computazionale concorrente nel quale le nozioni di sincronizzazione
e comunicazione possono essere espresse elegantemente in modo logico in termini
di implicazione e congiunzione. Recentemente i linguaggi sono stati proposti
i linguaggi ccp temporizzati [Sa89a,BGM00] quali estensioni di ccp adatte
per specificare sistemi reattivi e per modellare le loro proprieta' rilevanti.
Essendo basati su vincoli questi linguaggi concorrenti facilitano la specifica
e la verifica di sistemi complessi. Infatti, dato che i vincoli e le operazioni
di sincronizzazione e comunicazione possono essere espressi in termini logici,
e' possibile ottenere in modo relativamente semplice metodologie di verifica
[BGMP97] e di analisi [FGMP93].
Recentemente sono state studiate altre estensioni di ccp che permettono di esprimere algoritmi random (introducendo una estensione probabilistica degli usuali costrutti di ccp [GJS97,PW98]), di specificare sistemi ibridi (nei quali una parte dell'informazione e' continua) e di specificare sistemi distribuiti (usando opportune nozioni di store locali). Queste estensioni potrebbero essere utili nella specifica di sistemi reattivi complessi quali ad esempio quelli con componenti ibride.
Vincoli
L'idea alla base della programmazione con vincoli e' quella di sostituire la nozione classica di memoria (vista come valutazione) con una nozione che identifichi la memoria con un vincolo. Ad esempio, una relazione quale la legge di Ohm usando i vincoli puo' essere espressa direttamente come V = IxR, mentre in un linguaggio imperativi essa dovrebbe essere espressa indirettamente in termini di comandi che calcolano il valore di una variabile dato il valore delle altre due. Questo uso diretto delle relazioni come ``first class citizens'' nel modello computazionale permette un grande potere espressivo che semplifica la specifica di problemi complessi (ad esempio problemi combinatori). Inoltre esso permette di rappresentare finitamente in modo naturale un insieme di valori o di soluzioni infinito, fornendo cosi' un meccanismo di astrazione utile per la verifica di sistemi con infiniti stati possibili. Risolvere un problema di vincoli vuol dire trovare un assegnamento divalori alle variabili che soddisfa tutti i vincoli. I problemi di soddisfacimento di vincoli sono generalmente NP-hard, anche nel caso in cui le variabili del problema hanno un dominio finito. Quindi un qualunque algoritmo completo per trovare la loro soluzione sara' esponenziale nel caso pessimo. L'algoritmo completo piu' usato e' quello della ricerca con backtracking. Pero' ci sono tanti algoritmi incompleti, ma polinomiali, detti di propagazione di vincoli, che aiutano nella ricerca di una soluzione, rendendo meno costosa la ricerca con backtracking [T93,MS98].
I vincoli soft [BMR97-1,S95] sono un'estensione di quelli classici descritti sopra, detti anche vincoli hard. Ad ogni vincolo soft, o anche ad ogni tupla di valori per le variabili del vincolo, viene assegnato un elemento di un certo insieme, di solito ordinato. Ad esempio, i vincoli classici in questo formalismo sarebbero descritto scegliendo l'insieme {true, false}, e assegnando il valoro true alle tuple che soddisfano i vincoli, e false alle altre. I vincoli soft sono nati perche' ci si e' accorti che molti problemi reali non possono essere descritti fedelmente per mezzo di vincoli da soddisfare, poiche' hanno molte caratteristiche, come le probabilita', le incertezze, e i livelli di preferenza, che hanno bisogno di essere modellate. I vincoli soft permettono di modellarle.
Verifica basata sui Vincoli
Il paradigma Constraint-based Model Checking e' basato sulle seguenti idee. I vincoli vengono utilizzati come linguaggio asserzionale [KMMP97] per rappresentare collezioni infinite di configurazioni di un sistema concorrente. Le operazioni sui vincoli sono utilizzate quindi all'interno degli algoritmi basati su computazioni di punto fisso sui quali si basa il model checking. La tecnologia che supporta la tecnica di constraint-based symbolic model checking tuttavia e' ancora ad uno stadio molto preliminare. Infatti molti dei tool esistenti si basano sui `servizi' forniti da risolutori di vincoli general purpose. Ad esempio, Polka [HPR94] e HyTech [HHW97], due model checkers per sistemi ibridi, utilizzano la libreria per manipolare poliedri sviluppata da Halbwachs per l'analisi statica di programmi [CH78]. Il model checker di Bultan, Gerber and Pugh [BGP99] utilizza invece la libreria Omega, un risolutore per vincoli lineari aritmetici su interi (Presburger arithmetics). Recentemente, Bultan ha esteso questo tool con vincoli compositi, cioe' vincoli che combinano formule booleane e di Presburger [Bul00,DB01]. Infine McMillan sta sperimentando l'uso di SAT all'interno degli algoritmi di model checking simbolico [McM02]. Sfortunatamente, come provato sperimentalmente in [DR00,DRV01], un'integrazione troppo loose tra vincoli e model checking puo creare problemi quali l'esplosione degli stati simbolici dovuta alla dimensione dei vincoli rappresentanti risultati intermedi. Negli approcci ispirati a strutture dati quali OBBDs (una rappresentazione tramite diagrammi di decisione di formule booleane) utilizzati in Symbolic Model Checking questo problema e' stato affrontato solo per classi molto ristrette di vincoli aritmetici. Le strutture dati proposote in questo ambito sono: DDDs [MLAH99], una rappresentazione di difference constraints (vincoli utilizzati per modellare ed analizzare sistemi real-time) che migliora le rappresentazioni basate su matrici proposte in letteratura; CSTs [DR00], una rappresentazione compatta di insiemi chiusi all'insu' di marcature di Reti di Petri ottenuta tramite grafi chiamati sharing trees; NDDs [WB00] una libreria per gestire Presburger arithmetics basata sulla teoria degli automi.
Un confronto completo tra queste strutture dati (es. performance su problemi codificabili nella classe intersezione) non e' ancora stato fatto. Inoltre, rimangono da studiare estensioni di tali strutture dati a vincoli aritmetici piu' espressivi, ed euristiche per rendere fattibile l'analisi di casi pratici tramite queste tecniche.
Verifica come Soddisfacibilita' di Vincoli A partire dal 1991 abbiamo assistito ad un notevole miglioramento delle prestazioni dei SAT solvers: il numero di variabili proposizionali per problemi risolvibili tramite SAT solvers e' cresciuto da 100 a 10.000 variabili proposizionali. Tale progresso e' dovuto a una serie di nuovi algoritmi, tecniche ed euristiche sviluppate negli ultimi anni. Sulla base di tali risultati, molti ricercatori hanno iniziato a codificare e studiare problemi reali tramite SAT con risultati molto promettenti in particolar modo per applicazioni a pianificazione e verifica automatica di sistemi hardware. In particolare il SAT-based Bounded Model Checking [BCCZ99] e' stato recentemente proposto come approccio complementare a symbolic model checking basato su OBDDs. I risultati sperimentali indicano che i SAT-based Bounded Model Checkers possono dare migliori risultati degli OBDD-based Model Checkers quando applicati alla verifica di sistemi hardware. In molte altre applicazioni di interesse pratico e' possibile formulare proprieta' funzionali come problemi di constraint solving e stabilire la validita' della proprieta' invocando direttamente il solver corrispondente. Ad esempio, questo approccio viene seguito per l'analisi statica di protocolli modellati tramite reti di Petri. In questo ambito il protocollo e la proprieta' vengono descritti tramite un sistema di disequazioni lineari con soluzioni intere [EM97,EM00]. Tale problema si puo' risolvere quindi tramite risolutori di vincoli aritmetici su interi, oppure applicando un'approssimazione da interi a reali, tramite risolutori di vincoli aritmetici lineari su reali. I risultato di un'analisi statica possono essere anche utilizzati per migliorare l'efficienza delle procedure di model checking, ad es. tagliando lo spazio di ricerca come suggerito in [DRV01,DRV02]. Un punto fondamentale per il successo degli approcci alla verifica basati su vincoli e' lo sviluppo di risolutori per frammenti decidibili di vincoli, la loro combinazione, e la loro estensione a frammenti piu ampi. Mentre lo sviluppo di un risolutore e' solitamente basato su tecniche ad hoc un approccio uniforme alla sintesi di procedure di decisione e' stato proposto in [ARR01,ARR02]. Il problema di costruire procedure di soddisfacibilita' e' stato lungamente studiato. Due possibili soluzioni sono state fornite da Nelson e Oppen [NO78] e da Shostak [Sh84]. [AR01] presenta un'approccio che estende una procedura di decisione per aritmetica di Presburger in modo da poter trattare alcune classi di vincoli non lineari, ampliando cosi' la gamma di applicazioni.
Interpretazione astratta
L'interpretazione astratta [CC77, CC79] è una ben nota tecnica per approssimare la semantica di sistemi di computazione, ampiamente usata per specificare e validare analisi statiche dei comportamenti run-time del software. L'idea di base è alquanto semplice. La semantica approssimata viene specificata come un'esecuzione non standard della semantica formale del sistema: i dati concreti sono rimpiazzati da opportune descrizioni simboliche che formano una struttura ordinata chiamata dominio astratto che codifica il processo di approssimazione, mentre il calcolo astratto viene eseguito mediante operatori astratti e tecniche di estrapolazione di punti fissi (come widening e narrowing). I domini astratti svolgono quindi un ruolo chiave nell'approssimazione mediante interpretazione astratta. Quindi, sono stati definiti vari operatori sistematici per aumentare la precisione, modularizzare e ridurre la complessità di un'interpretazione astratta attraverso raffinamenti, semplificazioni, composizioni e decomposizioni di domini astratti. Interpretazioni astratte, a diversi livelli di astrazione, possono essere composte, decomposte, raffinate e compresse in base alle necessità. Il raffinamento e la semplificazione di domini astratti sono i concetti chiave [FGR96, GR97]. Informalmente, un raffinamento è un operatore sistematico che accresce l'accuratezza dei domini astratti, mentre una semplificazione agisce dualmente come un operatore che riduce la precisione dei domini. Il prodotto ridotto [CC79], i completamenti relazionali di Moore, di Heyting, e basati sulla logica lineare [GR99, GRS98, GS98] sono esempi di raffinamenti. Il complemento [CFGPR97] e la minima base disgiuntiva [GR98] sono invece esempi di operatori di semplificazione. Si è inoltre studiata una struttura fondamentale comune per questi operatori sistematici su domini astratti, basata sul concetto di approssimazione completa. Si sono individuati degli algoritmi di punto fisso che rendono un'interpretazione astratta completa mediante minimi raffinamenti o semplificazioni dei domini astratti dell'interpretazione [GRS00]. Maggiori dettagli sulla completezza in interpretazione astratta sono forniti nella descrizione del programma di ricerca.
Abstract model checking
La metodologia per la verifica automatica di sistemi comunemente detta model checking è ben nota. Il model checking è usato con grande successo come strumento di supporto alla specifica in molte industrie hi-tech (AT&T, IBM, Microsoft, Philips, etc., per citarne alcune). Le idee di base della tecnica del model checking risalgono ai primi anni '80 [CE81, CES83, CES86, QS82]. Le intense ricerche nel settore del model checking hanno prodotto numerosi algoritmi efficienti che permettono di verificare in pratica importanti proprietà (e.g. le cosiddette proprietà di safety e liveness) di sistemi con un enorme numero di stati e di sistemi ad infiniti stati. Tuttavia, il model checking soffre ancora di due limitazioni fondamentali: (1) il problema dell'esplosione esponenziale dello spazio degli stati [CGJLV01], poichè il numero degli stati del sistema cresce esponenzialmente con il numero dei processi componenti e/o con il numero delle variabili di stato; (2) gli stati del sistema devono essere in numero finito. Sono stati proposti numerosi metodi per ovviare a questi problemi. Tra questi vi è la classe dei metodi basati su interpretazione astratta, che permettono di approssimare il sistema da verificare [CGL92, CGL94]. Tali metodi sono comunemente noti con il nome di abstract model checking. Per entrambi i problemi (1) e (2) l'idea è essenzialmente la stessa. La verifica della specifica di correttezza viene fatta su un'astrazione del modello del sistema, detta modello astratto, che conservativamente tralascia alcune delle proprietà del sistema. Quindi, nell'abstract model checking sostanzialmente si applica l'interpretazione astratta al modello del sistema da verificare: si considera uno spazio degli stati astratti, dove uno stato astratto approssima alcune delle proprietà di uno stato concreto del sistema, e ciò dà luogo ad un sistema di transizione tra stati astratti, i.e. a un modello astratto. La verifica è eseguita nel modello astratto, e un teorema di correttezza assicura che se una specifica è valida nel modello astratto allora essa è valida anche nel modello concreto. L'approccio dell'abstract model checking ha registrato numerosi successi e ha permesso di verificare sistemi con un incredibile numero di stati possibili (ad esempio, un circuito ALU con 10^1300 stati raggiungibili fu verificato già nei primi lavori [CGL94]), poichè opportune astrazioni possono portare a drastiche riduzioni della dimensione del modello da verificare. I fondamenti e i principi dell'abstract model checking sono stati studiati e migliorati in molti aspetti [CJLW99, DGG97, DW95, LGSBB95]: sono stati proposti numerosi approcci per definire lo spazio degli stati astratti che usano risultati standard della teoria generale dell'interpretazione astratta; si è studiato l'impatto dell'abstract model checking sui linguaggi temporali di specifica; sono stati proposti degli approcci di abstract model checking simbolico, ovvero l'interpretazione astratta è stata applicata a strutture dati come i BDDs. Tecniche di interpretazione astratta sono state inoltre applicate per ottenere risultati di decidibilità nel model checking di sistemi ad infiniti stati [BLO98, CDG01, DF95, DW95]. Anche in questo caso l'idea di base è la stessa: un modello ad infiniti stati è approssimato e quindi ridotto ad un modello astratto con un numero finito di stati. Una misura della precisione di un'astrazione in rapporto all'insieme delle formule che valgono in un modello astratto e' data dalla nozione di "controesempi spuri" [CGJLV00], ovvero di controesempi che non corrispondono a nessuna transizione reale del sistema concreto. In [GQ01], questa nozione e' stata ridotta ad una mancanza di completezza per la corrispondente astrazione rispetto alla relazione di transizione del sistema che deve essere verificato. Mentre queste nozioni sono ben chiare nei sistemi discreti, la loro estensione al caso di sistemi reattivi ibridi e' ancora un problema aperto. Questi sistemi si basano su un software che interagisce in modo continuo con un qualche ambiente, e tipicamente consistono di vari processi separati che comunicano per scambio di messaggi o condivisione di memoria. Una estesa letteratura e' nota sui metodi formali per la verifica di sistemi ibridi, probabilistici e in tempo reale [AD94,AKNPS00,HHW97,KNSS01,KNSS00b,PS95,YPD94]. Tuttavia, non si e' mai considerato le tecniche di interpretazione astratta al fine di gestire un numero infinito di stati derivanti dalla verifica di questi sistemi. Risultati recenti hanno dimostrato che l'interpretazione astratta puo' essere generalizzata all'approssimazione di semantiche probabilistiche [Mon00,Mon01,DPW00].
Tipi
I tipi sono usati tradizionalmente per l'analisi statica dei programmi, in particolare per verificare l'assenza di errori a run-time. In effetti il type checking puo' essere visto come una procedura di verifica incompleta ma efficace. Usi piu' recenti di sistemi di tipo considerano i tipi come specifiche complete dei programmi, al costo di una certa complicazione della loro sintassi e proof-theory. Per alcune applicazioni sono usati sistemi di tipo che usano meccanismi abbastanza complessi quali quelli basati sul polimorfismo, sui sottotipi e sui tipi di dato astratti. Tali sistemi sono stati usati con successo per verificare proprieta' critiche quali controlli di sicurezza, accesso controllato alle risorse, assenza di garbage o deadlocks. Questo spostamento di obiettivi nell'uso dei tipi apre un ampio settore di ricerca che consiste nella definizione di sistemi formali che permettano di individuare proprieta' di programmi che siano controllabili staticamente (mediante i tipi) in modo guidato dalla sintassi. Cosi', ad esempio, i tipi possono essere usati nella verifica del bytecode Java, mediante un sistema di che permette di controllare la correttezza delle chiamate disubroutine [SA98]. I tipi sono stati usati anche per analizzare la topologia delle comunicazioni in processi di ML concorrente [ANN99]. Sostituendo il meccanismo di type inference alla Hindley/Miller con inferenze di tipo di rango 2, quali quelle proposte in [Dam00], si ottengono inoltre meccanismi di analisi composizionale che non sono possibili con i sistemi alla Hindley/Miller. In una direzione diversa, vi e' gia' una qualche evidenza de fatto che la mobilita' di ambienti di computazione [CG00] possa essere controllata effettivamente mediante opportuni sistemi di tipo, come proposto in [CG99]. Gli agenti possono anche essere arricchiti con ``capabilities'' (ovvero operazioni che essi devono eseguire su specifiche locazioni) che possono poi essere controllate in modo da garantire l'integrita' dei dati. Ad esempio, si puo' controllare che solo gli agenti con i diritti corretti possano accedere a determinate risorse [DFPV00, HR98]. Anche proprieta' di sicurezza state analizzate mediante l'uso dei tipi, ad esempio in un sistema introdotto da [A99] nel contesto dello spi-calcolo (questa e' un'estensione del pi-calcolo [MPW92] con primitive di crittografia [AG99]).
Aspetti implementativi
Le librerie esistenti per la manipolazione di poliedri convessi soffrono
di alcune limitazioni che, in determinati contesti, rendono il loro utilizzo
problematico [Fu98, GJ00, Je02, LW97, Wi93]. Alcune librerie, non essendo
in grado di gestire numeri a precisione arbitraria, possono incorrere in errori
causati dall'overflow. Analogamente, le librerie che utilizzano l'aritmetica
a virgola mobile, possono incorrere in problemi di underflow e, più
in generale, in errori di arrotondamento che possono invalidare il risultato
finale. Molte librerie non forniscono alcun supporto per la gestione dei
poliedri topologicamente non chiusi, ovvero dei poliedri ottenibili mediante
l'aggiunta di vincoli di disuguaglianza stretta. Le poche librerie nelle
quali questa estensione è possibile in realtà non forniscono
un supporto completo, incorrendo in inefficienze evitabili e lasciando all'applicazione
utente il compito non banale di interpretare i risultati ottenuti. Tutto
questo in aggiunta a problemi di efficienza che limitano la loro applicabilità
[HPW01]. Uno degli aspetti importanti per l'analisi di complessità
è rappresentato dalla possibilità di risolvere, in modo completamente
automatico, sistemi di relazioni di ricorrenza. Esistono in letteratura tecniche
e programmi per la soluzione di ricorrenze [Ck77, Iv78] che però trattano
una casistica piuttosto limitata e presuppongono l'interazione con un operatore
umano. (Pacchetti commerciali come Mathematica e Maple, opportunamente guidati
da un operatore, sono in grado di manipolare e semplificare alcune espressioni
che rientrano nel dominio delle ricorrenze.)
DESCRIZIONE DEI TASK DEL PROGETTO
La nostra metodologia complessiva consiste nell'identificazione di vari esempi
di problemi di verifica che si hanno in applicazioni reali di sistemi reattivi.
Tali problemi serviranno come casi di studio su cui testare i modelli, gli
algoritmi e le tecniche che saranno sviluppate nel progetto. Per raggiungere
gli obiettivi descritti poc'anzi intendiamo strutturare il progetto nei seguenti
Task (fra parentesi il nome del leader e le unita' che partecipano ad ogni
task)
Task 0 : Casi di studio
Task 1: Modelli di specifica (Montanari; Bologna, Udine)
Task 2: Vincoli (Delzanno; Bologna, Genova, Parma, Padova)
Task 3: Intepretazione astratta (File'; Padova, Udine, Verona)
Task 4: Tipi (Laneve; Bologna, Udine)
Task 5: Implementazioni di strumenti e risolutori (Bagnara; Genova,
Padova, Parma)
L'intero progetto e' diviso in 3 fasi. La prima fase, della durata di 6 mesi, sara' rivolta principalmente ai task 0 e 1.In questa fase saranno definiti i casi di studio e saranno identificati gli opportuni formalismi di specifica. La fase 2, di 12 mesi sara' dedicata ai task 2, 3 e 4. In questa fase saranno definiti gli specifici risolutori di vincoli, algoritmi, domini astratti e tipi per la verifica di sistemi reattivi e ne sara' valutata la rilevanza. Infine, nella fase 3, di 6 mesi, ci concentreremo sulla implementazione degli strumenti di verifica. Queste indicazioni sono da considerarsi per l'attivita' principale del progetto: unita' specifiche infatti potranno lavorare per periodi piu' lunghi e/o diversi su uno specifici (sub-)task. Nel seguito forniremo un descrizione piu' dettagliata del progetto illustrando i vari task.
Task 0 (Casi di studio)
Task 1 (Modelli di specifica)
Task 2 (Constraint Systems)
L'obbiettivo principale del task "Sistemi di Vincoli" e' quello di studiare applicazioni innovative di sistemi di vincoli esistenti o di sistemi di vincoli specializzati (e quindi dei risolutori) alla verifica automatica di sistemi reattivi (protocolli di comunicazione, sistemi distribuiti, e concorrenti). L'applicazione di tecniche di programmazione con vincoli (constraint programming) alla verifica di sistemi informatici e di comunicazione e' senz'altro uno dei filoni piu' promettenti e attivi nell'aerea di computer aided verification (verificata automatica di sistemi). I constraints rappresentano un concetto unificante per modellare e supportare la verifica di sistemi complessi, possibilmente parametrici, sistemi con tipi di dato eterogenei, e con spazio degli stati di grandi dimensioni o addirittura infinito [BGP99,DP99,HHW97,LPY97]. Il concetto di `vincolo' permette di estendere in maniera naturale paradigmi quali model checking e analisi statica a sistemi con un numero potenzialmente infinito di stati. I vincoli permettono di fronteggiare in maniera efficace anche il problema della esplosione degli stati che si verifica spesso durante l'analisi di sistemi finiti (e.g. hardware) e che puo' rendere l'uso dei tool di verifica automatica non praticabile [Bul00]. Il lavoro di ricerca verra' condotto lungo le seguenti linee di attivita'.
Task 2.1 (Sistemi di vincoli specializzati alla verifica)
Le techniche di programmazione basate su vincoli trovano naturale applicazione nell'ambito del paradigma chiamato "Constraint-based Model Checking". In questo approccio la tecnologia standard in model checking basata su OBBDs (una rappresentazione simbolica di formule booleane) viene generalizzata e sostituita con un sistema di constraint che possa gestire dati eterogenei. Contrariamente all'uso diretto di un risolutore di vincoli, in questo ambito i vincoli vengono interpretati come rappresentazioni simboliche di insiemi (possibilmente infiniti) di configurazioni; il risolutore di vincoli viene utilizzato ad ogni passo di una computazione di punto fisso per simplificare risultati intermedi. Il nostro obbiettivo e' quello di definire strutture dati sullo stile dei diagrammi di decisione (OBDDs) per memorizzare in modo compatto vincoli numerici (ad es. intervalli, vincoli aritmetici lineari) da utilizzare in algoritmi di model checking simbolico. Il punto di partenza e' rappresentato dalle strutture dati basate su grafi proposte recentemente per manipolare difference constraints (DDDS) e insiemi chiusi all'insu' di ennuple di numeri interi (CSTs). Il nostro goal e' quello di allargare la classe di vincoli aritmetici che si possano rappresentare in modo efficiente tramite strutture basate su grafi. Inoltre si vuole studiare la loro combinazione con altri sistemi di vincoli usati in verifica quali SAT e OBDDs. Inoltre, considerando il fatto che l'analisi statica puo essere utilizzata per migliorare l'efficienza degli algoritmi di symbolic model checking (vedi [DRV01,DRV02]), si vuole studiare la possibile combinazione delle tecniche sviluppate in questo task con quelle studiate nel Task 2.2 e nei Task 3 e 4. Lo sviluppo di librerie software prototipali verra' coordinato con le attivita' del Task 5.
Task 2.2 (Innovative Use of Existing Constraint Systems)
In molti problemi di verifica di interesse per il progetto, le tecniche di risoluzione di vincoli possono essere applicate in modo diretto per ottenere procedure di verifica automatica. In questo ambito un problema di verifica viene rappresentato come un problema di soddisfacibilita' di vincoli in un sistema di vincoli prefissato e quindi risolto tramite il solver corrispondente. Questo approccio richiede un'analisi preliminare (possibilmente automatica) per rappresentare la proprieta' da verificare nel linguaggio di vincoli accettato dal solver. Questa fase puo' richiedere l'uso di tecniche di interpretazione astratta, si prevede quindi una stretta collaborazione con l'attivita' del task 3 "Interpretazione Astratta". A tale scopo durante il progetto studieremo le potenzialita' di risolutori di vincoli definiti su domini ricorrenti in informatica quali SAT solvers, risolutori specializzati per programmazione intera linerare, risolutori di vincoli su insiemi, e la nuova teoria dei vincoli soft.
Task 2.3 (Soft Constraints)
I vincoli soft [BMR97-1,S95] sono nati perche' ci si e' accorti che molti problemi reali non possono essere descritti fedelmente per mezzo di vincoli da soddisfare, poiche' hanno molte caratteristiche, come le probabilita', le incertezze, e i livelli di preferenza, che hanno bisogno di essere modellate. I vincoli soft permettono di modellarle. I vincoli soft [BMR97-1,S95] sono un'estensione di quelli classici descritti sopra, detti anche vincoli hard. Ad ogni vincolo soft, o anche ad ogni tupla di valori per le variabili del vincolo, viene assegnato un elemento di un certo insieme, di solito ordinato. Ad esempio, i vincoli classici in questo formalismo sarebbero descritto scegliendo l'insieme {true, false}, e assegnando il valoro true alle tuple che soddisfano i vincoli, e false alle altre. In tale ambito l'obbiettivo e' quello di studiare l'applicabilita' di risolutori di vincoli soft a proprieta' di sicurezza per sistemi distribuiti [BB01]. A tale scopo si prevede lo sviluppo di prototipi per risolutori di soft constraints e l'applicazione sperimentale alla specifica ed analisi di casi pratici.
Task 3 (Abstract Interpretation)
In questo task ci si propone di studiare come la metodologia dell'interpretazione astratta possa essere applicata a e interagire con la verifica automatica di sistemi reattivi discreti ed ibridi. In particolare, si vogliono studiare le connessioni e interazioni incrociate tra model checking e interpretazione astratta, quali, ad esempio, già si possono riscontrare nell'abstract model checking per la verifica di sistemi con un numero finito o infinito di stati.
Task 3.1 (Domini astratti)
L'interpretazione astratta è strettamente legata all'idea e alla nozione di dominio astratto di calcolo. In termini semplici, un dominio astratto è un'opportuna approssimazione di qualche effettivo dominio di calcolo, detto dominio concreto, che consiste di rappresentazioni dei dati di qualche semantica formale di un sistema di computazione. Il dominio astratto fornisce una codifica delle proprietà semantiche del dominio concreto che devono essere conservativamente preservate dal processo di approssimazione. Il comportamento delle operazioni semantiche definite sul dominio concreto è simulato dalle cosiddette operazioni astratte, che sono appunto definite sui domini astratti e che calcolano astrattamente le proprietà semantiche approssimate codificate dai domini astratti. All'interno di questo sottotask, intendiamo concentrarci nelle due seguenti attività. (1) La prima idea è quella di definire dei domini astratti che consistono di vincoli astratti. Nel contesto della verifica dei sistemi sono già riportati dei risultati preliminari che scaturiscono da questa idea [BPR01, Del00, DB01, DP99, HPR97]. Questi lavori dimostrano che un tale approccio può fornire una soluzione effettiva al fenomeno dell'esplosione dello spazio degli stati. (2) In secondo luogo, intendiamo sfruttare l'idea dello sviluppo sistematico dei domini astratti nel contesto della verifica automatica dei sistemi. La teoria dello sviluppo sistematico dei domini astratti è ora matura e rappresenta uno dei principali vantaggi dell'interpretazione astratta rispetto ad altre tecniche di approssimazione ed analisi [CC79, CFGPR97, FGR96, GR97, GR99, GRS00]. La possibilità di modulare un'interpretazione astratta in precisione e costo è una caratteristica peculiare di questa teoria. Come già osservato nella base di partenza scientifica, sono stati definiti e studiati numerosi operatori sistematici che migliorano la precisione, riducono la complessità e modularizzano un'interpretazione astratta mediante raffinamenti, semplificazioni e decomposizioni dei sottostanti domini astratti. Si intende studiare l'impatto che queste metodologie possono avere nell'applicazione dell'interpretazione astratta alla verifica dei sistemi. In particolare, siamo interessati allo studio delle applicazioni a domini astratti che possono essere usati per l'abstract model checking, includendo informazione probabilistica e di tempo contiuno.
Task 3.2 (Progettazione sistematica di operatori di widening ed euristiche)
In questo campo siamo interessati nell'estendere le metodologie sistematiche conosciute in letteratura congiuntamente a quelle sviluppate nel sotto-task descritto sopra al fine di progettare domini astratti, al widening. Il widening e' una generalizzazione dell'interpretazione astratta basata su connessioni di Galois, che si focalizza sull'approssimazione dinamica di computazioni di punto fisso mentre queste vengono eseguite. La struttura debole delle operazioni di widening le rende estremamente generali e applicabili praticamente in tutti i casi in cui e' necessaria un'approssimazione del punto fisso. Gli operatori di widening sono particolarmente utili nella risoluzione di vincoli. Comunque, la generalita' di tali operatori e' anche un punto debole nel momento in cui si prova ad applicare metodi sofisticati per progettarli e valutarli sistematicamente (es. velocita' di convergenza, complessita' e accuratezza). Questo e' dovuto alla mancanza di una struttura matematica forte dietro gli operatori di widening. In questo progetto siamo interessati in widening con vincoli, i.e. widening che agiscono all'interno di uno specifico sistema di vincoli, e.g. quelli che risultano dall'astrazione di predicati [BPR01,BPR02], basati su un dato linguaggio logico fissato a priori. Noi siamo interessati nell'isolare questi linguaggi di vincoli che arricchiscono i widening della struttura appropriata ,in modo da introdurre metodi sistematici per il raffinamento, la semplificazione e il confronto, e.g. rispetto alla velocita' di convergenza, di widening. Particolarmente rilevante e innovativo e' lo studio di euristiche per guidare il widening verso un'approssimazione di punto fisso precisa (viz. completa). Questo corrisponde a raffinare widening, ovvero a migliorare la precisione nella computazione del punto fisso, guidando la strategia di widening mediante l'uso della semantica concreta. L'analogia di questo problema con il problema di rendere un dominio astratto completo [GRS00] e' un importante spunto per la ricerca futura nell'ambito di questo progetto.
Task 3.3 (Model checking astratto per sistemi discreti e ibridi)
La specifica di un sistema di abstract model checking è sempre accompagnata da un teorema di preservazione: se una formula è valida nel modello astratto allora essa è valida pure nel modello concreto. Teoremi di cosiddetta preservazione forte sono auspicabili: una formula di un opportuno linguaggio di specifica è valida nel modello astratto se e solamente se è valida nel modello concreto [CGL94, DGG97, LGSBB95]. Nella terminologia dell'interpretazione astratta, la preservazione forte corrisponde alla completezza del modello astratto. Gli aspetti di completezza in interpretazione astratta sono stati intensamente studiati da vari membri delle unità di ricerca del progetto, in particolare di Padova [GRS98, GRS00]. Si è osservato che la completezza per un'interpretazione astratta è una proprietà che non dipende dalle operazioni semantiche astratte ma che dipende solamente dai domini astratti sottostanti. Ciò pone il rilevante problema di rendere un'interpretazione astratta completa mediante minimi raffinamenti dei domini astratti. Si è dimostrato che questi minimi raffinamenti esistono e possono essere costruttivamente caratterizzati come soluzioni di punto fisso di equazioni tra domini astratti. Il principale obiettivo di questa attività consiste nell'ottenere dei risultati simili che permettano di rendere un abstract model checking completo. A questo scopo ci si propone di studiare le possibili applicazioni dei risultati esistenti per generiche interpretazioni astratte nel contesto dell'abstract model checking di sistemi discreti. Si mira quindi a sviluppare una adeguata teoria della completezza per l'abstract model checking. In particolare, prevediamo di studiare come la proprietà di preservazione forte possa essere vista e formalizzata come una proprietà di completezza per interpretazioni astratte opportunamente definite, una proprietà che non dipenda dalle transizioni tra stati astratti ma solamente dallo spazio degli stati astratti. Inoltre, intendiamo affrontare il problema del minimo raffinamento (e, dualmente, minima riduzione) dello spazio degli stati astratti che induce un modello astratto completo, con l'obiettivo di ottenere dei risultati costruttivi di esistenza, eventualmente considerando delle opportune restrizioni del linguaggio temporale di specifica. Recentemente, alcuni autori [CGJLV00, GQ01] hanno individuato e affrontato problemi simili: i risultati preliminari ottenuti sono molto promettenti e stimolano a proseguire lungo questa direzione di ricerca.
Task 4 Sistemi di tipi
In questo task considereremo l'applicazione in pratica dei tipi alla veirfica di sistemi reattivi.
Task 4.1 (Sistemi flessibili di tipi)
Come primo obiettivo identificheremo concetti di strutturazione che possano rendere i sistemi di tipo abbastanza flessibili da essere applicabili ad una ampia varieta' dei modello studiati nel task 1. Difatti tipi, tipi arricchiti e annotati sono metodi tradizionali di verifica statica di programmi. Recentemente i tipi sono stati usati per garantire proprieta' critiche dei sistemi reattivi quali sicurezza, accesso controllato alle risorse, assenza di garbage o deadlock. Nonostante queste applicazioni, l'uso in pratica dei sistemi di tipo e' piuttosto limitato dato che il type checking richiede una definizione ad hoc dei tipi che dipende fortemente dal tipo di proprieta' che si vuole verificare. Anche piccoli raffinamenti nella definizione di tale proprieta' possono implicare la necessita' di una ridefinizione completa del sistema di tipi. Per applicare quindi in pratica i sistemi di tipo alla verifica di sistemi reattivi abbiamo bisogno di meccanismi di strutturazione che rendano i sistemi di tipo flessibili. Questo permetterebbe di definire strumenti di verifica che potrebbero essere applicati in modo parametrico. Piu' precisamente, la correttezza del sistema di tipi dovrebbe esser provata una sola volta, per una classe (anche infinita) di proprieta' interessanti. Quindi il sistema di tipi dovrebbe essere istanziato di volta in volta a seconda della proprieta' alla quale si e' interessati, ottenendo cosi' specifici e potenti sistemi di verifica. Questo obiettivo di ricerca si avvarra' anche dei risultati ottenuti nei task del progetto che si occupano di intepretazione astratta e di rappresentazione mediante vincoli di proprieta'. Da tali settori ad esempio si potranno derivare costrutti di astrazione e rappresentazione per manipolare tipi parametrici e complessi.
Task 4.2 (Procedure di Type checking per la verifica)
la seconda parte dell'attivita' del task sara' rivolta alla studio di procedure di type-checking. Queste saranno intyegrate con tecniche basate su interpretazione astratta e vincoli per la verifica di sistemi reattivi sviluppate da altre unita' del progetto.
Task 5 (Implementazioni di strumenti e risolutori)
In questo task costruiremo librerie software e prototipi per la verifica basati sulle tecniche sviluppate negli altri task. Studi preliminari su librerie di vincoli specializzate (per domini di applicazione molto ristretti [DRV01,DRV02]) e su librerie general purpose [PPL-USER-0-3]) condotti da alcuni dei membri del consorzio forniscono una alta confidenza nella possibiita' di completare la realizzazione dei prototipi software entro i limiti temporali del progetto.
Task 5.1 (Librerie prototipo di risolutori di vincoli per la verifica)
L'obiettivo di questo specifico task e' la realizzazione di prototipi di librerie basate su vincoli da essere usate come motore negli strumenti di verifica. In particolare ci proponiamo di realizzare un'implementazione completa e professionale di domini di poliedri convessi che non sia soggetta alle limitazioni presenti nelle librerie oggi disponibili. In particolare, vogliamo fornire un supporto completo alla definizione di poliedri non necessariamente chiusi (NNC), non solo da un punto di vista implementativo, ma anche per quanto concerne la completezza e l'intuitività dell'interfaccia funzionale. Per operare una svolta nel campo dell'analisi e della verifica di complessità, affronteremo il problema della risoluzione automatica di relazioni di ricorrenza per quanto possibile generali. Per le applicazioni di verifica ed analisi automatica, la soluzione approssimata che ci interessa è nella forma di una minorazione e di una maggiorazione esplicite per la soluzione, e non nella forma di un termine principale con un termine d'errore dal comportamento asintotico noto, ma del quale non sono date altre informazioni (concernenti, ad esempio, il segno). Realizzeremo una libreria per la manipolazione di poliedri convessi NNC con, tra le altre, le seguenti caratteristiche: utilizzo di aritmetica intera a precisione arbitraria; applicazione sistematica di tecniche di computazione incrementale e lazy al fine di limitare per quanto possibile i problemi di efficienza; totale robustezza rispetto al rilevamento di condizioni eccezionali, quali l'esaurirsi della memoria disponibile o lo scadere di timeout; interoperabilità con altri domini di vincoli come intervalli [CC76] e differenze vincolate [Ba87, Da87, Mi01]. Studieremo anche algoritmi ottimizzati per particolari classi di poliedri, comunemente utilizzate in numerosi campi applicativi, come la classe dei poliedri non negativi (ovvero, sottoinsiemi dello spazio vettoriale i cui elementi hanno tutte le coordinate non negative) e la classe dei ``poliedri'' che approssimano uno spazio di soluzioni discreto (come gli Z-polyhedra [An91]). Riguardo alla soluzione automatica di relazioni di ricorrenza, realizzeremo una libreria per la soluzione di sistemi di ricorrenze
Task 5.2 (Piattaforme per integrare tecnologie diverse)
L'interazione dell'attivita' dei vari task e la possibile combinazione di model-checking basato su vincoli con interpretazione astratta e type-checking e' la parte piu' stimolante di questo task. Specificatamente, il goal e' la costruzione di strumenti di verifica nei quali il potere del model-chcking basto su vincoli sia rafforzato dall'uso di analisi statica e di astrazione raffinate dinamicamente. In pratica intendiamo produrre dei prototipi che permettano di valutare questa integrazione su esempi pratici. Parte di queste tecniche saranno integrate nell librerie specializzate basate su vincoli. I case studies identificati nel task 0 saranno usati per il benchmark degli strumenti ottenuti.