Behavioural and Spatial Type Systems

Project POSC/EIA/55582/2004 (July 1, 2005 - June 31, 2008) funded by FEDER and FCT. An initiative of CLC with CITI.

Team | Summary | Objectives | Tasks | Relevant publications

Luís Caires

Tiago Carvalho

Maxime Gamboni

António Ravara

Vasco T. Vasconcelos

Team | Summary | Objectives | Tasks | Relevant publications

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.

Team | Summary | Objectives | Tasks | Relevant publications

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.

Team | Summary | Objectives | Tasks | Relevant publications

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.

Team | Summary | Objectives | Tasks | Relevant publications

Non-uniform Types

Session Types

Spatial Types

Team | Summary | Objectives | Tasks | Relevant publications