|
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.
|