Creating and sharing knowledge for telecommunications

Project: Space-Time-Types: Behavioural and Spatial Type Systems

Acronym: STT
Main Objective: 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.
Reference: POSC/EIA/55582/2005
Funding: FCT/POSC
Start Date: 01-07-2005
End Date: 01-06-2008
Team: António Maria Alarcão Ravara, Maxime Emile Gamboni
Groups: Network Architectures and Protocols – Lx
Partners: CITI (Centro de Informática e Tecnologias da Informação, FCT/UNL), with Researchers Luis Caires and Vasco Vasconcelos
Local Coordinator: António Maria Alarcão Ravara
Links: http://www.math.ist.utl.pt/%7Eamar/projectos/fct/spacetimetypes.html
Internal Page
Associated Publications