Nowadays distributed computing systems are based on a simple
paradigm of asynchronous message passing, since communication is the
key feature of such systems and message passing is a natural way of
modelling interaction. However, a global computing scenario poses new
problems that are not present in the classical sequential and
centralised systems. Situations like (partial) failures, disruption of
connections, code mobility, dynamic reconfiguration of networks, make
this domain intrinsically complex, whose analysis is particularly
challenging. Moreover, the demand for safe and trustworthy
applications and systems is increasing, as users become aware of the
vulnerability of their present systems.
Solid mathematical foundations are essential to provide such
guarantees. Provably correct solutions require rigorous mathematical
models and analysis techniques, so that one may define precisely what
are the problems to address, and how to perform proofs for the claimed
properties. To express and prove properties logical systems are
needed, but since most interesting properties are undecidable one
cannot find complete proof systems. Furthermore, some decidable
properties are intrinsically difficult to verify.
The typical solution is to use a decidable static analysis system
(correct by over-approximating, but necessarily incomplete), of low
computational complexity (to be of practical to use). A popular
approach is the use of type systems to discipline the computational
mechanisms programming languages, disallowing interactions that may
lead to erroneous operations. Types are abstract representations of
the correct behaviour of the entities of a program. A language is type
safe, if it is equipped with a type (proof) system that guarantees
that if a program is typable, the computation mechanism preserves the
typability of the intermediate steps, and the absence of run-time
errors.
The goal of the project is to develop new type systems to
statically verify behavioural and structural properties of global,
distributed open systems. We shall pursue our previous work on three
inter-related subjects: non-uniform types for concurrent objects,
investigating decidability issues; session types for component
interoperability, investigating their extension to multi-party
protocols; spatial types, investigating static analyses methods to
prove not only behavioural and but also structural properties of
distributed systems. Moreover, we plan to study the relationship
between behavioural and session types, looking for a unified notion
and system, and to relate spatial to behavioural types, characterising
the latter in terms of the former.
Our goal is the development of static analysis systems to verify
safety and liveness properties of concurrent distributed systems
specified in calculi of mobile processes. The properties we are
interested in are not only behavioural, like deadlock freedom or
conformance to a protocol, but also structural (or spatial), like
connectivity or resource usage. The existing systems treat only some
of the behavioural properties, in a limited way (not purely static, or
in very restricted settings). Building on existing work on behavioural
types and on spatial logics,
we aim at the development of richer notions of types, able of
expressing behavioural and spatial properties of distributed
systems. We envisage expressive, yet decidable and computationally
tractable static analysis systems, which allow to formally prove that a
process enjoys a certain property, and that there will be no run-time
property violations.
T1 - Non-uniform Types
The specific goal of this task is the study of
the use of behavioural types in several contexts: (1) In systems of
concurrent objects, looking for a decidable notion of simulation which
coincides with subtyping, and then defining a type inference algorithm
for a non-uniform type system to a mobile calculus of objects. (2) In
a framework allowing the definition of a single type system using
tailored subtyping relation to check several properties which are now
treated separately, each by a particular system with a specific notion
of type. These properties are: no arity mismatch in the use of
channels; enforcement of input/output or linear use of channels,
message immediately or eventually understood, absence of orphan
messages.
T2 - Session Types
The specific goal of this task is the development of type systems which
allow complex protocols to be specified in a high-level manner, and
support verification by relatively straightforward static
type-checking. In previous work we have used session types to specify
the dynamic communication between components. We have also studied
precise definitions of compatibility and substitutability tests, which
form the basis of efficient static checks that components will interact
correctly. Our aims are now twofold: (1) To further develop the
framework of session types, extending them from dyadic to multiparty
interactions. (2) To equip our experimental concurrent functional
language with object-oriented constructs.
T3 - Spatial Types
The specific goal of this task is the definition of a decidable proof
system to statically verify spatial and behavioural properties of
processes (notice that model-checking is restricted to finite
reachability). Following the approach "propositions as types", the
types are spatial logic formulae, subtyping is logical entailment, and
the type system is a deductive system. We want to capture an expressive
sublanguage of spatial logics, which allow us to specify and verify the
referred properties, keeping the proof system decidable.