– PANDA

La plupart des programmes de contrôle-commande industriels sont des programmes parallèles (souvent basés sur le paradigme synchrone, mais pas toujours), ou des programmes distribués (le plus souvent, tolérants aux pannes). En général, les méthodes formelles et l'analyse statique n'ont été employés dans ce contexte que pour valider ces systèmes sous des hypothèses simplificatrices, concernant l'ordonnancement des tâches parallèles. Si ces hypothèses sont souvent satisfaites dans les systèmes "vraiment" critiques (on impose une forme de synchronisation, et en particulier de déterminisme, très strict, rendant le programme parallèle équivalent à un programme séquentiel), ce n'est plus le cas pour des systèmes moins critiques, plus asynchrones et plus non-déterministes. Quelque soit le modèle concret de calcul que l'on utilise, la validation des programmes parallèles et distribués est difficile, parce-que le nombre d'états accessibles est trop important pour être énumére, et il est difficile même d'écrire complètement la sémantique collectrice. Cela est du au trop grand nombre d'ordonnancements d'actions, possibles. Cela s'ajoute à la taille généralement importante de ces codes, qui, parce-qu'ils sont moins critiques, sont souvent plus gros. L'objectif de ce projet est de développer des théories et des outils permettant de s'attaquer efficacement à cette explosion combinatoire, afin de valider des programmes parallèles et distribués par analyse statique. Notre intérêt principal réside dans les systèmes multithreadés à mémoire partagée. Mais nous considérons également d'autres paradigmes de calcul parallèle, rendant compte de la plupart des paradigmes couramment utilisés (passage de message par exemple comme dans POSIX et VXWORKS), où ceux, plus récents, de Singularity, qui fourniront de bons cas d'études pour les méthodes et les sémantiques développées dans ce projet. Enfin, nous voulons montrer que nos approches pour comparer les modèles et analyseurs statiques basés sur ces modèles marchent bien en pratique. Nous nous baserons sur des codes académiques, mais aussi des codes industriels comme ceux fournis par Airbus. Nous comptons rendre public une partie des résultats de ce projet en publiant dans les meilleures conférences internationales et en publiant une partie de nos codes en open source.