Informations
Directeur de thèse :
Année de début :
Fin 2010
Université :
Université Constantine 2
Soutenance
Date de soutenance :
28 Février 2017
Membres de Jury :
Mohammed Benmohammed
Allaoua Chaoui
Nabil Belala
Djamel Meslati
Zineddine Bouras
Manuscrit
Téléchargement :
Détails
Titre :
Génération d'expresions LOTOS à partir de diagrammes UML

Résumé :

Les exigences et la complexité des systèmes modernes exigent l’utilisation des meilleures techniques disponibles pour assurer et maintenir la qualité des spécifications durant le processus de développement. Les langages formels avec leur rigueur, et parmi eux LOTOS, permettent d’atteindre ce niveau de qualité. Cependant, ces langages utilisent des notations mathématiques rigides et complexes, qui génèrent souvent une faible lisibilité et une difficulté d’intégration dans les processus de développement des logiciels. D’une autre part, et contrairement aux langages formels, les langages de spécification semi-formelle sont plus faciles à comprendre et à appliquer dans le processus de développement des logiciels. En particulier le langage UML fournit un cadre normalisé pour la modélisation objet à l’aide de divers diagrammes. La notation d’UML présente des avantages confirmés et en particulier la richesse sémantique et la représentation graphique des modèles. Cependant, cette notation manque de formalisation des différents concepts, ainsi que de bases solides pour la vérification et la validation des systèmes. Par conséquent, la proposition des approches de spécifications combinant des méthodes formelles et semi-formelles, en particulier UML et LOTOS, semble être la solution la plus adéquate pour surmonter ces lacunes et pour améliorer la qualité des spécifications des systèmes modernes.

L’objectif de cette thèse est d’étudier et de mettre en œuvre des techniques qui facilitent l’utilisation conjointe du langage à objets UML et du langage formel LOTOS, en particulier pour la modélisation et la vérification des comportements dynamiques des systèmes complexes. Dans une première étape, nous proposons une approche permettant l’intégration d’UML et de LOTOS pour la modélisation et la vérification des comportements dynamiques des systèmes. Ensuite nous proposons une approche de transformation de graphes pour automatiser la transformation de modèles UML en spécifications LOTOS. Les règles et l’outil de transformation sont développés à l’aide de l’outil de méta-modélisation AToM3.


Mots clés :
Méthode semi-formelles UML Diagramme d’états-transitions Diagramme de communication Méthode Formelles LOTOS Spécification Vérification Ingénierie Dirigée par les Modèles Méta-modélisation Transformation de Graphes Grammaires de Graphes AToM3


Abstract:

The requirements and the complexity of modern systems justify the use of best available techniques to ensure and maintain the quality of specifications during the development process. Formal methods, and among them LOTOS, allow to attain this level of quality. However, these languages use rigid and complex mathematical notations, which often generate a low readability and difficulties of integration in the software development process. On the other hand, unlike formal languages, semi-formal specification languages are easier to understand and to apply. In particular UML provides a standardized framework for the object modeling using various diagrams. The UML notation has confirmed benefits especially the richness of its semantic and the graphical representation of models. However, this notation lacks of formalization and solid foundations for the verification and validation of system specifications. Hence, propose advanced specification approaches combining formal methods and semi-formal methods, particularly UML and LOTUS, is the adequate solution to overcome these deficiencies and to improve the quality of modern system specifications.

The objective of this thesis is to study and develop techniques that facilitate the joint use of the object language UML and the formal language LOTOS, particularly for modeling and verifying dynamic behaviors of complex systems. In a first step, we propose an approach for integrating UML and LOTOS for modeling and verifying dynamic behavior of systems. Then we propose a graph transformation approach to automatically transform UML models into LOTOS specifications. Transformation rules and tool are developed using the meta-modeling tool AToM3.


Keywords:
Semi-formal methods UML Statechart diagram Communication diagram Formal methods LOTOS Specification Verification Model Driven Engineering Metamodeling Graph Transformation Graph Grammars AToM3