|
CONTENTS
- Description of main objectives
- Full description (objectives/tasks/scientific base)
OBJECTIVES
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
OBBIETTIVI
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
|
