Vérification Et Validation Des Transformations De Modèles

Résumé: L'Ingénierie Dirigée par les Modèles (IDM) se base sur l'utilisation intensive et systématique des modèles tout au long du processus de développement de logiciels. Ainsi, l'IDM vise à améliorer l'interopérabilité, la réutilisation et la possibilité de migrer les modèles pour desapplications hétérogènes. Dans le contexte de l'IDM, la transformation de modèles est une phase cruciale puisqu'elle définit l'automatisation qui peut être utilisée dans le processus de développement de logiciels. Il est donc nécessaire d'augmenter la sûreté, la vérification et la validation d'une telle transformation de modèles. A cet effet, il est important de proposerdes solutions pour intégrer les méthodes formelles dans le processus de transformation où la plupart des langages de transformation n'ont pas une sémantique formelle pour ajouter des spécifications détaillées sur le comportement attendu. L'idée de base de notre travail est de définir une transformation de modèles avec un langage de transformation comme QVT-op, vérifier la conformité des modèles avec le langage OCL et valider le programme de transformation en utilisant un assistant de preuve Coq. Nous illustrons ce travail en spécifiant une transformation de modèle complexe et hétérogène entre le diagramme d'états-transitions UML et les réseaux de Pétri.

Publié dans la revue: