Space-Time-Types - Behavioural and Spatial Type Systems
Mar 2005 - Mar 2008
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.
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.
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.
