Sommaire: UML et model checking
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
Extrait du mémoire UML et model checking
CHAPITRE I : UML & Génie logiciel
Le phénomène de crise de logiciel a été identifié, depuis les années 60s, dans la communauté de génie logiciel. Aujourd’hui après quarante ans, cette crise n’est pas totalement résolue. Ceci est essentiellement dû à la croissance des demandes de logiciel. En effet, l’immense utilisation de logiciel en pratique, la réalisation et la maintenance des logiciels déjà existants font de ces derniers des produits très coûteux.
La production du logiciel fait appel à beaucoup de technologies et de méthodologies dont la majorité n’ont pas atteint le stade de maturité et de stabilité. Ceci fait de cette production un processus dont l’approche est difficile à unifier.
Afin de répondre aux demandes de logiciel, qui sont croissantes, tout en augmentant leur productivité, certains efforts ont été inventés pour améliorer les techniques de développement de logiciel. Les méthodologies d’analyse et de conception dont l’approche orienté objet est la plus importante, les paradigmes de programmation et leurs langages proposés, les environnements du travail et les outils CASE, tous sont des variantes de ces efforts.
L’unification des efforts et des travaux similaires, est bien sûr une ambition toujours établie dans le monde d’informatique. UML (Unified Modeling Language), comme un excellant exemple, est un grand pas vers l’unification des méthodologies d’analyse et de conception orienté objet. Ce langage est devenu récemment, le standard incontournable de la modélisation. Ainsi, il s’infiltre, jour après jour, dans tous les secteurs de développement d’outils et de produits informatiques.
Dans ce chapitre, nous rappelons quelques définitions et quelques concepts sur; le génie logiciel, les critères de qualité d’un produit informatique, le cycle de vie d’un logiciel et ses modèles, les méthodes d’analyses et de conceptions fonctionnelles et objets. Puis on fait un survol sur le langage unifié de modélisation UML. À la fin du présent chapitre, on expose brièvement le processus unifié qui constitue un cadre général pour développer des logiciels en utilisant la notation UML.
………..
Si le lien ne fonctionne pas correctement, veuillez nous contacter (mentionner le lien dans votre message)UML et model checking (1.5 Mo) (Rapport PDF)
