Vai al contenuto| Home page|

   Ti trovi in: HOME »Programmi, progetti e risultati »I progetti »PRIN - Programmi di ricerca di Rilevante Interesse Nazionale»Programma di ricerca
INIZIO_TESTO_DA_INDICIZZARE

PROGRAMMA DI RICERCA 2005

italiano - english
Unità di Ricerca
Programmi di ricerca simili:
Classificazione scientifico-disciplinare
Classificazione brevettuale
Classificazione geografica
Bibliografia
[BBDS03] F. Barbanera, M.Bugliesi, M. Dezani, V. Sassone.
A Calculus of Bounded Capacities. LNCS 2896, 2003.

[BdL03] F. Barbanera, U. de' Liguoro.
Type Assignment for Mobile Objects. ENTCS 84, 2003.

[BC01] M. Bugliesi, G. Castagna. Secure Safe Ambients. POPL 2001.

[BCC01] M. Bugliesi, G. Castagna, S. Crafa.
Reasoning about security in mobile ambients.
CONCUR 2001, LNCS 2154, 2001.

[BCC04] M. Bugliesi, G. Castagna, S. Crafa.
Access Control for Mobile Agents: the Calculus of Boxed Ambients.
ACM TOPLAS, 26(1):57-124, 2004.

[BCG88] M.C. Browne, E.M. Clarke, O. Grumberg.
Characterizing finite Kripke structures in propositional temporal logic. TCS 59, 1,2, 1988.

[BCMS04] M. Bugliesi, S. Crafa, M. Merro, V. Sassone.
Communication and Mobility Control in Boxed Ambients.
I&C 2005. To appear.

[BCPS03] M. Bugliesi, S. Crafa, A. Prelic, V. Sassone.
Secrecy in Untrusted Networks. ICALP 2003, LNCS 2719, 2003.

[BDNN01] C. Bodei, P. Degano, F. Nielson, H. Riis Nielson.
Static analysis for the pi -calculus with applications to security.
I&C 168, 2001.

[CC01] L. Caires and L. Cardelli.
A Spatial Logic for Concurrency (Part I), TACS 2001, LNCS 2215, 2001.

[CD02] M. Coppo, M. Dezani.
A fully abstract model for higher-order mobile ambients.
LNCS 2294, 2002.

[CDGS03] M. Coppo, M. Dezani, E. Giovanetti, I. Salvo.
M3 Mobility Types for Mobile Processes in Mobile Ambients.
ENTCS 78, 2003.

[CDV03] T.Chothia, D.Duggan, J.Vitek.
Type-Based Distributed Access Control. CSFW-16 2003.

[CEI+05] A. Chander, D. Espinosa, N. Islam, P. Lee, G. Necula.
Enforcing Resource Bounds via Static Verification of Dynamic Checks.
ESOP'05, LNCS 3444, 2005.

[CG00] L. Cardelli, A. D. Gordon.
Anytime, Anywhere. Modal Logics for Mobile Ambients.
POPL'00. ACM Press, 2000.

[CG01] L. Cardelli and A. D. Gordon.
Logical Properties of Name Restriction.
TLCA'01, LNCS 2044, 2001.

[CGG00] L. Cardelli, G. Ghelli, A. D. Gordon.
Secrecy and Group Creation.
CONCUR'00, LNCS 1877, 2000.

[CGG02] L. Cardelli, G. Ghelli, A. D. Gordon.
Types for Mobile Ambients.
I&C, 186(2) 194-235 (2003).

[CGT02] W. Charatonik, A. D. Gordon, J-M. Talbot.
Finite-control mobile ambients. ESOP 2002, LNCS 2305, 2002.

[CGZ01] G. Castagna, G. Ghelli, F. Zappa Nardelli.
Typing Mobility in the Seal Calculus. CONCUR'01, LNCS 2154. 2001

[CMS05] G. Conforti, D. Macedonio, V. Sassone.
BiLogics: Spatial-Nominal Logics for Bigraphs. ICALP'05. To appear.

[CR05] S. Crafa and S. Rossi.
A Theory of Noninterference for the pi-calculus.
TGC'05, LNCS. To appear, 2005.

[CZ02] G. Castagna, F. Zappa Nardelli.
The Seal Calculus Revisited: Contextual Equivalence and Bisimilarity. FSTTCS'02, LNCS 2556, 2002.

[CW00] K. Crary, S. Weirich. Resource bound certification.
POPL'00. ACM Press, 2000.

[D96] M. Dam. Model Checking Mobile Processes.
I&C, 129(1), pp. 35-51, 1996.

[DDG99] F. Damiani, M. Dezani-Ciancaglini, P. Giannini.
A filter model for mobile processes. MSCS 9(1): 63-101 (1999)

[DeHe84] R. De Nicola, M. Hennessy.
Testing Equivalences for Processes. TCS 34, 1984.

[DFP98] R. De Nicola, G. L. Ferrari, R. Pugliese.
KLAIM: A Kernel Language for Agents Interaction and Mobility.
IEEE Transactions on Software Engineering, 1998, 24(5),315-330.

[DL04] R. De Nicola, M. Loreti. A Modal Logic for Mobile Agents.
ACM TOCL 5(1), 2004.

[DLB00] P.Degano, F.Levi, C.Bodei.
Safe Ambients: Control Flow Analysis and Security. LNCS 1961, 2002.

[DFPV00] R. De Nicola, G. Ferrari, R. Pugliese, B. Venneri.
Types for Access Control. TCS 240(1):215-254, 2000.

[DV95] R. De Nicola, F. Vaandrager.
Three logics for Branching Bisimulation. JACM, 42(2): 458-487, 1995.

[DS00] M. Dezani-Ciancaglini, I. Salvo.
Security Types for Mobile Safe Ambients. ASIAN'00, LNCS 1961, 2000.

[FGMP04] G. Ferrari, S. Gnesi, U. Montanari, M. Pistore.
A Model Checking Verification Environment for Mobile Processes.
ACM Tosem, 2004.

[GC99] A. Gordon, L. Cardelli.
Equational Properties of Mobile Ambients.
MSCS 12, 2002 (Also in FoSSaCs '99).

[GHS02] J.C. Godskesen, T. Hildebrandt, V. Sassone.
A Calculus of Mobile Resources. CONCUR'02, LNCS 2421, 2002.

[Gla93] R.J. van Glabbeek.
The linear time branching time spectrum (part II).
LNCS 715, 1993.

[HeLi95] M. Hennessy, H. Lin. Symbolic bisimulations. TCS 138, 1995.

[HeMi85] M. Hennessy, R. Milner.
Algebraic laws for nondeterminism and concurrency. JACM 32(1), 1985, 137-161.

[HH97] T. Hartonas, M. Hennessy.
Full Abstractness for a Functional/Concurrent Language with Higher-Order Value-Passing. I&C 145(1), 1998, 64-106.

[HJ03] M. Hofmann, S. Jost.
Static Prediction of Heap Space Usage for First-Order Functional Programs. POPL'03. ACM Press, 2003.

[HJNN99] R. R. Hansen, J. G. Jensen, F. Nielson, H. R. Nielson.
Abstract Interpretation of Mobile Ambients. SAS'99, LNCS 1694, 1999.

[HMR03] M. Hennessy, M. Merro, J. Rathke.
Towards a Behavioural Theory of Access and Mobility Control in Distributed System. TCS 322(3): 615-669, 2004.

[Hof02] M. Hofmann. The strength of non size-increasing computation.
POPL'02. ACM Press, 2002.

[HPJ02] Y. C. Hu, A. Perrig, D. Johnson.
Ariadne: A secure on-demand routing protocol for ad hoc networks. MobiCom 2002.

[HR02] M. Hennessy, J. Riely.
Resource Access Control in Systems of Mobile Agents. I&C 173, 2002, 82-120.

[HRY03] M. Hennessy, J. Rathke, N. Yoshida.
Safedpi: a language for controlling mobile code.
FOSSACS'03, LNCS 2620, 2003.

[IK02] A. Igarashi, N. Kobayashi. Resource usage analysis.
POPL 02. ACM Press, 2002.

[J02] D. B. Johnson, D. A. Maltz, Y.-C. Hu.
The dynamic source routing protocol for mobile ad-hoc networks (DSR). Internet draft, MANET working group, Feb. 2002.

[JM04] O. H. Jensen, R. Milner.
Bigraphs and mobile processes (revised).
Univ. of Cambridge, Tech. Report UCAM-CL-TR-580. Feb 2004.

[LS03] F. Levi, D. Sangiorgi.
Controlling Interference in Ambients.
ACM TOPLAS 25(1), 2003. Also in POPL'00.

[Mil89], R. Milner.
Communication and Concurrency. Prentice Hall, 1989.

[MPW93] R. Milner, J. Parrow, D. Walker.
Modal logics for mobile processes. TCS 114, 1993.

[MS02] M. Merro, V. Sassone.
Typing and Subtyping Mobility in Boxed Ambients.
CONCUR'02, LNCS 2421, 2002.

[Mye99] A.C. Myers.
Mostly-Static Decentralized Information Flow Control.
PhD thesis, TR MIT/LCS/TR-783. Jan. 1999.

[MZ03] M. Merro, F. Zappa Nardelli.
Bisimulation Proof Techniques for Mobile Ambients.
ICALP'03, LNCS 2719, 2003.

[MZ04] I. Margaria, M. Zacchi.
A Filter Model for Safe Ambients. ENTCS 2004.

[Pa81] D.M. Park.
Concurrency on Automata and Infinite Sequences.
LNCS 104, 1981.

[PiSa00] B. Pierce, D. Sangiorgi.
Behavioral Equivalence in the Polymorphic Pi-Calculus.
JACM, 47, 2000.

[PRD02] C. E. Perkins, E. M. Royer, S. R. Das.
Ad-hoc on-demand distance vector (AODV) routing.
IETF Internet draft, MANET working group, Jan.2002.

[PS96] B. Pierce and D. Sangiorgi.
Typing and Subtyping for Mobile Processes.
JMSCS, 6(5), 1996.

[S05] K. Sanzgiri, D. LaFlamme, B. Dahill, B. N. Levine, C. Shields, E. M. Belding-Royer.
Authenticated Routing for Ad Hoc Networks.
IEEE Journal on Selected Areas in communications, 23(3) March 2005.

[San01] D. Sangiorgi.
Extensionality and Intensionality of the Ambient Logic
POPL'01. ACM Press, 2001.

[San98] D. Sangiorgi.
On the bisimulation proof method. JMSCS 8, 1998.

[SW01] D. Sangiorgi, D. Walker.
The pi-calculus: a Theory of Mobile Processes.
Cambridge University Press, 2001.

[TZH02] D. Teller, P. Zimmer, D. Hirschkoff.
Using ambients to control resources. CONCUR'02, LNCS 2421, 2002.

[YH99] N. Yoshida, M. Hennessy.
Subtyping and locality in distributed higher order mobile processes.
CONCUR'99, LNCS 1664. 1999.

[W02] Joe Wells.
The essence of principal typings.
ICALP'02, LNCS 2380, 2002.
Parole Chiave
CALCOLI TIPATI PER CODICE MOBILE; EQUIVALENZE COMPORTAMENTALI; SISTEMI DI TRANSIZIONE ETICHETTATI; SISTEMI DI TIPO PER IL CONTROLLO DELLE RISORSE; LOGICHE TEMPORALI E SPAZIALI PER LA CONCORRENZA

Fondamenti Logici dei Sistemi Distribuiti e Codice Mobile

Università "Ca' Foscari" di Venezia
Abstract
Il moderno sviluppo di programmi software è sempre più spesso rivolto al servizio di applicazioni distribuite, situate a vari livelli di astrazione, da protocolli di comunicazione a livello IP per dispositivi mobili, come il protocollo IPv6, a transazioni commerciali e sistemi di commercio elettronico. Gli ambienti computazionali in cui questi programmi operano hanno una struttura inerentemente dinamica ed estensibile, sono caratterizzati dall'assenza di strutture di controllo centralizzate e sono costruiti a partire da reti fisiche e/o virtuali con una topologia complessa, connettività dinamica e servizi di entità e qualità variabile.

Il ruolo dei metodi formali di specifica, analisi e verifica del software è chiaramente critico in questo contesto in quanto, date le dimensioni delle applicazioni e la complessità dell'ambiente computazionale sottostante, lo sviluppo di software non può prescindere da una fase rigorosa di validazione prima che il software stesso venga posto in uso. Ciononostante, i metodi classici di specifica e le tecniche di analisi esistenti non sono efficaci in questi contesti. In primo luogo, l'assenza di controllo centralizzato, che distingue i sistemi aperti, invalida l'efficacia dei metodi di verifica correnti in quanto questi ultimi troppo spesso si basano sull'esistenza di assunzioni precise, ed affidabili, sulla struttura e sul comportamento di _tutte_ le componenti del >>>

Coordinatore Scientifico del Programma di Ricerca
Michele BUGLIESI Università "Cà Foscari" di VENEZIA
Obiettivo del Programma di Ricerca
L'esecuzione remota è un paradigma classico della ricerca sui sistemi distribuiti, che mira a sviluppare tecniche per supportare la condivisione del potere computazionale tra macchine allocate su diversi nodi di una rete, e/o dispositivi mobili. I progressi recenti nella tecnologia delle comunicazioni hanno creato rinnovato interesse e nuovi problemi per questo paradigma di programmazione.

Il moderno sviluppo di programmi software è sempre più spesso rivolto al servizio di applicazioni distribuite, situate a vari livelli di astrazione, da protocolli di comunicazione a livello IP per dispositivi mobili, come il protocollo IPv6, a transazioni commerciali e sistemi di commercio elettronico. Gli ambienti computazionali in cui questi programmi operano sono costruiti a partire da reti fisiche e/o virtuali con una struttura complessa, connettività dinamica e servizi di entità e qualità variabile. Inoltre, a tutti i livelli di astrazione, tali ambienti hanno una struttura inerentemente dinamica ed estensibile, sono caratterizzati dall'assenza di strutture centralizzate di controllo, di gestione di trust e di autorizzazione.

Il ruolo dei metodi formali di specifica ed analisi del software è indiscutibile: date le dimensioni delle applicazioni e la complessità dell'ambiente computazionale sottostante, lo sviluppo di software non può prescindere da una validazione rigorosa prima che il >>>

Durata
24 mesi
Base di partenza scientifica nazionale o internazionale
Tipi, logiche e tecniche di ragionamento equazionale si stanno affermando come strumenti efficaci per l'analisi di computazioni distribuite e di sistemi aperti. Alcune tematiche di particolare rilevanza per la presente proposta riguardano l'uso di tipi e logiche per la descrizione delle risorse e delle loro modalità di utilizzo e l'impiego di teorie equazionali tipate per caratterizzare proprietà osservazionali dei processi e la loro struttura spaziale. Nel seguito descriveremo brevemente una parte della letteratura rilevante in questo ambito.


Sistemi di tipo


Negli ultimi anni le problematiche legate al controllo delle risorse e della mobilità , in forme diverse, sono state un tema cardine della ricerca di base nella teoria dei tipi. Gli argomenti considerati comprendono l'analisi di aspetti quali: l'abilità di leggere da / scrivere su un canale [PS96], il controllo della distribuzione dei nomi dei canali [YH99], la garanzia che gli agenti mobili utilizzeranno le risorse solo dopo essere stati autorizzati [HR02,DFPV00,BC01,HMR03], il controllo dell'interferenza [LS03], il controllo della mobilità degli agenti eventualmente basata su permessi specificati mediante tipi [DS00,MS02,CGG02,CDGS03], le garanzie di safety per gli scambi all'interno di ambienti di calcolo locali [CGG02], la segretezza di tali scambi [CGG00], il controllo della diffusione e condivisione di informazioni basato sul contenuto e >>>