RICERCA ITALIANA     

Logical Foundations of Distributed Systems and Mobile Code

Università "Ca' Foscari" di Venezia

Abstract

Modern computer programs are increasingly being developed in support of distributed applications at different levels of abstractions, from IP-level communication protocols for mobile devices, such as IPv6, to application-level business transactions and e-commerce systems. The computing environments in which such programs operate are inherently open-ended, characterized by the absence of centralized structures, and built upon physical or virtual networks with complex structure and dynamic communication capabilities and services.

The role of formal methods for specification, analysis and verification is indisputable in this context as, given the size of the applications, and the complexity of the underlying computing environments, software development may not forego rigorous assessment before deployment. Yet, classical specification methods and verification techniques do not scale here. Firstly, the absence of centralized control, distinctive of open systems, invalidates the effectiveness of traditional verification methods which too often rely on the existence of precise, and reliable, assumptions on the structure and behavior of all system components to be analyzed and validated. Secondly, a number of core observables properties for computations in open systems, such as such as failures due to time-outs, delays due to shortage of communication bandwidth, quality of service parameters for communication links and other resource-centric parameters, remain >>>

Principal Investigator

Michele BUGLIESI Università "Cà Foscari" di VENEZIA

Research Objectives

Remote execution is an old and venerable topic in research on distributed systems, targeted at the development of techniques to support the sharing of computing power among distributed machines. The new advances in telecommunication tecnology have created revived interest and new challenges for this programming paradigm.

Modern computer programs are increasingly being developed to support distributed applications and protocols at different levels of abstractions, from IP-level communication protocols for mobile devices, such as IPv6, to application-level business transactions and e-commerce systems. The computing environments in which such programs operate are built upon physical or virtual networks with complex structure and dynamic communication capabilities and services. In addition, at all levels of abstractions these environments are inherently open-ended, and characterized by the absence of centralized structures of control, trust, and authorization.

The role of formal methods for specification, analysis and verification is indisputable in this context as, given the size of the applications, and the complexity of the underlying computing envronments, software development may not forego rigorous assessment before deployment. Yet, classical specification methods and verification techniques do not necessarily scale here: the absence of centralized control, distinctive of open systems, invalidates the effectiveness of traditional >>>

Timescale

24 months

National and international background

Types, logics and advanced techniques for equational reasoning are emerging as powerful tools for the analysis of distributed computations and open systems. Areas of particular relevance to the present proposal are related to the ability of types and logics to talk about resources and their usage, of typed equational theories to characterize observational properties of processes and their capture the spatial structure of systems. We briefly outline some relevant background below.

Type systems
Resource and mobility control, in diverse incarnations, has been the focus of extensive foundational research in type theory. Topics considered include the ability to read from and to write to a channel [PS96], the control of the location of channel names [YH99], the guarantee that distributed agents will access resources only when allowed to do so [HR02,CGZ01,BCC01,HMR03], the control of interference [LS03], the control of mobility, based on type-based permissions [DS00,MS02,CGG02,CDGS03], the guarantee of safety within local computational environments [CGG02], their secrecy [CGG00], the control on the flow and sharing of information, based on content and context [Mye99,CDV03].

With few exceptions, most of these systems rely on classical typing techniques whereby all the system components are type-checked under the same global typing assumptions. This is clearly unrealistic in distributed and dynamic environments as the ones of >>>