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.
Fundação da Faculdade de Ciências e Tecnologia, UNL