Une approche IDM du transformation du modèle ecore vers event-b.

• Résumé
  
• Remerciements
  
• Dédicaces
  
• Table des matières
  
• Table des figures
  
• Liste des tableaux
  
• Introduction générale
  
• Première partie
  
• Etat de l'art
  
• 1 Ingénierie dirigée par les modèles
  
  • 1.1 Introduction
    
  • 1.2 L'Ingénierie dirigée par les modèles(IDM)
    
    • 1.2.1 Principe et concepts généraux de l'IDM
      
    • 1.2.2 L 'Approche MDA (Model Driven Architecture)
      
  • 1.3 Transformation de modèles
    
    • 1.3.1 Principe géneral d'une transformation
      
    • 1.3.2 Types de transformation
      
    • 1.3.3 Taxonomies des transformations
      
    • 1.3.4 Paradigmes de transformation
      
      • 1.3.4.1 Transformation Modèle vers Modèle
        
      • 1.3.4.2 Transformation Modèle vers Code
        
  • 1.4 Langage de transformation de modèles ATL
    
    • 1.4.1 Vue d'ensemble sur la transformation ATL
      
    • 1.4.2 Présentation d'ATL
      
  • 1.5 La plateforme de modélisation sous Eclipse
    
    • 1.5.1 Eclipse Modeling Framework (EMF)
      
    • 1.5.2 XML Metadata Interchange (XMI)
      
  • 1.6 Le langage de génération de code Xpand
    
    • 1.6.1 Structure générale d'un template Xpand
      
  • 1.7 Le langage Check pour la vérification de contraintes
    
  • 1.8 MWE (Modeling Workflow Engine)
    
  • 1.9 Conclusion
    
• 2 Méta-modélisation :Le méta-modèle
  
• ECore
  
  • 2.1 Introduction
    
  • 2.2 La méta-modélisation
    
  • 2.3 Les langages de méta-modélisation
    
    • 2.3.1 MOF (Meta Object Facility)
      
    • 2.3.2 ECore
      
  • 2.4 Le Méta-modèle ECore
    
    • 2.4.1 Noyau d'ECore
      
    • 2.4.2 Caractéristiques structurelles
      
      • 2.4.2.1 EAttribute
        
      • 2.4.2.2 ERéférence
        
    • 2.4.3 Caractéristiques comportementales
      
    • 2.4.4 Classificateurs
      
      • 2.4.4.2 Types de données
        
      • 2.4.4.3 Types énumérés
        
      • 2.4.4.4 Package
        
  • 2.5 Etude de cas
    
    • 2.5.1 Présentation informelle
      
    • 2.5.2 Spécification du système bancaire en ECore
      
  • 2.6 Conclusion
    
• 3 La méthode formelle Event-B
  
  • 3.1 Introduction
    
  • 3.2 Quelques langages formels
    
    • 3.2.1 Le langage Z
      
    • 3.2.2 La méthode B
      
    • 3.2.3 La méthode Event-B
      
  • 3.3 Modèle Event-B
    
    • 3.3.1 Structure d'une Machine
      
    • 3.3.2 Structure d'un Contexte
      
    • 3.3.3 Structure d'un Evénement
      
      • 3.3.3.1 Les différentes formes des événements
        
  • 3.4 Exemple de machine en Event-B
    
  • 3.5 RODIN : l'outil support d'Event-B
    
  • 3.6 Conclusion
    
• Deuxième partie
  
• Contribution
  
• 4 Une approche IDM pour la généra-
  
• tion de modèle Event-B à partir de
  
• modèle ECore
  
  • 4.1 Introduction
    
  • 4.2 Les méta-modèles de notre approche
    
    • 4.2.1 Méta-modèle Event-B
      
      • 4.2.1.1 Méta-Classe de Context
        
      • 4.2.1.2 Méta-Classe Machine
        
      • 4.2.1.3 Méta-Classe Event
        
      • 4.2.1.4 Vue d'ensemble sur le méta-modèle Event-B
        
      • 4.2.1.5 Les règles de cohérences sous forme d'OCL (.chk)
        
    • 4.2.2 Méta-modèle ECore
      
      • 4.2.2.1 Les règles de cohérence du méta-modèle ECore sous forme d'OCL (OCLi-nECore)
        
  • 4.3 Formalisation en Event-B
    
    • 4.3.1 Formalisation du concept EPackage en Event-B
      
    • 4.3.2 Formalisation du concept EClass en Event-B
      
    • 4.3.3 Formalisation du concept EEnum en Event-B
      
    • 4.3.4 Formalisation du concept EAttribute en Event-B
      
    • 4.3.5 Formalisation du concept EReference en Event-B
      
    • 4.3.6 Formalisation du concept EOperation en Event-B
      
  • 4.4 Transformations de modèle ECore vers Event-B en utilisant une approche IDM (Ingénierie Dirigée par les Modèles).
    
    • 4.4.1 Transformation de modèles M2M
      
      • 4.4.1.1 Exemple des règles en ATL
        
    • 4.4.2 Transformation de modèle M2T
      
      • 4.4.2.1 Présentation de la transformation M2T
        
      • 4.4.2.2 Modèle Event-B en texte : Extraction via Xpand
        
      • 4.4.2.3 Le moteur de validation et de génération de code Ada
        
      • 4.4.2.4 Exemple d'utilisation: Système bancaire(Bank)
        
  • 4.5 Vérification formelle par l'outil Rodin
    
    • 4.5.1 Preuves d'une machine
      
  • 4.6 Conclusion
    
• Conclusion et perspectives
  
• Appendices