Langage de description d’exigences non-fonctionnelles temporelles

Table des matières

Chapitre I. Introduction
1. Développer des systèmes temps réel fiables
2. L’émergence d’un consensus : UML
3. Les réponses apportées par l’ingénierie des exigences
4. Contributions apportées dans ce mémoire
5. Organisation du mémoire
Chapitre II. Contexte et positionnement des travaux
1. Les systèmes temps réel (STR)
1.1. Exigences posées par les STR
1.2. Méthodologies de conception de STR
1.2.1. Avant UML
1.2.2. Les méthodologies orientées UML
1.2.3. Les méthodes formelles dans la conception et la validation des STR
2. Systèmes temps réel et distribués (STRD)
2.1. Les exigences temporelles liées à la Qualité de Service des STRD
2.2. Méthodologies de conception de STRD
3. TURTLE (Timed UML and RT-LOTOS Environment)
3.1. Un profil dédié à la vérification de systèmes temps-réel et distribués
3.1.1. La sémantique TURTLE : le langage RT-LOTOS
3.1.2. Les diagrammes UML TURTLE
3.1.3. Un profil outillé
3.1.4. Positionnement du profil TURTLE
3.2. Méthodologie présentée en [APV 06]
4. Conclusion
Chapitre III. Proposition d’une méthodologie
1. Vue d’ensemble de la méthodologie
1.1. Définition informelle
1.2. Langage de description d’une méthodologie
1.2.1. Principe
1.2.2. Définition formelle
1.2.3. Méta-modèle
2. Guide de lecture
3. Vérification formelle d’exigences temporelles de modèles en contexte UML/SysML
3.1. Traitement des exigences
3.1.1. Recueil des exigences
3.1.2. Hypothèses de modélisation
3.1.3. Spécification des exigences
3.2. Analyse
3.3. Conception
3.4. Vérification formelle des exigences
4. Spécialisation dans le domaine des protocoles
4.1. Les règles de traitement des exigences
4.1.1. Exigences liées au type de protocoles envisagés et à la qualité de service
4.1.2. Hypothèses de modélisation
4.1.3. Les règles liées à la phase d’analyse
4.2. Les règles liées à la phase de conception
5. Conclusion
Chapitre IV. Langage de description d’exigences non-fonctionnelles temporelles
1. Etat de l’art et positionnement de nos travaux
2. Définition d’un langage de description d’exigences temporelles
2.1. Formalisation d’exigences temporelles SysML
2.1.1. Exemple de diagramme d’exigences
2.1.2. Définitions formelles
2.1.3. Méta-modèle UML
2.2. Timing Requirement Description Diagram (TRDD)
2.2.1. Exemple
2.2.2. Définition formelle
2.2.3. Méta-modèles UML
2.2.4. Pouvoir d’expression des TRDD
3. Composition d’exigences
3.1. Les concepts de composition et satisfaction
3.2. Proposition d’extension des diagrammes d’exigences
3.3. Définition formelle
4. Conclusion
Chapitre V. Vérification formelle d’exigences temporelles sur le modèle de conception
1. Approches de vérification des exigences temporelles
1.1. La vérification par contrôle de modèles
1.2. Vérification guidée par les observateurs
1.2.1. Mise en œuvre d’observateurs dans le simulateur Véda
1.2.2. Observateurs de machines synchrones
1.2.3. Observateurs pour les systèmes auto-validés
1.2.4. Le langage GOAL
1.2.5. Les observateurs du profil UML OMEGA
1.2.6. Méthodes de surcharge
1.2.7. Diagrammes de contexte et d’observation
2. Génération d’observateurs TURTLE à partir d’exigences temporelles
2.1. Construction d’un observateur TURTLE
2.1.1. Définition d’un observateur TURTLE
2.1.2. Méta-modèle UML d’une Tclass observateur
2.2. Vue d’ensemble
2.3. Traduction d’un TRDD vers le diagramme d’activités de l’observateur
2.3.1. Tables de traductions
2.3.2. Méta-modèles UML du diagramme d’activités d’un observateur
2.3.3. Algorithmes de construction du comportement de l’observateur
2.3.4. Exemples
2.3.5. Algorithmes de construction du comportement complet de l’observateur
2.4. Intégration de l’observateur dans le modèle
2.4.1. Définition des points d’observations
2.4.2. Construction du modèle observable : principe
2.4.3. Méta-modèle UML du modèle couplé avec l’observateur
2.4.4. Algorithme d’insertion d’un observateur dans le système à observer
3. Discussion sur l’approche de vérification guidée par les observateurs
3.1. Hypothèses
3.2. Placement des points d’observations
3.3. Vers une implantation complète de l’approche
4. Conclusion
Chapitre VI. Application : le projet SAFECAST
1. Le projet SAFECAST
1.1. Réseau sans fil : le médium PMR
1.2. Revue de travaux sur la modélisation et la vérification de protocoles de sécurité
1.3. Pourquoi utiliser TURTLE dans le projet SAFECAST
2. Exigences, architecture et services considérés
2.1. Exigences temporelles d’un protocole de sécurité
2.2. Architecture générique
2.2.1. Services de diffusion sécurisée
2.2.2. Services de gestion des groupes
3. Etude du délai d’établissement d’une communication chiffrée
3.1. Traitement des exigences
3.1.1. Recueil des exigences
3.1.2. Hypothèses de modélisation
3.1.3. Spécification d’une exigence temporelle.
3.2. Modèle de conception pour la fonctionnalité Génération et Distribution des clés (Key_Renewal)
3.3. Construction des observateurs
4. Contributions et résultats
5. Conclusion
Chapitre VII. Conclusions et perspectives
1. Bilan des contributions
2. Perspectives
2.1. Enrichir les descriptions d’exigences non-fonctionnelles temporelles
2.2. Extension de la méthodologie dans les phases de déploiement et de codage
2.3. Perspectives liées au projet SAFECAST
Références