Micaela Mayero Homepage

Raffinement de spécifications de haut niveau:
(en collaboration avec C. Choppy et L. Petrucci)

De nos jours, les systèmes à modéliser et à analyser sont de taille de plus en plus grande. Pour s'affranchir des problèmes inhérents à l'explosion du nombre d'états, une spécification est souvent développée pas à pas (ce qui correspond à une démarche classique de développement de génie logiciel).

Tout d'abord, un modèle abstrait est défini. Une fois que ses propriétés sont vérifiées, une étape de raffinement, qui introduit un niveau de détail supplémentaire, peut être effectuée. Un tel ajout peut préciser la description de l'actuel fonctionnement d'une partie du système, ou introduire une partie supplémentaire. Le modèle ainsi raffiné est ensuite vérifié. Une nouvelle étape de raffinement peut alors être appliquée, et ce jusqu'à atteindre un niveau suffisant de description.

Trois types de raffinement ont été introduits par Lakos et Lewis, pour les réseaux de Petri de haut niveau :

le raffinement de sous-réseau
le raffinement de nœud
le raffinement de type

Ces raffinements ont été utilisés dans le cadre d'une approche incrémentale à la spécification de systèmes complexes. Outre les avantage du raffinement pour la spécification de systèmes, ils permettent de faciliter la vérification de propriétés. En effet, d'une part certaines propriétés sont préservées par le raffinement, et d'autre part, l'analyse du modèle abstrait permet de guider celle du modèle concret, économisant ainsi en temps de calcul et espace mémoire lors de la construction de graphes d'états.
Jusqu'à présent, le processus de raffinement de réseaux est complètement manuel. La vérification des contraintes peut être assez complexe. Par conséquent, nous souhaitons prouver automatiquement qu'un réseau est effectivement un raffinement d'un autre réseau (abstrait). Pour cela, nous utilisons des techniques de preuve de théorèmes, en particulier, l'assistant d'aide à la preuve Coq, développé à l'INRIA. Nous proposons donc une formalisation en Coq des définitions de raffinements ainsi que des réseaux auquels ils s'appliquent.