IPODS aims to solve some challenging problems that arise from pragmatical experiences in modern distributed computing systems by providing a robust theory where such problems can be dealt with systematically. In this sense, all contributions to the different themes can be read as far-from-trivial extensions of well-known approaches (process calculi, constraint systems, type systems, behavioural equivalences and conformance relations, etc.), which are best suited to attack the challenges posed by the requirements of complex interactions within open-ended systems in terms of flexibility and guarantees.

Roberto Bruni

Computer Science Department, University of Pisa

Largo B. Pontecorvo, 3 (formerly via F. Buonarroti, 2), I-56127 Pisa, Italy

E-mail: bruni AT di.unipi.it, Tel. (+39) 050 2212785, Fax: (+39) 050 2212726

• Roberto Bruni (Computer Science Dept., University of Pisa)
• Mariangiola Dezani (Computer Science Dept., University of Torino)
• Davide Sangiorgi (Computer Science Dept., University of Bologna)
• Michele Bugliesi (Computer Science Dept., Uni. of Venezia)

• Programme: Italian MIUR PRIN 2008 (2008-2010, 24 months)
• Original total cost: 260K Euro (as approved by reviewers)

The traditional concept of computation has evolved more and more rapidly in the recent years, to take into account the features of modern distributed systems as regards concurrency, dynamicity, mobility, security, interactivity, adaptability. In the meantime, the complexity of these “global” systems has increased: they are based on wide-area networks like the internet and are oriented to support a wide range of heterogeneous applications which, though developed separately, need to interact in a checked and safe way.

In this framework, the goal of the project is to develop robust mathematical foundations for collaborative scenarios that are characterised by high dynamicity of participants. The participants can join or leave collaborations in an autonomous way and their behaviours are strongly affected by the environment, i.e., by the set of the involved participants and the set of the rules that control the interaction. For example, a component might need to update or to cancel some of its functionalities, or to add new functionalities depending on its environment, if possible in an automatic way. In addition, there may be adversaries that try to cause the failure of some collaborations. These features are common to many domains, like social networks, web services, long transactions. More concretely, we aim at extending and integrating the techniques of static and dynamic analysis in order to offer some guarantees, with variable levels, on the ability of successfully carry out a given task, on the available resources and on the security of communications.

The project is characterised by the singling out of three different phases occurring in every collaboration: 1) negotiation; 2) commit; 3) execution. More precisely, in (1) the prospective participants negotiate some guarantees in order to define a sort of contract. Each of them can then, in the phase (2), either accept or reject the contract. If they accept, the contract will bind their behaviours in (3) so as to guarantee a globally correct execution. The schemata given by the phases (1-3) cover a wide range of situations. For example, these phases can be found in transactions (phases 1-2), in the sessions (phases 2-3), in the applications of proof-carrying code (phases 1 and 3). Necessarily we need to allow part of the verification to be done also at runtime, on the basis of both statically and dynamically negotiable information.

We will use the mathematical instruments given by the concurrency theory (process calculi, Petri nets, graph rewriting, behavioural relations) and by the type theory (session types, behavioural types, dependent types, polymorphic types). In particular, we will study how to extend: process calculi, in order to express constraints on interactions and to model sessions and transactions with compensations to be executed in case of failure; session types, for defining abstract conversations between components; relations of behavioural conformance for dealing with adaptivity; types and observational theories for expressing security invariants on data and on component behaviours. These extensions will help us to define useful abstractions for the specification of open and dynamic collaborative systems, where participants often have a partial view of the system, limited to the components with which they interact directly.

An important aspect of the interaction mechanisms sketched above concerns taking suitable measures to guarantee their success also in presence of malicious components. This requires the design of a series of low-level protocols able to find out and correct any deviation from the expected behaviour for each component. We will study these mechanisms and develop techniques for getting fully abstract encodings of the interaction primitives in the low-level protocols that implement them.

Equally important is the realisation of mechanisms to protect data. In an open system, for example in a peer-to-peer system, the participants need to know which data/resources are accessible to them, at which component locations. Dually, it is necessary that each component can specify access policies to its data/resources. We will therefore study negotiation techniques for matching the data necessary to each component to the associated access rights, so as to reduce in the execution phase the number of failures and the overhead due to checks.