Informations
Directeur de thèse :
Université :
Université Constantine 2
Soutenance
Date de soutenance :
4 Novembre 2017
Jury :
Djamel Eddine Saidouni
Allaoua Chaoui
Makhlouf Derdour
Fateh Boutakouk
Abdelhafid Zitouni
Manuscrit
Téléchargement :
Détails
Titre :
Une Approche pour la vérification de la cohérence comportementale des diagrammes UML 2.0 basée sur la transformation des diagrammes de séquence UML 2.0 vers les automates de Büchi

Résumé :

De nos jours, de nombreux projets, ou de grands systèmes complexes sont développés, mais la conservation de la cohérence entre les différentes spécifications devint un problème majeur. En pratique, cette tâche est délicate dû aux manques d'outils CASE qui peuvent aider à faire face à ce problème. Les spécifications doivent généralement être cohérentes, au cours des différentes étapes de développement et même au sein d’une étape elle-même. Les développeurs ont souvent tendance à effectuer ces vérifications manuellement (contrôle statique des éléments d’un même modèle), ce qui entraîne beaucoup de temps consacré à un travail qui pourrait être automatiquement réalisé, en plus du fait que la méthode manuelle peut ne pas être également correcte en tant que routine de vérification comparée à celle basée sur un outil de vérification.

La vérification comportementale des diagrammes UML 2.0 a fait l’objet de plusieurs recherches spécifiant deux grandes familles de traitement du phénomène, une utilisant les transformations de modèles vers un modèle formel et une autre consistant à utiliser directement le modèle. Le développement d’une approche de vérification basée sur les transformations passe obligatoirement par la compréhension profonde des sémantiques associées aux diagrammes manipulées.

Une des façons de spécifier le comportement dynamique dans UML consiste à modéliser les interactions entre les objets avec des diagrammes de séquence et de modéliser le comportement de chaque objet avec des machines à états. Dans ce contexte, le problème d'assurer la cohérence entre les diagrammes de séquence et les machines à états peut apparaître. Pour vérifier la cohérence, nous proposons une approche basée sur des compositions d'automates de Büchi qui nous permettent de saisir l'évolution de chaque objet le long de sa ligne de vie. Notre thèse se concentre sur les méthodes de modélisation et de vérification UML et comble l'écart entre les études théoriques sur les sémantiques formelles et les études pratiques pour implémenter les langages à travers des transformations de modèles. Les transformations comprennent les interactions de bases, des invariants d'état, la séquence strict et faible et des fragments d'interaction alternatifs.


Mots clés :
Conception UML Cohérence UML OCL Automates de Büchi ATL


Abstract:

Nowadays, many projects, or large complex systems are developed, but suffer to keep their specifications consistent. In practice, this is not an easy task due to the lack of CASE tools that help to deal with this problem. The specifications must generally be consistent, during different stages of development and even within a development stage. Developers often tend to perform these checks manually (static control of the same model elements), which results in a lot of time spent on work that could be automatically associated, in addition to the fact that the manual method may not be also correct as a verification routine compared to that based on a verification tool.

The behavioral verification of UML 2.0 diagrams has been the subject of several studies specifying two main families of treatment of the phenomenon, one using the transformations of models towards a formal model and another one consisting of using directly the model. The development of a transformation-based verification approach requires a deep understanding of the semantics associated with the manipulated diagrams.

One of the ways to specify dynamic behavior in UML is to model interactions between objects with sequence diagrams, and model the behavior of each object with state machines. In this context, the problem of ensuring consistency between the sequence diagrams and state machines may arise. To verify consistency, we propose an approach based on compositions of Büchi automata which allow us to capture the evolution of each object among the lifeline. Our paper focuses on UML modeling and verification methods and bridges the gap between theoretical studies on formal semantics and practical studies to implement languages through model transformations. The transformations include basic interactions, state invariants, strict and weak sequencing, and alternative interaction fragments.


Keywords:
UML design UML consistency OCL Büchi automata ATL


:الملخص

ﻓﻲ اﻟﻮﻗﺖ اﻟﺤﺎﺿﺮ، ﯾﺘﻢ ﺗﻄﻮﯾﺮ اﻟﻌﺪﯾﺪ ﻣﻦ اﻟﻤﺸﺎرﯾﻊ، أو أﻧﻈﻤﺔ ﻣﻌﻘﺪة ﻛﺒﯿﺮة، وﻟﻜﻦ ﺗﻌﺎﻧﻲ ﻟﻠﺤﻔﺎظ ﻋﻠﻰ ﻣﻮاﺻﻔﺎت ﻣﺘﺴﻘﺔ. ﻓﻲ اﻟﻤﻤﺎرﺳﺔ اﻟﻌﻤﻠﯿﺔ، ھﺬه ﻟﯿﺴﺖ ﻣﮭﻤﺔ ﺳﮭﻠﺔ ﻧﻈﺮا ﻟﻌﺪم وﺟﻮد أدوات اﻟﺘﻨﺴﯿﻖ اﻟﺘﻲ ﺗﺴﺎﻋﺪ ﻋﻠﻰ اﻟﺘﻌﺎﻣﻞ ﻣﻊ ھﺬه اﻟﻤﺸﻜﻠﺔ. ﯾﺠﺐ أن ﺗﻜﻮن اﻟﻤﻮاﺻﻔﺎت ﻣﺘﺴﻘﺔ ﻋﻤﻮﻣﺎ، ﺧﻼل ﻣﺮاﺣﻞ ﻣﺨﺘﻠﻔﺔ ﻣﻦ اﻟﺘﻄﻮﯾﺮ وﺣﺘﻰ ﻓﻲ ﻣﺮﺣﻠﺔ اﻟﺘﺼﻤﯿﻢ .ﻏﺎﻟﺒﺎ ﻣﺎ ﯾﻤﯿﻞ اﻟﻤﻄﻮرون إﻟﻰ إﺟﺮاء ﻋﻤﻠﯿﺎت اﻟﺘﺤﻘﻖ ھﺬه ﯾﺪوﯾﺎ (اﻟﺘﺤﻜﻢ اﻟﺜﺎﺑﺖ ﻟﻌﻨﺎﺻﺮ اﻟﻨﻤﻮذج ﻧﻔﺴﮫ)، ﻣﻤﺎ ﯾﺆدي إﻟﻰ اﻟﻜﺜﯿﺮ ﻣﻦ اﻟﻮﻗﺖ اﻟﺬي ﯾﻘﻀﯿﮫ اﻟﻌﻤﻞ اﻟﺬي ﯾﻤﻜﻦ رﺑﻄﮫ ﺗﻠﻘﺎﺋﯿﺎ، ﺑﺎﻹﺿﺎﻓﺔ إﻟﻰ ﺣﻘﯿﻘﺔ أن اﻟﻄﺮﯾﻘﺔ اﻟﯿﺪوﯾﺔ ﻗﺪ ﻻ ﺗﻜﻮن ﺻﺤﯿﺤﺔ ﺑﺎﻟﻤﻘﺎرﻧﺔ ﻣﻊ ذﻟﻚ اﺳﺘﻨﺎدا إﻟﻰ أداة اﻟﺘﺤﻘﻖ آﻟﯿﺎ.

ﻣﻮﺿﻮع اﻟﻌﺪﯾﺪ ﻣﻦ اﻟﺪراﺳﺎت ﺗﺤﺪﯾﺪ اﺛﻨﯿﻦ ﻣﻦ اﻷﺳﺮ 2.0 وﻗﺪ ﺗﻢ اﻟﺘﺤﻘﻖ اﻟﺴﻠﻮﻛﻲ ﻣﻦ اﻟﻤﺨﻄﻄﺎت أوﻣﻞ اﻟﺮﺋﯿﺴﯿﺔ ﻟﻌﻼج ھﺬه اﻟﻈﺎھﺮة، واﺣﺪة ﺑﺎﺳﺘﺨﺪام ﺗﺤﻮﻻت اﻟﻨﻤﺎذج ﻧﺤﻮ ﻧﻤﻮذج رﺳﻤﻲ وآﺧﺮ ﯾﺘﻜﻮن ﻣﻦ اﺳﺘﺨﺪام ﻣﺒﺎﺷﺮة اﻟﻨﻤﻮذج. ﯾﺘﻄﻠﺐ ﺗﻄﻮﯾﺮ ﻧﮭﺞ اﻟﺘﺤﻘﻖ اﻟﻘﺎﺋﻢ ﻋﻠﻰ اﻟﺘﺤﻮل وﯾﺠﺐ ﻓﮭﻢ ﻋﻤﯿﻖ ﻟﻠﺪﻻﻻت اﻟﻤﺮﺗﺒﻄﺔ ﺑﺎﻟﻤﺨﻄﻄﺎت.

ﻣﻦ ﺑﯿﻦ اﻟﻄﺮق ﻟﺘﺤﺪﯾﺪ اﻟﺴﻠﻮك اﻟﺪﯾﻨﺎﻣﯿﻜﻲ ﻓﻲ ھﻲ ﻧﻤﻮذج اﻟﺘﻔﺎﻋﻼت ﺑﯿﻦ اﻟﻌﻨﺎﺻﺮ ﻣﻊ ﻣﺨﻄﻄﺎت () ﺗﺴﻠﺴﻞ وﻧﻤﻮذج ﻟﺴﻠﻮك ﻛﻞ ﻋﻨﺼﺮ ﺑﺂﻟﺔ اﻟﺤﺎﻟﺔ اﻟﺨﺎﺻﺔ ﺑﮫ. وﻓﻲ ھﺬا اﻟﺴﯿﺎق، ﻗﺪ ﺗﻈﮭﺮ ﻣﺸﻜﻠﺔ ﺿﻤﺎن اﻻﺗﺴﺎق ﺑﯿﻦ ﻣﺨﻄﻄﺎت ﺗﺴﻠﺴﻞ وآﻻت اﻟﺤﺎﻟﺔ اﻟﺨﺎﺻﺔ ﺑﺎﻟﻌﻨﺎﺻﺮ. ﻟﻠﺘﺤﻘﻖ اﻻﺗﺴﺎق، ﻧﻘﺘﺮح ﻧﮭﺠﺎ ﯾﻘﻮم ﻋﻠﻰ اﻟﺘﺮاﻛﯿﺐ اﻵﻟﻲ اﻟﺘﻲ ﺗﺘﯿﺢ ﻟﻨﺎ أن ﻧﻔﮭﻢ ﺗﻄﻮر ﻛﻞ ﻋﻨﺼﺮ ﻋﻠﻰ طﻮل ﺧﻂ اﻟﺤﯿﺎة ﻟﻠﻌﻨﺼﺮ. ﺗﺮﺗﻜﺰ () اﻷطﺮوﺣﺔ ﺣﻮل أﺳﺎﻟﯿﺐ اﻟﻨﻤﺬﺟﺔ واﻟﺘﺤﻘﻖ وﺗﻤﻸ اﻟﻔﺠﻮة ﺑﯿﻦ اﻟﺪراﺳﺎت اﻟﻨﻈﺮﯾﺔ ﻓﻲ اﻟﺪراﺳﺎت () اﻟﺪﻻﻟﯿﺔ واﻟﻌﻤﻠﯿﺔ اﻟﺮﺳﻤﯿﺔ ﻟﺘﻨﻔﯿﺬ ﻟﻐﺔ اﻟﺒﺮﻣﺠﺔ ﻣﻦ ﺧﻼل اﻟﺘﺤﻮﻻت اﻟﻨﻤﻮذﺟﯿﺔ. وﺗﺸﻤﻞ اﻟﺘﺤﻮﻻت  اﻷﺳﺎﺳﯿﺔ  اﻟﺜﻮاﺑﺖ اﻟﻮﺿﻌﯿﺔ، اﻟﺘﺴﻠﺴﻞ اﻟﻀﺌﯿﻞ، اﻟﺘﺴﻠﺴﻞ اﻟﺼﺎرم واﻟﺘﺤﻮل اﻟﺒﺪﯾﻞ.


:الكلمات المفتاحية
ﺗﺼﻤﯿﻢ UML ﺗﻨﺴﯿﻖ UML آﻻت Büchi OCL ATL