Contenuto
Ti trovi in: HOME »Programmi, progetti e risultati »I progetti »PRIN - Programmi di ricerca di Rilevante Interesse Nazionale»Programma di ricerca»Unità di ricercaINIZIO_TESTO_DA_INDICIZZARE
UNITA' DI RICERCA
italiano
Bibliografia
ABO03P. Abdulla, A. Bouajjani, J. d'Orso
Deciding Monotonic Games.
CSL 2003: 1-14
ABJN99
P. A. Abdulla, A. Bouajjani, B. Jonsson, and M. Nilsson.
Handling Global Conditions in Parameterized System Verification.
CAV 99, 1999.
ACJT96
P. A. Abdulla, K. Cerans, B. Jonsson, and Y.-K. Tsay.
General Decidability Theorems for Infinite-state Systems.
LICS 96, 1996.
AJ03
P. Abdulla, B. Jonsson
Model checking of systems with many identical timed processes.
TCS 290(1): 241-264,2003
ACH+95
R. Alur, C. Courcoubetis, T. A. Henzinger, N. Halbwachs,
P. Ho, X. Nicollin, A. Olivero, J. Sifakis, and S. Yovine.
The algorithmic analysis of hybrid systems.
TCS 138:3-34, 1995.
AD94
R. Alur and D.L. Dill.
A theory of timed automata.
TCS 126:183-235, 1994.
AH92
R. Alur and T. A. Henzinger.
Logics and models of real time: a survey.
Real Time: Theory in Practice, 1992.
AHK02
R. Alur, T. A. Henzinger, and O. Kupferman
Alternating-time Temporal Logic
J. ACM 49:672-713, 2002.
AJ98
P. A. Abdulla and B. Jonsson.
Verifying Networks of Timed Processes.
TACAS 98, 1998.
BLP+99
G. Behrmann, K. G. Larsen, J. Pearson, C. Weise, and W. Yi.
Efficient Timed Reachability Analysis Using Clock
Difference Diagrams.
CAV 99, 1999.
BM99
A. Bouajjani and R. Mayr.
Model Checking Lossy Vector Addition Systems.
STACS 99, 1999.
Bry86
R. E. Bryant.
Graph-based Algorithms for Boolean Function Manipulation.
IEEE Transaction on Computers, C-35(8):667-691, 1986.
BXS04
T. Bultan, X. Fu, J. Su.
Tools for Automated Verification of Web Services.
ATVA 2004: 8-10
BCB+90
J. R. Burch, E. M. Clarke, K. L. McMillan, D. L. Dill,
and J. Hwang.
Symbolic Model Checking: States and Beyond.
LICS 90, 1990.
BCL91
J. R. Burch, E. M. Clarke, and D. E. Long.
Symbolic Model Checking with partitioned transition relations.
VLSI 91, 1991.
BGP99
T. Bultan, R. Gerber, and W. Pugh.
Model-checking concurrent systems with unbounded
integer variables: Symbolic representations, approximations,
and experimental results.
ACM TOPLAS, 21(4):747--789, 1999.
CE81
E. M. Clarke and E. A. Emerson.
Synthesis of synchronization skeletons for branching
time temporal logic.
Ws.Logic of Programs, 1981.
CES86
E. M. Clarke and E. A. Emerson and A. P. Sistla.
Automatic verification of finite-state concurrent
systems using temporal logic specifications.
TOPLAS, 8(2):244- 263, 1986.
CDL+99
I. Cervesato, N. Durgin, P. Lincoln, J. Mitchell, and A. Scedrov.
A Meta-Notation for Protocol Analysis.
CSFW 99, 1999.
CGL94
E. Clarke, O. Grumberg and D. Long.
Verification tools for finite-state concurrent systems.
A Decade of concurrency-Reflections and Perspectives.
LNCS 803, 1994.
CGH+93
E. M. Clarke, O. Grumberg, H. Hiraishi, S. Jha,
D.E. Long, K.L. McMillan, and L.A. Ness.
Verification of the Futurebus+cache coherence protocol.
CHDLA '93, 1993.
CLM89
E.M. Clarke, D. E. Long, K. L. McMillan.
Compositional Model Checking.
LICS 89, 1989
CR97
G. Costa, G. Reggio
Specification of Abstract Dynamic-Data Types:
A Temporal Logic Approach.
TCS 173(2): 513-554 (1997)
CS84
G. Costa, C. Stirling
A Fair Calculus of Communicating Systems.
Acta Inf. 21: 417-441 (1984)
DEP99
G. Delzanno, J. Esparza, and A. Podelski.
Constraint-based Analysis of Broadcast Protocols.
CSL 99, 1999.
DP99
G. Delzanno, A. Podelski.
Model Checking in CLP.
TACAS 99, 1999.
Del00
G. Delzanno.
Automatic Verification of Parameterized Cache Coherence Protocols.
CAV 00, 2000.
Del00b
G. Delzanno.
Verification of Consistency Protocols via Infinite-State
Symbolic Model Checking - A Case Study -
Forte/PSTV 00, 2000.
DR00
G. Delzanno and J. F. Raskin.
Symbolic Representation of Upward-Closed Sets.
TACAS 00, 2000.
Del01
G. Delzanno.
An assertional language for systems parametric in
several dimensions (Preliminary results).
VEPAS 01, 2001.
DRV01
G. Delzanno, J.-F. Raskin, and L. Van Begin.
Attacking Symbolic State Explosion.
CAV 01, 2001.
DB01
G. Delzanno and T. Bultan.
Constraint-based Verification of Client-Server Protocols.
CP 01, 2001.
BD02
M. Bozzano, G. Delzanno.
Algorithmic Verification of Invalidation-Based Protocols.
CAV 02: 295-308
Del02
G. Delzanno.
Constraint-Based Model Checking for
Parameterized Synchronous Systems.
FroCos 02: 72-86
BD02
M. Bozzano, G. Delzanno.
Beyond Parameterized Verification.
TACAS 02: 221-235
Del02
G. Delzanno: An Overview of MSR(C): A CLP-based Framework
for the Symbolic Verification of Parameterized Concurrent
Systems.
ENTCS 76: (2002)
Del03
G. Delzanno
Constraint-Based Verification of Parameterized
Cache Coherence Protocols.
FMSD 23(3): 257-301 (2003)
Del04
G. Delzanno: A Symbolic Procedure for Control Reachability in
the Asynchronous Pi-calculus: Extended Abstract.
ENTCS 98: 21-33 (2004)
Hen96
T. A. Henzinger.
The theory of hybrid automata.
LICS 96, 1996.
HHM+00
T. A. Henzinger, B. Horowitz, R. Majumdar, and H. Wong-Toi.
Beyond HyTech: Hybrid System Analysis Using Interval
Numerical Methods.
HSCC 00, 2000.
HHW97
T. A. Henzinger, P.-H. Ho, and H. Wong-Toi.
HYTECH: a Model Checker for Hybrid Systems.
CAV 97, 1997.
HM00
T. A. Henzinger, R. Majumdar.
Symbolic Model Checking for Rectangular Hybrid Systems.
TACAS 2000, 2000.
HNSY94
T. A. Henzinger, X. Nicollin, J. Sifakis, and S. Yovine.
Symbolic model checking for real-time systems.
Information and Computation 111:193-244, 1994.
Hull04
Web Services Composition: A Story of Models, Automata, and
Logics, a tutorial for the 2004 EDBT Summer School.
http://edbtss04.dia.uniroma3.it/Hull.pdf
KMMPS01
Y. Kesten, O. Maler, M. Marcus, A. Pnueli, E. Shahar
Symbolic model checking with rich assertional languages.
TCS 256(1-2): 93-112 (2001)
LPY95
K. G. Larsen, P. Pettersson and W. Yi.
Diagnostic Model-Checking for Real-Time Systems.
DIMACS Ws VCHS 95, 1995.
LPY97
K. G. Larsen, P. Pettersson, and W. Yi.
UPPAAL in a Nutshell.
STTT, 1(1-2):134-152, 1997.
MCJ97
W. Marrero, E. M. Clarke, and S. Jha.
Model Checking for Security Protocols.
Technical Report CMU-SCS-97-139,
CMU, 1997.
McM93
K. L. McMillan.
Symbolic Model Checking: An Approach to the State
Explosion Problem.
Kluwer Academic, 1993.
Pnu81
A. Pnueli.
A temporal logic of concurrent programs.
TCS 13:45-60, 1981.
RKS+00
A. Roychoudhury, K.N. Kumar, C.R. Ramakrishnan,
I.V. Ramakrishnan and S. A. Smolka.
Verification of Parameterized Systems Using
Logic-Program Transformations.
TACAS 2000, 2000.
Yov97
S. Yovine.
Kronos: A verification tool for real-time systems.
STTT, 1(1-2), 1997.
Web
Web Services Activity: http://www.w3.org/2002/ws/
Programma di ricerca
Vincoli e preferenze come formalismo unificante per l'analisi di sistemi informatici e la soluzione di problemi realiUniversità di riferimento
Università degli Studi di GENOVA - INFORMATICA E SCIENZE DELL'INFORMAZIONE - GENOVA(GE)Responsabile dell'Unità di ricerca
Giorgio DELZANNODescrizione
Descrizione dell'unita'L'unita' e' formata da specialisti in applicazione di vincoli
a problemi di concorrenza (Delzanno) e in teoria della concorrenza e logiche temporali (Costa). Inoltre consta di 4 dottorandi:
Montagna e' attualmente impegnato in ricerca su estensioni di logiche temporali basate su giochi, Cordi' su sistemi multi-agente, Ganty e Mantovani su analisi di sistemi basata su risolutori di vincoli proposizionali.
La ricerca verra' svolta sia in collaborazione con altre unita' del progetto che con membri del DISI che del DIST (Dip. di Informatica Sistemistica e Telematica dell'Univ. di Genova) che non hanno potuto partecipare formalmente a questo progetto essendo impegnati in progetti PRIN partiti nel 2005.
Inoltre si prevede un assegno di un anno per un giovane ricercatore.
Descrizione del programma di ricerca
La ricerca è mirata all'utilizzo di linguaggi e sistemi di programmazione con vincoli per la modellazione e l'analisi di sistemi concorrenti con spazio degli stati infinito.
La metodologia che verra' seguita si basa su un paradigma nel quale i vincoli sono usati come modello intermedio per rappresentare problemi di analisi di diversi tipi di sistemi concorrenti. Il vantaggio di tale rappresentazione consiste nel poter utilizzare tecniche di risoluzione (eventualmente approssimata) di vincoli per studiare i problemi definiti sui modelli di partenza.
Il paradigma risultante permette quindi di implementare un possibile trasferimento di tecnologia da sistemi con vincoli ad tool per l'analisi di sistemi concorrenti.
In lavoro precedenti sono stati utilizzati con successo diverse istanze di tale paradigma. Ad es. in [Del00,Del03] attraverso la codifica di modelli a macchine a stati in problemi di vincoli su interi e' stato possibile utilizzare tecniche di rilassamento dei vincoli lineari e risolutori di vincoli su reali per verificare in modo automatico proprieta' di mutua esclusione di protocolli di coerenze delle cache utilizzate in sistemi multiprocessore.
Partendo da questa idea, verranno affrontate le seguenti
tematiche di ricerca:
Tematica 1: Combinazione di Teorie
(Partecipanti: Delzanno - Cordi' - Montagna - Mantovani - Ganty)
Questa ricerca e' mirata all'estensione del paradigma illustrato precedentemente in modo da combinare tra loro diversi risolutori di vincoli (cioe' le relative procedure di decisione) per poter gestire sistemi concorrenti con strutture dati eterogenee. In questo senso sembra di particolare interesse lo studio della combinazione di linguaggi per vincoli (ad es. vincoli lineari) e linguaggi logici basati su multiset rewriting. Le logiche basate su multiset rewriting sono particolarmente adatte infatti per modellare processi concorrenti [Del01,BD02]. Ad es. la regola
send(m) | rec(m) --> end1 | end2
dove | e' un costruttore di multinsiemi modella in modo naturale l'interazione tra un processo che invia un messaggio "m" e un processo pronto a ricevere "m", che porta alla terminazione di entrambi. La combinazione con vincoli permette di esprimere in modo naturale condizioni sui dati utilizzati dai processi.
Ad es. la regola
send(x) | rec(y) --> end1 | end2 : x>y
introduce condizioni sui dati (in questo caso un vincolo aritmetico) come guardia per la sincronizzazione dei processi.
In questa tematica i sotto-obbiettivi sono:
1.1) Studiare l'espressivita' di linguaggi risultanti
da diverse combinazione di multiset rewriting e vincoli.
1.2) Studiare tecniche di analisi basate su risolutori di vincoli
per linguaggi che combinano multiset rewriting e vincoli
1.3) Studiare codifiche di diversi modelli e linguaggi per
la concorrenza (con particpolare interesse per sistemi
mobili e multi agente) in multiset rewriting con vincoli.
Tematica 2: Vincoli per Analisi Composizionale
(Delzanno - Ganty - Mantovani)
Un aspetto interessante per quanto riguarda la ricerca nel campo della
verifica di sistemi concorrenti riguarda lo sviluppo di tecniche di prova composizionali. In questo ambito l'obbiettivo e' di raffinare
il paradigma illustrato precedentemente in modo da rendere composizionale sia la codifica dei sistemi e problemi iniziali che la fase di analisi. In particolare la ricerca sara' focalizzata sui seguenti punti:
2.1) Codifica composizionale
Partendo da problemi di verifica per modelli definiti
tramite operatori di composizione (ad es. process algebra)
si vogliono studiare codifiche in problemi di vincoli che
siano a loro volta definite in modo composizionale.
2.2) Analisi composizionale
Partendo dai vincoli risultanti da codifiche che soddisfano
i requisiti del punto (2.1) si vogliono studiare sistemi di
prova (semi) automatici basati sui sottostanti risolutori
di vincoli per poter realizzare tool di analisi composizionale.
Tematica 3: Vincoli per Logiche basate sui Giochi
(Delzanno - Montagna - Costa)
La tecnica di model checking e' stata recentemente estesa con alcune nozioni provenienti dalla teoria dei giochi per poter modellare proprieta' di sistemi che interagiscono con l'ambiente, ad es. la logica ATL [AHK02]. In queste logiche si possono esprimere proprieta' legate alla cooperazione di agenti. Sulla base di risultati recenti [ABO03, in questa tematica la ricerca sara' focalizzata sui seguenti punti:
3.1) Studio dell'estensione di logiche come ATL per
modellazione di sistemi con spazio degli stati infinito
3.2) Studio di tecniche simboliche basate su vincoli per
il model checking di logiche basate sui giochi
Tematica 4: Applicazioni
(Tutta l'unita')
Il target della ricerca proposta nelle 3 tematiche precedenti e' l'applicazione della combinazione di tecniche basate su vincoli e multiset rewriting, su composizionalita' e su possibile estensioni del linguaggio di specifica per le proprieta' tramite logiche basate sui giochi all'analisi di sistemi con spazio degli stati infinito.
In particolare utilizzeremo come casi di studio i protocolli utilizzati per i web services [BXS04, Hull04,Web]. Questo tipo di applicazioni presenta caratteristiche quali concorrenza e distribuzione, mobilita' del codice, e presenza di sessioni multiple che rendono l'analisi
un problema interessante per l'applicazione di nuove tecnologie.
Descrizione dei compiti e collaborazioni con altre unita'
Il primo anno verranno affrontati i punti 1.1-2, 2.1, 3.1.
Il secondo anno verranno affrontati i punti 1.3, 2.2 e 3.2.
La tematica 4 verra' studiata nel corso di tutti e due gli anni
(come spunto concreto per studiare modelli e problemi di analisi).
Le tematiche 1 e 2 verranno studiate in collaborazione con l'unita' di Pescara con punti di contatto con l'unita' di Padova per lo studio di risolutori di vincoli. La tematica 3 verra' studiata in collaborazione con l'unita' di Udine.
