Vérification et Validation dans l’Ingénierie Dirigée par les Modèles 

Le développement du logiciel fait face à une augmentation de la complexité des systèmes malgré l’utilisation des techniques spécifiques qu’on les appelle modèles de cycles de vie d’un logiciel comme le modèle en cascade, le modèle en V et le modèle en W. A l’instar d’autres sciences, la modélisation est de plus en plus utilisée pour maîtriser cette complexité des systèmes. L’ingénierie dirigée par les modèles (IDM), ou Model Driven Engineering (MDE) en anglais s’inscrit dans cette évolution en prônant l’utilisation systématique de modèles pour automatiser une partie des processus de développement suivis par les ingénieurs. Donc l’IDM propose de modéliser les applications à un haut niveau d’abstraction où elle se place le modèle au cœur du processus de conception puis génère le code de l’application à partir des modèles. Ainsi, l’IDM est une approche générale et ouverte qui fait suite à la proposition du standard MDA (Model-Driven Architecture) proposé par l’OMG en 2000. Elle a permis plusieurs améliorations significatives dans le développement des logiciels en permettant de se concentrer sur l’utilisation intensive des modèles et leur transformation..

Concepts de base de l’IDM

L’ingénierie Dirigée par les Modèles [33] a permis de prendre en charge la croissance de la complexité des systèmes logiciels développés où la modélisation de ces systèmes se base sur l’usage intensif de modèles. De cette manière, le développement est réalisée avec un niveau d’abstraction plus élevé que celui de la programmation classique. Cette approche permet alors d’automatiser, ou au moins de dissocier et de reporter, la part du développement qui est proprement technique et dédiée à une plate-forme d’implémentation.

L’ingénierie dirigée par les modèles (IDM) est donc une approche du génie logiciel sur laquelle le modèle est considéré comme une première présentation du système à modéliser, et qui vise à développer, maintenir et faire évoluer le logiciel en réalisant des transformations de ce modèle. Au sens large, le paradigme de l’IDM propose d’unifier tous les aspects du processus du cycle de vie en utilisant les notions de modèle et de transformation..

Dans ce qui suit, nous présentons des définitions [32] pour bien comprendre les concepts de base de l’ingénierie des modèles et les relations existants entre ces concepts.

Système : un système est un ensemble d’éléments identifiables, interdépendants, c’est-à-dire liés entre eux par des relations telles que, si l’une d’elles est modifiée, les autres le sont aussi et par conséquent tout l’ensemble du système est modifié et transformé. C’est également un ensemble borné dont on définit les limites en fonction des objectifs (propriétés, buts, projets, finalités) que l’on souhaite privilégier..

Pour modéliser un système dans le domaine de l’IDM, il est intéressant de bien comprendre et de bien maîtriser les notions de modèle et métamodèle. Nous retiendrons les définitions suivantes tirées de [11].

Modèle : Un modèle est une description abstraite d’un système construite dans un but donné. Donc, il doit pouvoir être utilisé pour répondre à des questions sur le système.

Les modèles doivent en général, respecter des contraintes décrites par un métamodèle.

Métamodèle : Un métamodèle est un modèle qui permet d’exprimer un modèle.

Le métamodèle est l’élément de structuration de modèles. Il permet de définir de façon précise les différents formalismes qui permettent de construire les modèles.

Métamodélisation

Pour manipuler un modèle, il est nécessaire de définir sa structure, sa sémantique et son langage de modélisation. Ces derniers sont représentés par un métamodèle qui illustre une définition formelle d’un modèle. En d’autres termes, le métamodèle exprime les éléments, la structure ainsi que la sémantique de ces modèles. En plus il définit la relation existante entre un modèle et le système à modéliser. La mise en oeuvre de cette relation représente alors la métamodélisation. Dans [52], la métamodélisation est une activité qui consiste à définir des métamodèles contemplatifs qui reflètent la structure statique des modèles.

Transformation de modèles

Dans l’IDM, la transformation de modèles définit la partie cruciale du processus de développement de logiciels. Généralement, elle exprime la phase de translation d’un modèle en un autre type de modèle à l’aide d’un programme de transformation écrit avec un langage dédié. Les langages de transformation de modèles peuvent être classifiés en trois catégories. La première catégorie concerne les langages de transformation déclaratifs comme QVT-Relations (QVTr) [73], Triple Graph Grammar (TGG) [57], et Transformation Nets (TNs) [82]. La deuxième catégorie regroupe les langages impératifs comme Kermeta [55]. Tandis que la troisième catégorie représente les langages hybrides regroupant les caractéristiques des deux précédentes catégories. Les langages les plus illustratifs de cette classe sont le langage ATL (Atlas Transformation Language) [43] et le langage ETL (Epsilon Transformation Language) [59]. Un processus de transformation de modèles se base sur les éléments suivants : la définition des métamodèles et leur modèles et la spécification des règles de transformation. Les métamodèles peuvent être définis avec des langages de métamodélisation comme MOF [71], Ecore [16], KM3 (Kernel MetaMetaModel) [54]. Les modèles sont calculés par une instanciation de leurs métamodèles.

• Transformation : Une transformation de modèles est une génération automatique d’un modèle cible à partir d’un modèle source selon la définition de la transformation.
• Définition de transformation : C’est un un ensemble de règles de transformation qui décrivent comment un modèle source peut être transformé en un modèle cible.
• Règle de transformation : Une règle de transformation est une description de la manière dont une ou plusieurs constructions dans un langage source peuvent être transformées en une ou plusieurs constructions dans un langage cible.

Pourquoi la transformation de modèles?

La transformation de modèles joue un rôle fondamental dans le développement des logiciels et vise des objectifs divers comme la automatise la génération automatique du code, la translation de modèle, la migration, et l’ingénierie inverse .

Génération automatique du code 

La génération de code est l’une des principales activités dans la technologie de l’IDM qui a été utilisée fréquemment dans la littérature de recherche à des buts différentes. En général, l’objectif est de transformer un modèle vers un un modèle spécifique représentant un code source pouvant être exécuté. Un exemple typique d’une telle transformation de modèles, qui a été utilisée fréquemment dans la littérature de recherche est la transformation de modèles Petrinet2Java. Son but est de convertir un modèle de réseau de Petri à un code exécutable Java.

Translation de modèle

La translation de modèle est une transformation d’un modèle à un modèle équivalent mais dans une différente représentation. Une des raisons pour l’utilisation de la translation de modèle est de faciliter l’interopérabilité. Il est souvent souhaitable d’utiliser et d’échanger des modèles entre les différents outils de modélisation, et même entre les différents langages de modélisation. Un exemple typique est la traduction de quelques outils de représentation spécifique de modèles UML dans XMI (et vice versa), langage de type XML et qui est un standard d’OMG pour l’échange de modèles. Cela facilite l’échange des modèles UML entre les différents outils de modélisation UML [76].

Migration de modèles 

Une autre utilisation de la transformation de modèles est la migration de modèles. La migration peut être définit comme une transformation d’un modèle écrit dans un langage en un autre modèle écrit dans un autre langage, en gardant le même niveau d’abstraction des modèles. Par exemple, l’évolution du langage (EJB2 2.0) vers une version plus récente telle que (EJB3 3.0), nécessite de migrer les modèles vers une version plus récente à l’aide d’une transformation de modèles qui englobe et automatise cette migration au lieu de migrer chaque modèle individuellement.

Ingénierie inverse

L’ingénierie inverse est un autre exemple d’une transformation de modèles. Elle est l’inverse de la génération de code, et permet de comprendre la structure du programme. Prenant le code source en entrée, elle permet de construire un modèle mental ou visuel (par exemple un modèle UML) à un niveau supérieur d’abstraction, afin de faciliter la compréhension du code et connaître comment il est structuré. L’ingénierie inverse est utilisée pour l’adaptation des applications vers les nouvelles technologies.

Table des matières

Introduction Générale  
Chapitre 1 Ingénierie Dirigée par les Modèles  
1.1 Introduction
1.2 Concepts de base de l’IDM
1.2.1 Métamodélisation
1.2.2 Transformation de modèles
1.3 Pourquoi la transformation de modèles?
1.3.1 Génération automatique du code
1.3.2 Translation de modèle
1.3.3 Migration de modèles
1.3.4 Ingénierie inverse
1.4 Les approches de transformation
1.4.1 Transformation de modèle à modèle
1.4.1.1 Approches manipulant directement les modèles
1.4.1.2 Approches relationnelles
1.4.1.3 Approches basées sur la transformation de graphes
1.4.1.4 Approches dirigées par la structure
1.4.1.5 Approches hybrides
1.4.2 Transformations Modèle à code
1.4.2.1 Approches basées sur le parcours de modèles
1.4.2.2 Approches basées sur les templates
1.5 Critères de classification des approches de transformation de modèles
1.5.1 Règles de transformation
1.5.2 Portée des règles
1.5.3 Relation entre le modèle source et le modèle cible
1.5.4 Ordonnancement des règles
1.5.5 Organisation des règles
1.5.6 Traçabilité
1.5.7 Directivité ou réversibilité
1.6 Conclusion
Chapitre 2 Les Méthodes Formelles  
2.1 Introduction
2.2 Pourquoi utiliser les méthodes formelles?
2.3 Classification des Méthodes Formelles
2.3.1 Classification de J. Wing
2.3.1.1 Méthodes Orientées propriétés
2.3.1.2 Méthodes Orientées Modèles
2.3.2 Classification de Meyer
2.3.2.1 Méthodes logiques
2.3.2.2 Méthodes dynamiques
2.3.2.3 Méthodes ensemblistes
2.3.2.4 Méthodes hybrides
2.3.3 Autre classification
2.3.3.1 Méthodes de Spécification Formelle
2.3.3.2 Méthodes de Vérification Formelle
2.3.4 Comparaison des classifications
2.4 Conclusion
Chapitre 3 Vérification et Validation dans l’Ingénierie Dirigée par les Modèles 
3.1 Introduction
3.2 Vérification dans la transformation de Modèles
3.3 Techniques de Vérification
3.3.1 Techniques semi-formelles
3.3.2 Techniques formelles
3.3.2.1 Vérification formelle par preuve
3.3.2.2 Vérification formelle par « Model checking »
3.4 Validation dans l’IDM
3.5 Techniques de validation
3.5.1 Techniques semi-formelles
3.5.2 Techniques formelles
3.5.2.1 Validation formelle par la méthode B
3.6 Conclusion
Chapitre 4 Outils d’expérimentation 
4.1 Introduction
4.2 Outils de l’IDM
4.2.1 Langage Ecore
4.2.2 Langage OCL
4.2.3 Langage QVT
4.2.3.1 La partie déclarative
4.2.3.2 La partie impérative
4.3 Outil formel : Assistant de preuve Coq
4.3.1 Les termes de base
4.3.2 Types inductifs
4.3.3 Fonctions et Fonctions récursives
4.3.4 Théorème et Preuve
4.4 Conclusion
Chapitre 5 Transformation de Modèles : Etude de cas 
5.1 Introduction
5.2 Exemple d’étude de cas
5.2.1 Diagramme d’états-transitions
5.2.1.1 État
5.2.1.2 État Simple
5.2.1.3 État Final
5.2.1.4 État Composite
5.2.1.5 Pseudo-État
5.2.1.6 Sous-machine à états
5.2.1.7 Transition
5.2.1.8 Région
5.2.2 Réseau de Petri
5.3 Approche IDM
5.3.1 Métamodélisation
5.3.1.1 Spécification du métamodèle source
5.3.1.2 Spécification du métamodèle cible
5.3.2 Processus de transformation de modèles
5.4 Exécution de la transformation
5.4.1 Exemple : Système ATM
5.4.2 Exemple : Comportements de la montre
5.5 Conclusion
Chapitre 6 Mise en œuvre de la vérification et de la validation 
6.1 Introduction
6.2 Vue générale sur notre approche
6.3 Mise en œuvre de la vérification
6.3.1 Spécification des propriétés du métamodèle source
6.3.2 Spécification des propriétés du métamodèle cible
6.4 Mise en œuvre de la validation
6.4.1 Spécification en langage Gallina
6.4.1.1 Spécification des métamodèles source et cible
6.4.1.2 Spécification des modèles source et cible
6.4.1.3 Spécification des règles de transformation
6.4.2 Formalisation de théorème
6.4.3 Preuve de théorème
6.5 Conclusion
Conclusion Générale

Ingénierie Dirigée par les ModèlesTélécharger le document complet

Télécharger aussi :

Laisser un commentaire

Votre adresse e-mail ne sera pas publiée. Les champs obligatoires sont indiqués avec *