Lifo - Laboratoire d'Informatique Fondamentale d'orléans INSA Centre Val de Loire Université d'Orléans Université d'Orléans

Lifo > Les Actions de Recherche du LIFO > Action de Recherche : VEHICULAIRE

 English Version



Contact

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 70 11
Fax: +33 (0)2 38 41 71 37



VEHICULAIRE : Vérification Efficace de Haut-nIveau multi-proCesseur et modULAIRE

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.

Financement

Groupement de Recherche Architecture, Systèmes, Réseaux (ASR), pôle Grille, Système et Parallélisme (GSP)

Participants

Radia BENHEDDI

Jean-Michel COUVREUR

Frédéric LOULERGUE

Duy Tung NGUYEN

Page web de l'action

http://www.univ-paris12.fr/lacl/gava/vehiculaire/vehiculaire.html