LIFO - Bâtiment IIIA
Rue Léonard de Vinci
B.P. 6759
F-45067 ORLEANS Cedex 2
Email:
contact.lifo
Tel: +33 (0)2 38 41 99 29
Fax: +33 (0)2 38 41 71 37
La vérification automatique de modèles (model checking) est une approche séduisante mais généralement coûteuse en termes de temps de calcul et d'espace mémoire nécessaire. Beaucoup de travaux dans le domaine sont dédiés à l'accélération des calculs et à la réduction de l'espace d'exploration. La parallélisation de ce calcul est l'une des techniques envisageables. Cependant, elle est en général employée avec des modèles de bas-niveau (tant au niveau du modèle étudié que du langage et du parallélisme utilisés pour implanter le model checker) et avec une distribution plus ou moins naïve des données.
L'objectif de ce projet est tout d'abord la conception d'un algorithme parallèle BSP de construction de l'espace d'exploration d'une algèbre de réseaux de Petri colorés de haut-niveau, appelé M-Net. L'utilisation d'un tel modèle fortement structuré nous permettra d'utiliser le parallélisme structuré et donc plus efficace (et portable) qu'est le modèle BSP. Ensuite, une implantation modulaire et polymorphe (indépendante des types de données, donc idéale pour le model cheking symbolique et pour une algèbre de haut-niveau) sera effectuée avec une bibliothèque de programmation parallèle de haut-niveau, appelée BSMLlib, développée conjointement au LACL et au LIFO. Enfin, des tests appliqués à des problèmes de sécurité informatique (thème fédérateur du LACL) seront effectués sur les différentes grappes de PCs du LACL et du LIFO.
Groupement de Recherche Architecture, Systèmes, Réseaux (ASR), pôle Grille, Système et Parallélisme (GSP)
Radia BENHEDDI
Duy Tung NGUYEN
http://www.univ-paris12.fr/lacl/gava/vehiculaire/vehiculaire.html
Université d'Orléans | INSA Centre Val de Loire