Utilisation Des Systèmes De Réécriture Pour La Modélisation Et La Vérification Des Applications Orientées Aspect

Résumé: La programmation orientée aspect est considérée comme une des approches de séparation avancées des préoccupations. Elle a prouvé son efficacité dans le domaine de génie logiciel. En effet, elle a pu remédier, avec son nouveau lot de concepts et mécanismes, à certains problèmes observés avec la programmation orientée objet tels que le problème d’enchevêtrement et de dispersion du code. La programmation orientée aspect propose de décomposer le programme non seulement en unités modulaires représentant les préoccupations fonctionnelles de base, mais aussi en unités modulaires, qui s’appellent aspects, dédiées à la représentation des préoccupations transversales. Ces aspects sont ensuite composés puis intégrés dans le programme de base par un processus automatique appelé tissage. Cependant, bien que cette approche améliore le système en termes de modularité, réutilisabilité et maintenabilité, elle souffre du problème d’interaction des aspects. En effet, les aspects peuvent violer la cohérence du système initial après leur composition et intégration dans ce système. Ceci est dû aux interactions qui peuvent exister entre les aspects eux-mêmes et/ou entre les aspects et le système de base. En effet, lorsque plusieurs aspects s’intéressent au même point de jointure de système de base et si aucun ordre d’exécution des aspects n’est défini, ceux-ci vont être exécutés dans un ordre quelconque. De ce fait, des interactions conflictuelles peuvent se manifester entre les aspects qui influencent à leur tour sur le comportement de système de base. L’approche formelle en général et les systèmes de réécriture en particulier peuvent apporter une solution à ce problème en recourant à la modélisation des interactions système de base/aspects par des digrammes UML. Ces derniers seront facilement vérifiés en utilisant les outils disponibles pour la vérification formelle. Ce travail vise deux objectifs. Le premier consiste, d’une part, à proposer des cadres formels pour la modélisation et la vérification des systèmes orientés aspect dans le niveau conceptuel. D’autre part, cet objectif porte sur l’élaboration d’un système de réécriture tout en se basant sur la construction du cadre formel permettant la transformation de modèles UML vers des spécifications dans le langage Maude. Ces spécifications sont ensuite vérifiées avec le vérificateur de modèles de Maude. Le deuxième objectif consiste à proposer un outil formel AO-Maude qui se base sur la méta-réécriture afin de spécifier et vérifier formellement les systèmes orientés aspect.

Publié dans la revue: