Project PTDC/EIA-CCO/117513/2010 (March 2012 - March 2015), funded by FCT.
Principal investigator: António Ravara.
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 to guarantee that such devices work correctly and securely, that the functions the devices perform are correct, that the dynamic addition of functionalities does not compromise the overall behaviour of the device, and 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 programmers 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 that 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 be incorporated in compilers.
Specifically, our objectives are the following.Last modified: Sat Dec 7 16:48:20 WET 2013