GABBRIELLI	MAURIZIO
(cognome)	(nome)
Università degli Studi di BOLOGNA	Facoltà di SCIENZE MATEMATICHE FISICHE e NATURALI
(università)	(facoltà)
INF/01	Dipartimento di SCIENZE DELL'INFORMAZIONE
(settore scient.discipl.)	(Dipartimento/Istituto)

gabbri@cs.unibo.it
(E-mail)

GABBRIELLI	MAURIZIO
(cognome)	(nome)

Professore ordinario	20/11/1960	GBBMRZ60S20D612L
(qualifica)	(data di nascita)	(codice di identificazione personale)

Università degli Studi di BOLOGNA	Facoltà di SCIENZE MATEMATICHE FISICHE e NATURALI
(università)	(facoltà)
INF/01	Dipartimento di SCIENZE DELL'INFORMAZIONE
(settore scient.discipl.)	(Dipartimento/Istituto)

051 2094510		gabbri@cs.unibo.it
(prefisso e telefono)	(numero fax)	(E-mail)

Testo italiano

Maurizio Gabbrielli e' professore straordinario di Informatica al Dipartimento di Scienze di Informazione dell'Universita' di Bologna. Ha conseguito il titolo di Dottore di ricerca in Informatica nel 1992 presso l'Universita' di Pisa. Dal 1993 al 1995 e' stato impiegato presso il CWI di Amsterdam come borsista e poi come ricercatore, dal 1995 al 1998 e' stato ricercatore presso l'Universita' di
Pisa e dal 1998 al 2001 e' stato professore associato presso l'Universita' di Udine. I suoi interessi di ricerca includono i metodi formali per la verifica e l'analisi, la programmazione con vincoli, la teoria della concorrenza ed i sistemni real-time. E' autore di piu' di 50 pubblicazioni su riviste e atti di congressi internazionali, e' stato membro del comitato di programma di numerose conferenze internazionali, e' stato conference chair di SAS/PLILP/ALP (Static Analysis Symposium) 1998 e program chair della conferenza ACM PPDP 2000 (Principles and Practice of Declarative Programming). E' attualmente membro del comitato esecutivo di ALP (Association for Logic Programming), membro dello Steering Committee di PPDP e membro del board di EAPLS (European Association for Programming Languages and Systems). Ha partecipato ai progetti ESPRIT INTEGRATION, PARFORCE, all' ESPRIT Working Group 23677 COTIC e a numerosi progetti italiani.

Testo inglese

Maurizio Gabbrielli is professor of computer science at the Department of Computer Science of the University of Bologna. He received his Phd. in Computer Science in 1992 from the University of Pisa. In 1993-95 he was employed at CWI (Amsterdam), from 1995 to 1998 he was assistant professor at the University of Pisa and from 1998 to 2001 he was associate professor at the University of Udine. His research interests include formal methods for program verification and analysis, constraint programming, concurrency theory and languages for real-time applications. He is author of more than 50 publications on international journals and conferencs, served as a program committee member of several international conferences, was conference chair of SAS/PLILP/ALP (Static Analysis Symposium) 1998 and program chair of the ACM conference PPDP 2000 (Principles and Practice of Declarative Programming). He is currently member of the executive committee of ALP (Association for Logic Programming), of the Steering Committee of PPDP, and of the EAPLS board (European Association for Programming Languages and Systems). He partecipated to the ESPIRT projects INTEGRATION, PARFORCE and to the ESPRIT Working Group 23677 COTIC and to several national projects.

1. DE BOER F., GABBRIELLI M., MEO C. (2002). Proving correctness of Timed Concurrent Constraint Programs. Foundations of Software Science and Computation Structures (FOSSACS). LNCS, Springer-Verlag.
2. ETALLE S., GABBRIELLI M., MEO C. (2001). Trasformation of CCP programs. ACM TRANSACTIONS ON PROGRAMMING LANGUAGES AND SYSTEMS.
3. DE BOER F., GABBRIELLI M., GABBRIELLI M. (2000). A Timed Concurrent Constraint Language. INFORMATION AND COMPUTATION. vol. 161.
4. F.S. DE BOER, GABBRIELLI M., E. MARCHIORI, C. PALAMIDESSI. (1997). Proving Concurrent Constraint Programs Correct. ACM TRANSACTIONS ON PROGRAMMING LANGUAGES AND SYSTEMS. vol. 19(5), pp. 685-725.
5. BOSSI A., GABBRIELLI M., LEVI G., MARTELLI M. (1994). The s-semantics approach: Theory and applications. JOURNAL OF LOGIC PROGRAMMING. vol. 19-20, pp. 149--197.

Nº	Cognome	Nome	Dipart./Istituto	Qualifica	Settore scient.	Mesi uomo
						2002	2003
Personale docente:
1	GABBRIELLI	MAURIZIO	SCIENZE DELL'INFORMAZIONE	Prof. ordinario	INF/01	11 (ore: 1507)	8 (ore: 1100)
2	CIANCARINI	PAOLO	SCIENZE DELL'INFORMAZIONE	Prof. ordinario	INF/01	4 (ore: 550)	5 (ore: 685)
3	LANEVE	COSIMO	SCIENZE DELL'INFORMAZIONE	Prof. associato	INF/01	3 (ore: 411)	8 (ore: 1100)
Altro personale:

1.7.2 Personale universitario di altre Università

Nº	Cognome	Nome	Università	Dipart./Istituto	Qualifica	Settore scient.	Mesi uomo
							2002	2003
Personale docente:
1	FANTECHI	ALESSANDRO	FIRENZE	SISTEMI E INFORMATICA	Prof. associato	ING-INF/05	3 (ore: 411)	4 (ore: 550)
2	MEO	MARIA CHIARA	CHIETI	SCIENZE	Prof. associato	INF/01	1 (ore: 137)	8 (ore: 1100)
Altro personale:

1.7.3 Titolari di assegni di ricerca

Nº	Cognome	Nome	Dipart./Istituto	Anno del titolo	Mesi uomo
					2002	2003
1	ROSSI	DAVIDE	Dip. SCIENZE DELL'INFORMAZIONE	2000	7 (ore: 959)	5 (ore: 685)
2	WISCHIK	LUCIAN JULIES	Dip. SCIENZE DELL'INFORMAZIONE	2002	10 (ore: 1375)	8 (ore: 1100)

1.7.4 Titolari di borse per Dottorati di Ricerca e ex L. 398/89 art.4 (post-dottorato e specializzazione)

Nº	Cognome	Nome	Dipart./Istituto	Anno del titolo	Mesi uomo

1.7.5 Personale a contratto da destinare a questo specifico programma

Nº	Qualifica	Costo previsto	Mesi uomo
1.	Assegnista di ricerca	15000	11  (ore: 1507)

1.7.6 Personale extrauniversitario dipendente da altri Enti

Nº	Cognome	Nome	Ente	Qualifica	Mesi uomo
1.	GNESI	STEFANIA	CNR	PRIMO RICERCATORE	4  (ore: 550)

Testo italiano

Modelli basati su linguaggi concorrenti con vincoli e tipi per la verifica di sistemi reattivi.

Testo inglese

Models based on concurrent constraint languages and types for the verification of Reactive Systems

Testo italiano
PROGRAMMAZIONE CONCORRENTE CON VINCOLI ; SISTEMI REATTIVI E TEMPORIZZATI ; TIPI ; INTERPRETAZIONE ASTRATTA

Testo inglese
CONCURRENT CONSTRAINT PROGRAMMING ; TIMED SYSTEMS ; TYPES ; ABSTRACT INTERPRETATION

Testo italiano

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, 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.
Un secondo strumento di verifica gia' usato anche nel campo dei sistemi reattivi e' costituito dai 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]).

Testo inglese

The models for the verification of (real) reactive-systems proposed in recent works are often based on extension of Petri Nets[BCR01,Del00,DR00,DRV01,EN98] and on labeled transitions systems [ACJT96,FS01] . Petri Nets however can only be used to represent abstractions of protocols in which individual components have simple internal structure, since tokens in Petri Net have no structure. Although more general, transition systems are not a user-friendly specification language since they do not provide high level primitives for structuring a specification. A different specification formalism has been proposed recently in the context of concurrent constraint programming (ccp)[Sa89a,SRP91]. This is a general concurrent computational model where the notions of synchronization and communication can be expressed in an elegant logical way in terms of entailment of constraints. Recently, timed concurrent constraint programming (ccp) languages [Sa89a,BGM00] have been proposed as an extension of ccp suitable to specify reactive and time-critical systems and to model their relevant properties. Being based on constraints, these concurrent languages facilitate the specification and verification of complex systems. In fact, the basic idea behind constraint programming is to replace the classical notion of ``store as valuation'' of the Von Neumann model with the ``store as constraint (or relation)'' one. For example, such a relation as, say, the Ohm's Law, can be expressed directly by using constraints as V = IxR rather than indirectly in terms of statements which compute a value for one of the variables given the values of the other two (as in imperative languages). This direct use of relations as ``first class citizens'' in the computational model allows a great expressive power which simplifies the specification of complex problems (e.g. combinatorial ones); moreover it allows a natural finite representation of infinite set of solutions for the problems at hand, thus providing an ``abstraction'' property useful for the verification of infinite state systems.
A second verification techinque for programming languages and also for reactive systems is based on types.
Types are a traditional tool for the static analysis of programs, in particular for checking the absence of run-time errors. Indeed, type checking can be seen as an incomplete, but efficient verification procedure for infinite-state automata. More recent uses of type systems look types as full-blown program specifications, at the cost of complicating their syntax and proof theory. Powerful type systems, relying on complex type mechanisms, such as polymorphism, subtyping, abstract data types, are used. For instance, types have been successfully used to enforce critical properties of reactive systems, such as security checks, controlled accesses to the resources, absence of garbage or deadlocks. This shift of emphasis opens up a wide field of investigation, that consists in setting up formal systems that establish (statically checkable) program properties through type checking, in a syntax-directed manner. Thus, types can be used for example in the verification of the Java virtual machine code (bytecode), in the form of a type system suitable to verify the correctness of subroutine calls [SA98]. Type and effect systems have been used for analying the communication topology of Concurrent ML processes [ANN99]. Replacing Hindley/Milner type inference with rank 2 intersection type inferences such as the one proposed in [Dam00] allows a compositional analysis which is not possible with the Hindley/Milner type system. In a different direction, there is evidence that mobility of computational ambients [CG00] can be controlled effectively via suitable types, as proposed by [CG99]. In addition, agents are endowed with capabilities (namely, operations to be performed by them at specific locations) that can be controlled in order to ensure data integrity (only agents with the correct rights can access to resources and data, see [DFPV00,HR98]). Secrecy properties have also been studied by means of types, for example in a system introduced by [A99] on top of the spi-calculus, an extension of Milner's pi-calculus [MPW92] with cryptographic primitives [AG99].

[AG99] Abadi, M., Gordon, A. A Calculus for Cryptographic Protocols: The
spi-calculus. Information and Computation, 148(1):1-70, 1999.
[ACJT96] P. A. Abdulla, K. Cerans, B. Jonsson, and Y.-K. Tsay.
General Decidability Theorems for Infinite-state Systems. In
Proc. LICS 96, 1996.
[ANN99] Amtoft T., NielsonF., and Nielson H. R.. Type and Effect
Systems: Behaviours for Concurrency. Imperial College Press, 1999.
[BCR01] T. Ball, S. Chaki, S. K. Rajamani. Parameterized
Verification of Multithreaded Software Libraries. In Proc.
TACAS'01, LNCS 2031, pages 158-173, 2001.
[BD02] M. Bozzano, and G. Delzanno Beyond Parameterized
Verification. In Proc. TACAS 2002, April 2002.
[BL00] G. Bigliardi and C. Laneve. A Type System for JVM Threads.
ACM Sigplan Workshop on Types in Compilation (TIC '00),
Montreal, September 2000.
[BGMP97] F.S. de Boer, M. Gabbrielli, E. Marchiori and C.
Palamidessi. Proving Concurrent Constraint Programs Correct.
Transactions on Programming Languages and Systems (TOPLAS),
19(5): 685-725. ACM Press, 1997.
[BGM00] F.S. de Boer, M. Gabbrielli and M.C. Meo. A Timed CCP
Language. Information and Computation, 161, 2000.
[BGM01time] F.S. de Boer, M. Gabbrielli and M.C. Meo. A Temporal
Logic for reasoning about Timed Concurrent Constraint Programs.
In Proc. TIME 01. IEEE Press, 2001.
[BGM00agp] F. S. de Boer, M. Gabbrielli, and M. C. Meo. A
Denotational Semantics for a Timed Linda Language.
In Proc. PPDP. ACM Press, 2001.
[BGM02] F.S. de Boer, M. Gabbrielli and M.C. Meo. Proving
Correctness of Timed Concurrent Constraint Programs. In Proc.
FOSSACS 02, LNCS. Springer-Verlag. To appear, 2002.
[CG99] Cardelli L., Gordon A. Types for Mobile Ambients, POPL '99, ACM 1999.
[CG00] Cardelli, L., Gordon, A. Mobile Ambients. TCS 240(1):177-213,
Elsevier 2000.
[cou96a] P. Cousot. Abstract interpretation. ACM Comp. Surv.,
28(2):324--328, 1996.
[CC00] P. Cousot and R. Cousot. Temporal abstract
interpretation. In Conference Record of the Twentyseventh Annual
ACM SIGPLAN-SIGACT Symposium on Principles of Programming
Languages, pages 12--25, Boston, Mass ., January 2000. ACM
Press, New York, NY.
[Dam00] Damiani F. Typing local definitions and conditional expressions
with rank 2 intersection. FOSSACS'00, LNCS 1784, 2000.
[DFGI01]N. De Francesco, A. Fantechi, S. Gnesi, P. Inverardi, "Finite
Approximations for Model Checking Non-finite-state Processes" , The
Computer Journal, vol 44 no 2, 2001.
[Del00] G. Delzanno. Automatic Verification of Parameterized
Cache Coherence Protocols. In Proceedings of the 12th
International Conference on Computer Aided Verification, CAV
2000, Lecture Notes in Computer Science, vol. 1855, pages
53--68, Springer 2000.
[DP99] G. Delzanno, and A. Podelski. Model Checking in CLP. In
Proceedings of the Fifth International Conference on Tools and
Algorithms for the Construction and Analysis of Systems, TACAS
'99, pages 223-239, Lecture Notes in Computer Science, vol.
1579, Springer, 1999.
[DR00] G. Delzanno, and J. F. Raskin. Symbolic Representation of
Upward-closed Sets. In Proceedings of the 6th International
Conference on Tools and Algorithms for Construction and Analysis
of Systems, TACAS 2000, Lecture Notes in Computer Science, vol.
1785, pages 426-440, Springer 2000.
[DRV01] G. Delzanno, J.-F. Raskin, and L. Van Begin. Attacking
Symbolic State Explosion. In Proceedings of the 13th
International Conference on Computer Aided Verification, CAV
2001, pages 298-310, Lecture Notes in Computer Science, vol.
2102, Springer, 2001.
DFPV00] De Nicola, R., Ferrari, G., Pugliese, R., Venneri, B. Types for
Access Control. TCS 240(1):215-254, Elsevier 2000.
[EN98] E. A. Emerson and K. S. Namjoshi. On Model Checking
for Non-deterministic Infinite-state Systems.
In Proc. LICS 98, 1998.
[FS01] A. Finkel and P. Schnoebelen. Well-Structured Transition
Systems Everywhere! Theoretical Computer Science,
256(1-2):63--92, 2001.
[ FPV00] M. Falaschi and A. Policriti and A. Villanueva.
Modeling Timed Concurrent systems in a Temporal Concurrent
Constraint language-I. In Proc. of AGP-2000, extended version to
appear in ENTCS.
[Ha87] D. Harel. Statecharts: A Visual Formalism for Complex
Systems. Science of Computer Programming 8, pages 231-274, 1987.
[HR95] M. Hennessy and T. Regan. A temporal process algebra. \it
Information and Computation, 117: 221-239, 1995.
[HR98] Hennessy, M., Riely, J. Resource Access Control in Systems of
Mobile Agents. Int. Workshop on High-Level Concurrent Languages,
ENTCS 16, Elsevier 1998.
[GBGM91] P. Le Guernic, M. Le Borgue, T. Gauthier, and C. Le Marie.
Programming real time applications with SIGNAL. In \it Special
issue on Another Look at Real-time Systems, Proceedings of the
IEEE, 1991.
[LevesonT93] N. G. Leveson and C. S. Turner. An investigation of
the Therac-25 accidents. IEEE Computer, 26(7):18--41, 1993.
[MPW92] Milner, R., Parrow, J., Walker, D. A calculus of mobile processes
I and II. Information and Computation, 100(1):1-77, 1992.
[JM94] J. Jaffar and M. J. Maher. Constraint logic programming:
A survey. Journal of Logic Programming, 19/20, pp. 503--581,
1994.
[MP91] Z. Manna and A. Pnueli. The temporal logic of reactive
systems. Springer-Verlag, 1991.
[Pnu81] A. Pnueli. A temporal logic of concurrent programs.
TCS, 13:45-60, 1981.
[Sa89a] V.A. Saraswat. Concurrent Constraint Programming
Languages. PhD thesis, Carnegie-Mellon University, January 1989.
Published by The MIT Press, 1991.
[SA98] R. Stata and M. Abadi, 1998: A type system for Java bytecode
subroutines, in Proceedings of the 25th PoPL, ACM, 1998, pp. 149-160.
[SJG96] V.A. Saraswat, R. Jagadeesan, and V. Gupta. Timed Default
Concurrent Constraint Programming. Journal of Symbolic
Computation, 22(5-6):475--520, 1996.
[SRP91] V.A. Saraswat, M. Rinard, and P. Panangaden. Semantics
foundations of Concurrent Constraint Programming. In Proc. of
POPL. ACM Press, 1991.
[Sm95] G. Smolka.The Definition of Kernel Oz. In A. Podelski
editor, Constraints: Basics and Trends, vol. 910 of LNCS, pages
251--292. Springer-Verlag, 1995.
[Yov97] S. Yovine. Kronos: A verification tool for real-time
systems. Journal of Software Tools for Technology Transfer,
1(1-2), 1997.
[BG9] G. Berry and G. Gonthier. The ESTEREL programming language:
Design, semantics and implementation. Science of Computer
Programming, 19(2):87-152, 1992.
[NV02] M. Nielsen and F.D. Valencia. The ntcc Calculus and its
applications. Draft, 2001.
[PV01] C. Palamidessi and F.D. Valencia. A Temporal Concurrent
Constraint Programming Calculus. In {\em Proc. CP 01}, LNCS
2239, pag. 302-316. Springer-Verlag, 2001.
[Va00] F.D. Valencia. Reactive Constraint Programming.
Brics Progress Report, June 2000.

Testo italiano

L' unita' di Bologna intende contribuire a tre obiettivi di questo programma di ricerca. Innanzitutto intendiamo identificare opportuni linguaggi di specifica basati su vincoli sia per la modellizzazione di sistemi reattivi che per l'implementazione di procedure di verifica. In questo area intendiamo quindi contribuire principalmente al task 1 in collaborazione con l'unita' di Udine, ma vi saranno anche contributi ai task 2 e 5 e quindi colaborazioni con le unita' di Genova e Parma. Inoltre studieremo l'applicazionie dei tipi alla verifica dei sistemi reattivi, contribuendo quindi al task 4. Infine intendiamo lavorare anche al task 3 in collaborazione con le unita' di Padova e Udine, in particolare studiando l'integrazione di interpretazione astratta e model checking. Dato che l'unita' di Bologna coordina il progetto, insieme all'attivita' di ricerca svolgeremo anche un'attivita' di coordinamento del lavoro svolto dalle altre unita' nei vari task. Nel seguito forniamo ulteriori dettagli sul nostro programma di ricerca.
Il nostro primo obiettivo consiste nell'identificazione di opportuni linguaggi di specifica basati su vincoli per la rappresentazione di classi eterogenee di sistemi reattivi e per la verifica di correttezza dei medesimi. Il concetto di vincolo e' basilare in questo contesto. Lavori recenti hanno gia' mostrato che vari protocolli e applicazioni software posono essere analizzati usando una tecnologia basata sui vincoli. Prendendo ispirazione da tali lavori intendiamo focalizzare la nostra attenzione sui sistemi reattivi e temporizzati quali quelli che si hanno nelle seguenti aree: sistemi aperti e distribuiti, transzioni web, commercio elettronico, protocolli di comunicazione, programmi multithreaded, micro-controller e protocolli di sincronizzazione. A partire da linguaggi con constraint esistenti [JM94,Sa89a,SJG96,SRP91] e recenti lavori sui sistemi parametrici [BD02], opportuni linguaggi con constraint sarannodefiniti per modellare in modo uniforme classi di sistemi reattivi quali quelli delle applicazioni menzionate poc'anzi. Opportuni meccanismi di astrazione e primitive di strutturazione saranno individuati a partire dai casi di studio per ottenere un linguaggio di specifica di facile uso pratico. In particolare, intendiamo usare i linguaggi concorrenti convincoli temporizzati per i seguenti motivi. Inannanzitutto, come accennato prima, l'uso dei vincoli facilita la modellizzazionedi sistemi complessi, incluso quelli time-critical, dato che i vincoli permettono di esprimere in modo dichiarativo relazioni complesse fra le variabili usate per modellare il sistema. Secondariamente l'astrazione dal ``flusso di controllo'' implicita in questi modelli computazionali facilita la transizione dalle specifiche ai programi e semplifica gli aspetti semantici. Di conseguenza in questi linguaggi la complessita' aggiuntiva indotta dagli aspetti di concorrenza e di tempo puo' essere trattata in modo piu' efficace. In terzo luogo, questi modelli facilitano il compito della verifica di correttezza dato che permettono una descrizione logica abbastanza immediata che e' utile per la definizione di strumenti di verifica [BGMP97,BGM01time,BGM00]. Infine la disponibilita' di varie versioni implementate di questi linguaggi (incluse alcune commerciali), di numerosi risolutori di vincoli e di strumenti di programmazione matematica semplifica considerevolmente la prototipazione e l'implementazione degli strumenti di verifica ottenuti (si veda ad esempio [DP99]). Questa attivita' sara' integrata e coordinata con lo studio di metodologie di verifica basate su vincoli fatto dalle altre unita' del progetto.
Il secondo obiettivo dell'unita' di Bologna e' l'applicazione in pratica di 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 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. Nell'unita' di Bologna infine intendiamo anche studiare procedure di type-checking per integrarle con tecniche basate su interpretazione astratta e vincoli per la verifica di automi a stati infiniti sviluppate da altre unita' del progetto.

Testo inglese

Given the different expertises present in the unit of Bologna, our overall goal in this project is threefold. We plan to
identify suitable constraint specification languages both for modeling (finite and infinite-state) reactive systems and for
implementing the verification procedures. In this sense, our main contribution will be given to task 1 in cooperation with the units of Udine, but we plan to cooperate also with the units in Genova and Parma on the tasks 2 and 5, respectively. We also plan to apply types to verification of reactive systems , thus contributing to task 4. Finally we plan to work also in task 3 on the integration of abstract interpretation and verification, in cooperation with the units of Padova and Verona.
Since the unit of Bologna is the coordinator of the project, together with the research activity this unit will carry out also a coordination work to support the activity of the other units in the various tasks involved in the project. Below we provide some more details on our research programme.
Our first objective is to identify suitable, constraint based, specification languages for representing heterogeneous classes of reactive systems and for verifying their correctness. The concept of constraint is central for this phase: Recent works have shown, in fact, that several interesting protocols and software applications can be analyzed using constraint-based technology. Inspired by these works, we will focus our attention on reactive and time-dependent systems arising in the following areas: open and distributed systems, web transactions, electronic commerce and communication protocols, multithreaded programs, micro-controller and process synchronization protocols. Starting from constraint-based logic languages [JM94,Sa89a,SJG96,SRP91] and recent works on parameterized systems [BD02], suitable constraint-based languages will be identified which allow to model in an uniform way classes of (finite and infinite-state) systems related to the practical examples considered. These example will be used also to identify suitable abstraction mechanisms and structuring primitives to be used in the specification language in order to obtain a simple specification formalism. In particular, we plan to use (suitable versions of) timed concurrent constraint languages for several reasons. Firstly, as previously mentioned, the use of constraint languages facilitates the modeling of complex systems, including time critical ones, since constraints can be used to express in a declarative way complex relations among system data variables. Furthermore, the abstraction from the ``flow of control'' inherent to these computational models facilitates the transition from specifications to programs and simplifies the semantic issues. Consequently in these languages the additional complexity induced by concurrency issues and timing constraints of various sorts can be singled out more clearly. Thirdly, these models also simplifies the task of program verification, since they admit a rather simple direct logic description which is very useful when considering logic-based verification methods [BGMP97,BGM01time,BGM00]. Finally, the availability of several implemented versions of constraint logic languages (including commercial ones), as well as of many constraint solvers and mathematical and integer programming tools, considerably simplifies the prototype implementation of validation tools (see for example [DP99]). This activity will be integrated and coordinated with the study of constraint-based verification methodology performed by other units in the project.
The second objective of the unit of Bologna is the application in practice of types to verification of reactive systems. Types, enhanced types with effect systems and annotated types are a traditional method for the static verification of programs. Recently they have been used to enforce critical properties of reactive 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 reactive 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 of infinite-state systems which provide the necessary abstraction and syntactic representation for complex and parametric types.
Finally, we also plan to study type checking procedures in order to integrate them with techniques developed for the verification of infinite-state automata, such as abstract interpretation and constraints, studied by other units.

Nº	Anno di acquisizione	Descrizione
		Testo italiano	Testo inglese

Attrezzatura I
Descrizione

valore presunto ( Euro)   percentuale di utilizzo per il programma

Attrezzatura II
Descrizione

valore presunto ( Euro)   percentuale di utilizzo per il programma

QUADRO RD

4.1.1 Altro

QUADRO RA

4.2.1 Altro

Firma ____________________________________________

(per la copia da depositare presso l'Ateneo e per l'assenso alla diffusione via Internet delle informazioni riguardanti i programmi finanziati; legge del 31.12.96 n° 675 sulla "Tutela dei dati personali")