Abstract interpretation of mobile processes

Lines connect the coordinator with its partners. CORDIS does not always give exact coordinates for projects before 2014. These points are placed at city or country level.

Project objective

The design of efficient concurrent distributed systems is currently one of the major challenges in computer science. Compile time analysis is essential in software engineering and to develop efficient realizations able to fill the gap between high-level descriptions and their actual implementations. The basic idea of driving designers and implementors of systems with a hierarchy of semantics closer and closer to implementations is common to parametric theory of distributed systems and abstract interpretation. The candidate plan to extend the parametric theory based on the SOS description of proved transition system developed during his Ph. D. studies to the powerful format of GXSOS. This format allows the specification of finite as well as infinite behaviours of processes in an uniform way. Since infinite behaviours are an essential feature of distributed systems, and hence of mobile processes, the extension should improve the verification of these systems. In order to maintain the parametricity of the semantic definitions that allow a hierarchy of semantic descriptions, the candidate plans to replace relabelling functions defined on finite proved computations in his previous works with abstract intcrpretation. This is an essential step towards the realization of integrated programming environment that support designers of distributed systems in any phase of their life-cycle.

Original text from CORDIS.

Participants

• Centre National de la Recherche Scientifique (CNRS) · PARISCoordinatorFrance
• Not availableCity levelItaly

Links

• View on CORDIS