Restricted Access

Restricted Access



In this project we are interested in verification of complex reactive systems. These are ubiquitous computer systems which maintain an ongoing interaction with an external environment, responding with appropriate actions to the external stimuli, and which often perform critical activities such as controlling industrial plants, managing financial transactions, scheduling time-critical operations, running e-commerce and web applications. With the increase of the dependency of our society from computer applications and reactive systems their correct behavior is becoming more and more critical, however their verification is particularly difficult. Practical examples of reactive systems in fact often consists of several sub-components that interact with an environment. Furthermore, their specification may require heterogeneous data and may depend on parameters whose values cannot be fixed a priori. Also, in many cases the set of possible states is infinite. Any of these aspects represents a big obstacle for the applicability of the state-of-the-art verification technology. As an example, let us consider the well-known mutual exclusion protocol called Szymanski's Algorithm [Szy90]. Every process involved in the protocol stores its own identifier (an integer number), and uses a control location, and some Boolean variables. The behavior of every process is described via test and assignments defined over the data variables. A generic configuration of the system consists of K processes executing in parallel the same protocol. To validate the protocols using techniques like symbolic model checking we should fix a value for K, encode our model into quantified boolean formulas (e.g. encoding identifiers with Boolean variables), explore all possible executions using symbolic representations of the state space. While this method might work well for a small number of system components, it will not scale up for big values of K. Furthermore, though model checking can find potential bugs, it cannot prove the protocol correct for any possible value of K. Given the complexity and variety of aspects involved in verification problems like the one informally described above, it seems natural to look for new direction of research taking inspiration from notions and techniques coming from different fields of theoretical and applied computer science.

The scientific global goal of the project is to use the notion of `constraint', supported by abstract interpretation and type theory, as the unifying concept for the specification and automated verification of complex reactive systems. To pursue this goal, we envisage the following specific research objectives.

First Objective

Our first objective is to identify suitable constraint specification languages for modeling complex reactive systems, and for reasoning about their properties. The use of constraint-based languages facilitates the modeling of complex systems. The constraints can be used to express in a declarative way complex relation among system data variables. They also simplifies the task of reasoning about system properties, since they admit a rather simple direct logic description which is very useful when considering logic-based verification methods. Furthermore, the availability of several implemented versions of constraint logic languages, as well as of many constraint solvers for mathematical and symbolic domains, considerably simplifies the prototype implementation of validation tools. Our case-studies will be selected among classes of applications presenting difficult aspects for standard verification techniques, as the above described example. Specifically, we will consider case-studies coming from open and distributed systems, time-dependent systems, abstractions of multithreaded programs, Web transactions, and protocols for e-commerce.

Second Objective

Our second objective concerns the study of the foundations of constraint-based verification techniques. Specifically, we will investigate constraint solving as a tool for automated verification. The general goal of constraint solving is checking the satisfiability of a constraint formula via specialized and efficient solvers. The application of this paradigm to the verification of reactive systems requires a preliminary step for modeling the system and the property in the constraint language accepted by the solver. This step may require a preliminary abstraction and static analysis phase, thus motivating the need of combining expertise coming from abstract interpretation and type systems. In this setting we will investigate also innovative uses of existing constraint systems. Specifically, we will investigate the use of solvers for linear arithmetic constraints (over integers and reals) for static analysis of parameterized systems, SAT solvers for the analysis of communication protocols, solvers for soft constraints for the analysis of systems with multiple levels of priorities, and set constraints for optimizing equivalence tests for concurrent systems.

Third Objective

The third objective is the combination of constraints, model checking and abstract interpretation for verification purposes. This is a promising field which has received some attention only very recently. In this setting constraint solvers are used as sub-procedures of model checking algorithms based on fixpoint computations. Abstract interpretation finds here several important applications: it provides techniques to systematically design abstract constraint domains, methods to evaluate the quality of the resulting approximations, and operations to enforce the termination of the analysis (widening and narrowing). Abstract interpretation has also an important role as a method to design refinement procedures for model checking. `False negative' results can be used here to iteratively refine the abstract models analyzed via model checking until either the property is proved or a counterexample is found. It is also important to devise efficient constraint solvers and specialized libraries for handling efficiently the intermediate results of the analysis. For this purpose, we will study new specialized solvers for handling arithmetic constraints and their combination with existing solvers like BDDs and SAT solvers so as to obtain verification technology for systems with heterogeneous data. Finally, we will explore the extensions of model checking techniques to systems with time-dependent constraints by exploiting a consolidated connection between verification and automata theory and by investigating extensions of this paradigm to automata with constraints.

Fourth Objective

Our fourth objective is the application in practice of types to verification of reactive systems. Types and enhanced types with effect systems and annotated types, are a traditional method for the static verification of programs and recently they have been used to enforce critical properties of infinite-state systems, such as security checks, controlled accesses to the resources, absence of garbage or deadlocks. However, notwithstanding their applications, the practical use of types is rather limited since type checking requires an ad-hoc design of types, which strongly depends on the property one wants to verify. Therefore, even smooth refinements of the property may need a complete redesign of the type system. In order to apply in practice types to verification of infinite state systems, we plan to identify structuring concepts which could make type systems flexible. This could lead to verification procedures and tools which could be applied in a parametric way. More precisely, the correctness of the type system should be proved once and for all, for a possibly infinite class of properties one could be interested in. Then the type system can be instantiated, according to the particular set of properties one is interested into, thus getting ad-hoc powerful type systems. This objective will benefit from the research in abstract interpretation and constraint representation of properties, which provide the necessary abstraction and syntactic representation for complex and parametric types.

Fifth Objective

The fifth objective is finally the design of verification tools based on a combination of the techniques investigated in the project. We plan to implement both specific libraries for constrain solving and prototype verification tools to be tested on the case studies.

Torna al menu


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.

Torna al menu