Méthodologie de conception de systèmes temps réel et distribués en contexte UML/SysML

L’émergence d’un consensus : UML

   L’Unified Modeling Language (UML) [UML] [BOO 03] est un langage pour documenter et spécifier graphiquement tous les aspects d’un système à logiciel prépondérant. L’ambition des promoteurs d’UML est de fédérer en une seule notation les meilleures caractéristiques des différents langages de modélisation qui utilisent le paradigme objet. En tant que standard de l’OMG (Object Management Group) [OMG], UML jouit d’une popularité sans précédent à la fois dans le monde industriel et académique. UML se veut être un médium, sous forme de modèle graphique, servant à harmoniser les différents acteurs concourant à la réalisation d’un système, et à garantir la cohérence et la qualité de la conception.

UML présente l’avantage de pouvoir se décliner sous forme de « profils » spécialisés en fonction des domaines d’application considérés (pour le temps réel par exemple [OMG 05] [OMG 07]). Ces profils permettent aussi de combler des lacunes d’UML en termes de sémantique pour servir de pivot à des outils de validation (dans notre cas la vérification formelle). Les outils dédiés aux profils « UML temps réel », c’est-à-dire aux personnalisations d’UML destinées à mieux prendre en compte le caractère réactif de ces systèmes mais aussi l’expression d’exigences et de mécanismes temporels, pêchent par le volet méthodologique. La manière d’utiliser le profil est insuffisamment et informellement documentée (manque de modèles génériques par exemple). De surcroit, l’objectif de traçabilité des exigences si souvent affiché n’est que partiellement atteint dans la mesure où certaines exigences doivent être décrites hors du modèle UML et reliées de manière ad-hoc et non automatisable à la validation de modèle.

Une qualité importante du langage UML est de se construire autour des fonctions que le système doit offrir (c’est-à-dire les exigences fonctionnelles) ; ce sont les cas d’utilisations. Ce concept permet d’avoir un vue opérationnelle du système en termes de mécanismes à concevoir, ce qui convient bien pour décrire des solutions logicielles (architectures, comportement). Mais UML est mal adapté pour décrire le problème à résoudre – l’objet même du cahier des charges – les exigences non-fonctionnelles (dans le domaine temporel, par exemple, le temps de sortie des trains d’atterrissage d’un avion). Or ces exigences non-fonctionnelles influencent toutes les définitions des mécanismes définis dans des cas d’utilisations.

Les réponses apportées par l’ingénierie des exigences

   Pour palier le problème de l’expression des exigences non-fonctionnelles, l’ingénierie des exigences [LAM 06] [HUL 04] définit le concept d’objectif et permet de formuler plus précisément les exigences, fonctionnelles ou non-fonctionnelles. L’utilisation des techniques de modélisation orientées « objectifs » [LAM 06] permet d’élaborer le cahier des charges d’un système de manière rigoureuse. En effet, à partir d’un objectif donné, en se posant la question du « pourquoi », on peut identifier des objectifs de haut niveau à satisfaire ; en se posant la question du « comment », on peut identifier l’ensemble des mécanismes qui vont permettre d’atteindre les objectifs en question. Dans ce contexte, l’OMG a récemment normalisé SysML [SysML] amenant avec lui, entre autres concepts, l’idée de pouvoir formuler des exigences au moyen d’un diagramme d’exigences. Ceux-ci concourent à assurer, à des fins documentaires, un suivi de ces exigences dans le cycle de développement du système par la construction d’une matrice de traçabilité. Notons néanmoins que dans les premiers outils disposant de plug-ins SysML (par exemple, TAU G2.3.1 [TAU]), les exigences sont décrites de manière totalement informelle et sans lien automatisé avec les fonctionnalités de validation de modèles.

Exigences posées par les STR

[HUL 04] distingue deux classes d’exigences dans un système :
• Les exigences fonctionnelles représentent les différentes fonctionnalités que devra satisfaire le système et correspondent à l’aspect opérationnel de ce système. En matière de vérification formelle, on associe généralement ce type d’exigences à des « propriétés générales » telles que l’absence de blocage non désiré (« deadlock »), l’absence de fonctionnement cyclique infini non désiré (« livelock ») ou encore la possibilité de revenir à l’état initial.

• Les exigences non-fonctionnelles correspondent aux critères de qualité attendus du système, par exemple en termes de performances temporelles. A titre d’exemple, pensons aux différentes garanties temporelles (par exemple des délais maximum ou minimum) que doit satisfaire un système temps réel. Dans le domaine du temps réel, les exigences non-fonctionnelles temporelles se répartissent plus précisément en deux catégories [WAH 94] :

• Les exigences où le temps est exprimé de manière qualitative (ou logique). On ne considère alors qu’un ordre partiel entre événements (par exemple un ascenseur doit être à l’arrêt pour que la porte s’ouvre).

• Les exigences où le temps est exprimé de manière quantitative. On considère dans ce cas l’ordre des événements mais aussi les distances temporelles entre ces derniers (par exemple la porte d’un ascenseur doit s’ouvrir deux secondes après l’arrêt de la cabine). Dans le domaine de la vérification formelle d’exigences temporelles quantitatives, il existe deux manières de représenter le temps [ALU 94] :

• En l’exprimant de manière discrète en considérant le temps comme une horloge préalablement définie. Le modèle temporel correspondant est donc basé sur une horloge discrète. Cette expression du temps peut s’avérer être un facteur limitant : par exemple, si un système a des constantes de temps variant de 1 à 10000, considérer une horloge discrète de granularité 1 engendre un nombre d’états prohibitif dans le modèle. D’autre part, l’utilisation du temps discret, par la construction d’une horloge discrète, suppose la connaissance exacte de la durée totale d’exécution du système, c’est-à-dire des durées des diverses opérations à réaliser.

• En l’exprimant de manière continue en considérant le temps comme une succession d’horloges et de frontières temporelles. Pour cela on construit un modèle plus fin où l’on peut utiliser différentes horloges pour spécifier le comportement temporel du système. Outre la meilleure prise en compte des différentes granularités temporelles du système, cette représentation du temps permet aussi de prendre en compte une incertitude sur les contraintes temporelles du système (durée des tâches, des communications). Ce mémoire se focalise sur les exigences non-fonctionnelles temporelles quantitatives où le temps est représenté de manière continue. Ces dernières correspondent à des propriétés de vivacité1 bornée [ALU 93] issues de la classe des propriétés de sûreté2 (« safety ») liées à la correction partielle du système. Les propriétés de vivacité bornée se voient affecter une date butoir pour laquelle la propriété n’est plus satisfaite [ALU 93] ; ceci implique donc que le système doit être borné temporellement pour pouvoir être vérifié.

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

Télécharger le rapport complet