Etablissement
Ecole Nationale Supérieure d'informatique
Affiliation
Département de Post-Graduation
Auteur
BENNAMA, Miloud
Directeur de thèse
Thouraya Bouabana-Tebibel (Professeur)
Filière
Informatique
Diplôme
Doctorat
Titre
Modélisation formelle basée sur les diagrammes globaux d’interaction d’UML2
Mots clés
UML2, IOD, SD,OCL,HCPN, ASKCTL, CPNtools, Formalisation, vérification, analyse, model-checking, validation, interprétation, animation.
Résumé
Les versions successives d’UML, parvenant aujourd’hui à 2.4.2 (OMG-11), constituent une évolution importante dans la modélisation structurale et comportementale des systèmes. Cette évolution est justifiée, principalement, par le changement radical dans la portée de son diagramme d’activités et la promotion de la sémantique de ses interactions. Les nouveaux concepts et diagrammes introduits sont essentiellement inspirés d’autres formalismes tels que PN(Petri Net), MSC (Message Sequence Chart), et SDL (Specification and Design Language). Toutefois, l’imprécision de sa sémantique exclut l’intégration de toute activité de validation. Ceci se manifeste par l’absence d’outils garantissant l’analyse formelle de ses modèles (Störrle-07). Pour combler cette insuffisance, l’idée de marier la notation semi-formelle UML à des méthodes formelles comme les réseaux de Pétri a émergé progressivement dans l’axe d’ingénierie des systèmes. L’intégration du diagramme global d’interaction (IOD) dans UML 2 a permis d’introduire un flot de contrôle sur les diagrammes de séquences. L’IOD dispose d’un pouvoir d’expression qui lui permet de montrer l’interaction des composants d’un système à un haut niveau d’abstraction. Sa force réside dans sa capacité d’exhiber les dépendances entre les séquences d’un système par le biais d’une structure de contrôle. Sa structuration hiérarchique et le flot de contrôle de ses interactions sont des caractéristiques favorisant son utilisation pour la modélisation des systèmes interactifs. Ces caractéristiques interpellent également sur la nature du formalisme approprié à la formalisation de sa sémantique. Les réseaux de Pétri colorés et hiérarchiques (HCPNs) paraissent constituer un formalisme de choix pour ce diagramme. Ils se distinguent par leur pouvoir de spécification formelle dans le domaine et sont supportés par de nombreux outils permettant l’édition, la simulation et l’analyse de leurs modèles. Beaucoup de travaux ont déjà abordé l’étude de la sémantique des diagrammes d’activités et de séquence d’UML2 à base des réseaux de pétri (Bouabana-07), (Störrle-05), (Andrade-09), (Staines-08), (Fernandes-07), (Alhroob-10). Cependant, peu de résultats sont communiqués sur la formalisation du diagramme global d’interaction utilisé pour combiner des fragments d’interactions dans une sorte de flots de contrôle et de données. Quatre travaux de formalisation de la sémantique des IODs méritent d’être cités. Le premier est celui de Kloul et Filipe (Kloul-05) qui montrent l’apport des IODs pour modéliser les systèmes mobiles en les transformant en algèbre de processus stochastique PEPA. Le travail d’Andrade et al. (Andrade-08) est plus proche du nôtre. Il transforme les IODs vers les réseaux de Petri temporisés (non hiérarchiques). Une autre étude, plus récente, celle de Whittle (Whittle-10) exploite les concepts des diagrammes d’activités pour étendre la sémantique des IOD vers des EIOD pour une éventuelle simulation avec l’outil UCSIM. Une autre formalisation de la sémantique des IODs à base de formules de la logique temporelle TRIO a été présentée dans (Baresi-11). Mais aucun de ces travaux n’a employé les PNs hiérarchiques et aucun n’a traité le problème d’interprétation et de rétroaction des résultats d’analyse. Un cas d’interprétation du diagramme d’état-transition d’UML1.x par retour de diagrammes de séquence a été présenté dans (Hu-04). Notre contribution va au-delà de la simple formalisation des composants de ce diagramme, déjà présents dans les diagrammes d’activités et de séquences. Elle vise la mise en place d’un véritable atelier de spécification et de vérification formelle des IODs, au travers d’une interface exhibant, seulement, les éléments de modélisation UML. Ainsi, le modélisateur UML spécifie puis valide ses modèles sans connaissance aucune des formalismes exécutés en arrière plan de son atelier. Une première étude a déjà été entreprise dans (Bouabana-09) et (Bennama-09) où les HCPNs sont simplement vérifiés par le model-checker Prod (PROD-04). Notre présente étude, quant à elle, s’oriente vers l’analyse et l’interprétation des modèles HCPN dérivés des IOD au moyen du model-checker CPNtools (Ratzer-03) et l’animateur des graphes BRITNeY, après les insuffisances rencontrées dans Prod. Les résultats de la validation seront retournés au modélisateur dans une forme interprétée sur les modèles UML qu’il a construits. Cette idée a déjà été traitée dans (Bennama-10) mais le travail manquait de maturité. Il nécessitait une étude plus poussée sur la structure des objets en interaction, les paramètres des messages échangés et l’expression des prés et post-conditions sur les interactions pour arriver à une interprétation de l’analyse des modèles HCPNs traduite de façon avancée sur les diagrammes UML. Une telle analyse repose, essentiellement, sur des propriétés génériques liées à la bonne construction du système et des propriétés spécifiques écrites par le modélisateur pour contrôler la cohérence de la modélisation. Notre nouvelle étude (Bennama-12) requiert, par ailleurs, le recours à de nouveaux diagrammes, à savoir les diagrammes de classes et d’objets, pour localiser les différentes erreurs de modélisation. Une nouvelle contribution de ce travail apparait, également, dans la translation des contraintes OCL en logique ASKCTL à base du langage ML. L’approche de vérification et d’interprétation est appliquée sur un Distributeur Automatique de Billets (DAB).
Statut
Vérifié