La modélisation d'un système en donne une représentation symbolique, le modèle, dont la sémantique peut être analysée plus ou moins automatiquement. Lorsque le but est la vérification d'une propriété du système (model checking), l'analyse doit être automatique, et l'immense majorité des sémantiques considérées sont alors des systèmes de transitions représentant les états possibles du modèle ainsi que les transitions le faisant passer d'un état à un autre. On appelle cela l'espace des états du modèle. Plusieurs caractéristiques des systèmes considérés amènent au problème connu sous le nom d'explosion de l'espace des états : les causes en sont généralement une forte combinatoire des états de sous-systèmes relativement indépendants ou la présence dans le modèle de données sur de grands ensembles.

Afin de contrer l'explosion de l'espace des états, plusieurs grandes familles de techniques existent : réduction du nombre d'états représentés en utilisant des classes d'états, abstraction symbolique des données, représentation compacte de l'espace des états, vérification modulaire de sous-systèmes ou de sous-espaces, parallélisation de la vérification etc.

Sur le plan international, la communauté de la vérification est très active sur la plupart des techniques d'accélération mais on peut constater un certain morcellement de l'effort dans ce contexte assez concurrentiel. Des tentatives de rapprochement entre différentes techniques existent mais restent des cas isolés.

Le projet VEHICULAIRE s'intéresse à la vérification de systèmes modélisés à base de réseaux de Petri de haut niveau, plus particulièrement une algèbre de réseaux structurée appelée M-Net. Ce formalisme a été choisi pour différents critères :

• Il relève du domaine de compétence des membres de l'équipe " Systèmes communicants " du LACL ;
• Les réseaux de Petri commencent à être utilisés de manière pratique par l'industrie et des communautés différentes que celles de la vérification des systèmes ;
• Il présente des caractéristiques autorisant d'intéressantes techniques d'accélération : les réseaux de Petri utilisés sont composables, autorisant ainsi une modélisation structurée ;
• L'algèbre est de haut-niveau et permet donc une représentation plus compacte des problèmes à modéliser et une explosion des états moindres du fait de cette description plus symbolique ;
• Les techniques d'accélération utilisées pour ce modèle (basées sur la concurrence des actions) sont souvent complémentaires de celles développées pour d'autres (abstraction, réduction, etc.).

Le projet a pour but principal la conception d'un algorithme parallèle BSP de construction du graphe des états d'une classe dédiée des M-Nets. Nous nous baserons sur la structuration d'une telle classe et du modèle BSP (via son modèle de performance) pour réduire les communications de l'algorithme et permettre un re-balancement optimal des données et des calculs pour la construction de ce graphe. En effet, la structuration de ces réseaux nous permettra de connaître de manière dynamique les tailles maximales des sous-graphes des sous-réseaux et ainsi de re-balancer au mieux les calculs et les communications (afin d'optimiser les performances de l'outil). L'utilisation du modèle de coûts BSP nous donnera aussi une prédiction des performances du model-checker et ce de manière très portable : il sera alors possible à l'utilisateur de prédire le temps d'exécution de l'algorithme sur une machine parallèle et donc de choisir au mieux la machine qu'il souhaite utiliser (ce travail, dans le futur, pourra être fait de manière automatique sur une grille de calcul via l'utilisation très aisée d'agents mobiles). Ceci diffèrera des précédents résultats sur des algorithmes distribués de model-checking où les performances sont imprédictibles et où les calculs (ainsi que les communications) sont mal balancés : une distribution randomisée des données sur les processeurs est en général utilisée et se révèle trop souvent inefficace à cause du mauvais balancement des calculs.

Pour implanter cet algorithme nous utiliserons le langage de programmation de haut-niveau (fonctionnelle, polymorphe, modulaire, etc.) Objective Caml (OCaml) et son extension BSP via une bibliothèque développée conjointement au LACL et au LIFO (la BSMLlib). L'utilisation des modules et du polymorphisme de OCaml nous permettra une exécution native (compilation en code machine) des réseaux sans nécessité un interpréteur de réseau : un réseau sera en fait un foncteur dépendant d'un module décrivant le type de jeton présent dans les places du réseau et d'un autre module décrivant les calculs faits par les transitions entre les places du réseau. Cette programmation de haut-niveau est donc idéale pour une indépendance de l'algorithme aux types de données (symboliques ou non) représentées par les jetons. Il en résultera donc une autonomie vis- à-vis des autres techniques de réduction des graphes des états.

Ce projet est innovant à plus d'un titre, en particulier sur ces deux points principaux :

• A notre connaissance il n'existe pas de technique de modularisation et de parallélisation (structurée) basées sur la bonne structuration d'un modèle de haut-niveau ;
• Contrairement à la tradition de la communauté de vérification qui tend à privilégier les langages de bas-niveau (C ou C++), nous utiliserons un langage de haut-niveau dont les bénéfices attendus seront une meilleure portabilité, une maintenance plus aisée, une meilleure évolutivité et la capacité d'exécuter de manière native les transitions d'un réseaux de Petri de haut-niveau (les transitions pourront être directement écrites dans du code OCaml).

Pour vérifier expérimentalement notre travail, nous appliquerons notre implantation à des protocoles cryptographiques qui ont déjà été modélisés par des membres du LACL avec une classe particulière des M-Nets (la sécurité et la sûreté des systèmes étant les thèmes fédérateurs du LACL). Pour continuer cette expérimentation, il sera envisagé de modéliser avec les M-Nets, puis vérifier avec notre outil de model-checking, les systèmes étudiés au LIFO par l'équipe PRV (notamment les protocoles pour le commerce électronique).