Objectives

The Panda project has the following main objectives:

• Give the theoretical tools for comparing the models of concurrent programs at hand, in particular newer ones, such as the geometric models for concurrency.
• Compare several rising models to more classical ones:
  • geometric models vs transition systems, Mazurkiewicz traces and event structures;
  • models based on higher order categories vs rewriting systems, event structures, and Mazurkiewicz traces.
• Bring together models for concurrency completing each other so we can take into account various aspects of parallelism. In particular, we think the interaction between spatial/separation logics and geometric models will raise breakthrough in understanding concurrent tasks behaviour.
• Implement a common platform for the static analysis of concurrent programs, based on the existing ALCOOL analyzer (developed by CEA LIST). In particular we wish to prove the adequacy of our approach on a representative piece of code (provided by Airbus). For instance, in order to adress the lack of primitive synchronization notions of languages like PROMELA, ALCOOL offers an input language natively provided with a wide range synchronization mechanisms.
• Develop a comprehensive framework for probabilistic concurrent systems that would apply to several models of concurrency; understand how usual concepts and tools from probability theory such as limit theorems apply to those models. A challenging part is to deal with asynchrony in terms of partial orders together with probability.

Panda deals with several implementation issues, and in particular with applications to fault detection in industrial parallel and distributed software. The industrial needs for an efficient toolbox for verifying and certifying the analysis of parallel avionics programs (detection of typical parallel properties: race conditions, deadlocks, etc.) is clearly increasing and our project addresses this concern.