CITI has stopped operations in 2014, to co-launch NOVA LINCS THIS SITE IS NOT BEING UPDATED SINCE 2013
citi banner
  Home  \  Research Projects  \  Project Page Login  
banner bottom
File Top
Liveness, statically

Technical Note:

The main objective of the project is the development of automatic solutions to guarantee liveness properties of distributed, collaborative, communication-centred, software systems and applications. With the generalisation of internet access, computational devices are these days network-aware and need to adapt dynamically to the environment they are working in. They are inherently concurrent, running often in multi-core architectures, and running distributed software applications which integrate information and resources from heterogeneous locations, providing services to the end-user. In this global computing scenario, a new communication-centred programming paradigm emerged. Sound programming abstractions and methodologies are crucial to support the development of theories, languages, and tools to assist hardware and software developers. Hardware and software developers should be able of guaranteeing that such devices work correctly and securely: not only the functions the devices perform are correct, the dynamic addition of functionalities do not compromise the overall behaviour of the device, and furthermore, that the devices are reliable. Excluding undesired behaviours like protocol incompatibilities, deadlocks, races, livelocks, just to name a few, is a very difficult task, requiring much more than just the programmer's skills. To provide such guarantees, one needs to be able of rigorously modelling both the requirements of the systems and of the applications they run, as well as their behaviour. Moreover, one needs to provide the intended assurances a priori, before the devices and applications actually run in (potentially dangerous) open environments. Therefore, one has to be able of not only defining precisely the properties, but also of reasoning and provably ensure the properties hold for a given system specification. Furthermore, to be widely used and applicable to large systems, the tools used should be automatic. Our aim is to develop source-level program analysis techniques and tools to statically ensure liveness properties of communication-centred systems and applications. Using expressive specification languages to describe interaction patterns, where the behavioural statements are formulae of some decidable fragment of a logic, we envisage decidable compile-time checking of the properties. Combining the approaches of model-checking and of type-checking, we plan to develop automatic proof systems to incorporate in compilers. Specifically, our objectives are the following. 1) Pursue a semantical approach to types for concurrency: we want to study the expressiveness of languages like session-, or conversation-, types, looking for decidability and complexity results. 2) Develop type systems for various settings, from process calculi to programming languages, able of ensuring liveness properties like the absence of races, deadlocks, or livelocks, and like activeness (ability to establish a connection) and responsiveness (ability to conduct a conversation for each connection), progress and termination. 3) Study generic type systems using spatial logics and ensuring general properties, either existential (some run of the system enjoys of a property from some moment on) or universal (all runs of the system enjoys of a property from some moment on). 4) Develop prototypes, integrating the type systems with model checkers and with compilers for core programming languages.

{ Project Info }

Coordinated by: Fundação da Faculdade de Ciências e Tecnologia (FFCT/FCT/UNL)

Project Type: PN ( National basic research or R&D projects )

Funding Entity: FCT / MCTES

Total Funding Amount: 132.2 Keuro

CITI Funding Amount: 73.3 Keuro

Start Date: 2012-03-20 / Efective Start Date: 0000-00-00

End Date: 2015-04-19 / Efective End Date: 0000-00-00

{ CITI Participations }

{ Partnerships }
File Bottom