leila-TTG
Memoire Complet♣ Contenu du memoire
INTRODUCTION GENERALE
CHAPITRE I : UML & GENIE LOGICIEL
1. LE GENIE LOGICIEL
1.1 DEFINITION
1.2 CRITERES DE QUALITE D’UN PRODUIT LOGICIEL
1.3 CYCLE DE VIE D’UN LOGICIEL
1.4 MODELE DE CYCLE DE VIE D’UN PRODUIT LOGICIEL
1.4.1 Modèle de cycle de vie en cascade
1.4.2 Modèle de cycle de vie en V
1.4.3 Modèle de cycle de vie en spiral
1.4.4 Modèle de cycle de vie par Incréments
1.5 METHODES D’ANALYSE ET DE CONCEPTION
1.5.1 Méthodes fonctionnelle descendante :
1.5.2 Méthodes orientées objet
2. L’APPROCHE OBJET
2.1 L’OBJET
2.2 LES CLASSES
2.3 L’INSTANCIATION
2.4 LES RELATIONS ENTRE ASSOCIATIONS
2.5 LES MESSAGES & LA SYNCHRONISATION :
2.6 GENERALISATION ET SPECIALISATIONS
3. UNIFIED MODELING LANGUAGE
3.1 DEFINITION
3.2 LES VUES D’UML
3.3 LES ELEMENTS DU MODELE
3.4 MECANISMES GENERAUX
3.5 LES DIAGRAMMES
3.5.1 Diagrammes structurels
3.5.2 Les diagrammes comportementaux
3.5.3 Diagramme d’interaction (interaction diagram)
4. LE PROCESSUS UNIFIE
4.1 DEFINITION
4.2 VIE DU PROCESSUS UNIFIE
4.3 LES TACHES D’UN CYCLE DE VIE D’UP
4.4 LES PHASES D’UN CYCLE DE VIE D’UP
CHAPITRE II : DIAGRAMMES D’ETATS-TRANSITIONS & TRAVAUX DE FORMALISATION
1. DIAGRAMME D’ETATS-TRANSITIONS
1.1 DEFINITION
1.2 ETATS
1.3 EVENEMENTS
1.4 TRANSITIONS
1.5 ETATS ET TRANSITIONS AVANCES
1.5.1 Activités d’entrée/sortie
1.5.2 Transitions Internes
1.5.3 Activités-Do
1.5.4 Evénements déférés
1.5.5 Sous-machine
1.6 SOUS-ETATS
1.6.1 Sous-état séquentiel
1.6.2 Sous-état Orthogonal
1.6.3 Etat Historique
1.7 POINT DE CHOIX
1.7.1 Point de Jonction
1.7.2 Point de Décision
1.8 TRANSITION COMPLEXES
1.9 SEMANTIQUE DE MACHINE D’ETAT
2. TRAVAUX DE FORMALISATION DE DIAGRAMME D’ETATS TRANSITIONS.
2.1 LES MODELES MATHEMATIQUES
2.2 LES SYSTEMES DE REECRITURE
2.3 LES APPROCHES DE TRANSLATIONS
CHAPITRE III : LOGIQUE DE REECRITURE, MAUDE ET MODEL-CHECKING
1. LES METHODES FORMELLES
1.1 PREUVE DE THEOREME
1.2 EXPLORATION DE L’ENSEMBLE DES ETATS
2. LOGIQUE DE REECRITURE
2.1 PRESENTATION
2.2 CONCEPTS DE BASES DES THEORIES
3. LANGAGE MAUDE
3.1 PRESENTATION
3.2 MODULES FONCTIONNELLES
3.3 MODULES SYSTEMES
3.4 SPECIFICATIONS ORIENTEES OBJET EN MAUDE
3.5 EXECUTION DU MAUDE
3.6 COMMANDES MAUDE
4. MODEL-CHECKING ET MAUDE LTL MODEL-CHECKER
4.1 MODEL CHECKING
4.2 STRUCTURE DE KRIPKE ET LTL
4.3 MAUDE LTL MODEL-CHECKER
CHAPITRE IV : METHODE DE MODEL-CHECKING DES MODELES UML EN UTILISANT MAUDE
1. PRESENTATION DE LA METHODE
1.1 ELABORATION DU MODELE UML
1.2 TRANSLATION DU MODELE UML
1.3 DEFINITION DES PROPRIETES A VERIFIER
1.4 VERIFICATION DU MODELE
2. EXEMPLE I : PROBLEME DE DINER DES PHILOSOPHES
2.1 MODELE UML POUR LE PROBLEME DE DINER DES PHILOSOPHES
2.2 TRANSLATION DU MODELE UML
2.3 DEFINITION DES PROPRIETES A VERIFIER
2.4 VÉRIFICATION DU MODÈLE
3. EXEMPLE II : ATM-BANK
3.1 MODÈLE UML ATM-BANK
3.2 TRANSLATION DU MODELE UML
3.3 VERIFICATION DES COLLABORATIONS
REFERENCES
Memoire Complet
