Soutenance mémoire
Contexte de l’étude et contributions
Les systèmes temps-réel, répartis et embarqués (TR2E) réagissent à des stimuli provenant de capteurs spécifiques. Ils fournissent la possibilité d’interagir avec leur environnement en collectant des données, ou en le contrôlant au travers de périphériques dédiés. Ces systèmes sont largement utilisés de nos jours dans des domaines d’activité variés, comme l’avionique [BW98], l’automobile [TYZP05], le militaire [PPSS00], l’ubiquitaire [NTI+04] ou encore la robotique [MNL08]. Selon le contexte d’exécution de tels systèmes, une faute, une panne ou une erreur d’exécution peut se traduire en pertes civiles ou financières. Ils doivent donc pouvoir être évalués selon différents critères afin de s’assurer qu’ils ne produiront pas d’erreur, ou dans le but de prévoir leurs réactions si l’environnement d’exécution change de façon inattendue. Ces critères sont liés à la performance, au comportement, ou encore à la gestion de ressources. Ces systèmes doivent respecter des contraintes industrielles qui sont souvent relatives à des standards. Ces derniers peuvent être spécifiques au domaine d’application du système TR2E et couvrent tous les aspects allant du processus d’ingénierie (D0178B [Sta93]) à la réalisation (ARINC653 [ari07]).
Nous nous intéressons dans le cadre de nos travaux à cette phase de réalisation, quand l’architecture de ces systèmes a déjà été établie. Nous étudions les propriétés amenées par les différents aspects des systèmes TR2E, que nous présentons ci-après
Définitions générales
Nous donnons ici une définition des systèmes qui nous intéressent dans le cadre de notre étude et qui définissent différents aspects des systèmes TR2E : les systèmes répartis, les systèmes embarqués, les systèmes temps-réel et les systèmes critiques.
Définition 1.1 (Systèmes répartis) [Gos07]
Un système réparti est un essaim d’unités de calcul échangeant des informations et travaillant de concert pour exécuter une tâche.
Ils nécessitent la mise en œuvre de mécanismes de répartition. Des infrastructures dédiées (les intergiciels) permettent de les masquer en proposant des abstractions adéquates. Ils s’appuient sur des modèles de répartition, comme les objets répartis (CORBA [OMG06a]), les appels de procédures distants (RPC [BN84]), le passage de messages (DDS [OMG07]) ou encore la mémoire partagée distribuée (TreadMarks [KCD+94]).
Définition 1.2 (Systèmes embarqués) [Bar07]
Un système embarqué est un sous-système dédié à une tâche particulière. Le nombre de tâches qu’il est en mesure d’effectuer est limité.
Il n’existe pas de modèle canonique de système embarqué : ils sont pensés, conçus et implantés pour répondre à des besoins spécifiques. Ils doivent cependant être :
– Adaptables car ils peuvent être déployés sur des éléments matériels variés ou même exotiques (processeurs spécifiques par exemple).
– Peu exigeants car leur environnement d’exécution peut être limité : contraintes économiques (répercussion sur le matériel sous-jacent), et ressources limitées.
– Fiables, car ils doivent fonctionner sans fautes ou pannes le plus longtemps possible, ou être capables de fonctionner avec des performances raisonnables en mode dégradé.
Définition 1.3 (Systèmes temps-réel) [BW01]
Un système temps-réel est un système qui doit fonctionner correctement dans un intervalle temporel spécifique en réponse à des stimuli extérieurs.
Ces systèmes doivent être déterministes et prédictibles (accès aux ressources matérielles en temps borné par exemple), de façon à pouvoir s’assurer a priori qu’ils respectent les exigences temporelles spécifiées. On distingue les échéances temporelles «dures», dont le respect est crucial pour une application, des échéances «souples» (ou «molles»).
Définition 1.4 (Systèmes critiques) [Rus94]
Un système critique est un système dont l’échec ou la panne peut avoir de lourdes conséquences financières, environnementales, ou humaines.
Ces systèmes sont évalués en fonction de leur criticité. Il en existe différents niveaux, relatifs à l’impact possible des dysfonctionnements. On distingue les catégories suivantes :
– Business critical : provoque des pertes coûteuses ;
– Mission critical : provoque l’échec de la mission ;
– Life critical : provoque des pertes humaines ou environnementales graves.
Ils doivent respecter des contraintes particulières tout au long de leur développement pour offrir des garanties sur leurs aspects critiques. Ils doivent être documentés, suivis depuis leur conception jusqu’à leur implantation et leur déploiement, testés et validés.
Nous sommes donc en mesure de définir la catégorie de systèmes que nous allons considérer dans la suite de ce manuscrit :
Définition 1.5 (Systèmes TR2E) [Hug05]
Un système TR2E est un système qui supporte une application répartie, devant respecter des contraintes temps-réel, et s’exécutant dans un environnement contraint. De tels systèmes peuvent être critiques.
Ils doivent donc être validés et vérifiés pour s’assurer de leur adéquation aux exigences et aux contraintes de leur environnement d’exécution. La notion de vérification est souvent associée à celle de validation. Les deux termes décrivent un processus assurant qu’un système correspond à des spécifications, mais avec un angle de vue différent :
Définition 1.6 (Validation et Vérification) [FL00]
– La vérification peut être associée à un processus interne (respect de normes par exemple), résumé par cette question : «Sommes-nous en train de construire correctement le système ?»
– La validation peut être associée à un processus externe (respect de contrats, comme un cahier des charges), résumé par cette question : «Sommes-nous en train de construire un système correct ?» .
Complexité d’analyse des systèmes TR2E
Les définitions précédentes ont mis en valeur les différentes contraintes qu’un système TR2E est susceptible de subir. Nous précisons ici les relations entre ces contraintes et leur impact sur les analyses qu’il est nécessaire d’effectuer.
Criticité et temps-réel Les systèmes critiques et temps-réels doivent être déterministes sur des aspects que les méthodes formelles sont à même de garantir : leur comportement doit être prédictible, reproductible, simulable et analysable (par exemple, s’il est possible de modéliser un système avec des automates déterministes, alors il est possible de garantir ce déterminisme par tautologie).
Répartition Les systèmes répartis mettent en œuvre des canaux de communication entre les différents nœuds de l’application. La gestion de ces canaux rend complexe l’analyse du système, et concerne par exemple l’autorisation d’accès aux média de transfert, ou la gestion du multiplexage de requêtes. Ces caractéristiques ont un impact fort sur les aspects temps-réels de l’application, via les délais de transmission ou les politiques de gestion des messages. Il est donc nécessaire de prendre en compte ces informations lors de l’analyse des aspects temps-réel d’un système TR2E.
Embarqué Les systèmes embarqués peuvent subir des contraintes matérielles fortes ayant une influence sur le fonctionnement de l’application : temps d’accès aux périphériques, gestion des interruptions. Ces aspects impactent les éléments temps réel d’un système TR2E et doivent être pris en compte dans l’analyse d’icelui.
En conclusion, ces systèmes TR2E sont complexes à analyser car ils amènent différents types de contraintes propres à chacun de leurs aspects (embarqués, temps-réel, répartis, critiques). Il est cependant nécessaire de les valider et de les vérifier avant de les déployer pour offrir des garanties quant à leur fonctionnement.
Validation et vérification des systèmes TR2E
Valider et vérifier de tels systèmes nécessite de pouvoir raisonner sur des informations qui leurs sont relatives, et qui doivent être structurées. La modélisation de ces systèmes le permet, et nécessite le cadre d’un processus définissant de manière rigoureuse les informations à capturer et la façon de les structurer. Ces processus mettent en œuvre des notations standardisées, spécifiques au domaine d’application.
Modélisation des systèmes TR2E : Cette étape est essentielle pour l’analyse. Traditionnellement, des approches comme l’IDM («Ingénierie Dirigée par les Modèles») centrent le processus de développement autour de la modélisation du système, traditionnellement réalisée à l’aide de langages de description d’architecture (ADL, pour Architecture Description Language) [Med00]. Ils sont dans la plupart des cas considérés comme semi-formels :
Définition 1.7 (Semi-formel)
Langage : langage standardisé dont la sémantique est définie informellement en langage naturel, et donc soumise à interprétation.
Dans notre contexte, ils permettent de spécifier des systèmes TR2E, structurant les informations, facilitant le partage ou encore l’intégration de travaux provenant de différentes équipes. Celles-ci traitent différents aspects d’un système à l’aide de spécifications séparées : spécifications fonctionnelles, matérielles ou encore temporelles. Au sein d’une même spécification, les ADLs permettent d’exprimer les contraintes du système sous forme d’attributs spécifiques. Le langage AADL [SAE08] est un ADL dédié à la modélisation de systèmes TR2E, dans le but de procéder à leur analyse. AADL aide l’ingénieur à séparer ses préoccupations, et facilite l’analyse du système en différenciant les informations temps-réel des informations embarquées ou réparties.
Cependant, si, dans le domaine des systèmes TR2E, une approche dirigée par les modèles facilite le processus de développement pour les ingénieurs, elle ne permet pas de garantir, seule, le respect des contraintes énoncées par le client.
|
Table des matières
1 Introduction générale
1.1 Contexte de l’étude et contributions
1.2 Validation et vérification des systèmes TR2E
1.3 Contributions
1.4 Organisation du mémoire
2 Etat de l’art et positionnement
2.1 Langages de description d’architecture
2.2 Méthodes formelles
2.3 Cycles de développement
2.4 Positionnement
3 AADL : un langage pivot comme support pour les analyses formelles
3.1 Eléments de langage : composants
3.2 Eléments de langage : extension de la spécification
3.3 Eléments de langage : attributs
3.4 AADL, un support pour une ingénierie dirigée par les Vérifications et les Validations
3.5 Synthèse
4 Guides et patrons de transformation depuis AADL vers les réseaux de Petri
4.1 Méthodologie pour la vérification comportementale
4.2 Définition des formalismes
4.3 Application de la méthodologie aux réseaux de Petri : patrons et règles de transformation
4.4 Réduction de la taille des réseaux générés
4.5 Synthèse
5 Spécification en Z d’un exécutif AADL : application à PolyORB
5.1 Relations entre l’exécutif AADL et sa spécification formelle
5.2 Z : une notation formelle pour la spécification
5.3 Eléments d’architecture cruciaux
5.4 Patrons Z : ORB et types de base
5.5 Patrons Z : Opérations
5.6 Patrons Z : Système d’ORBs
5.7 Combinaison des briques Z
5.8 Obligations de preuves
5.9 Approche par scenarii
5.10 Synthèse
6 Chaîne d’outils mise en œuvre
6.1 Outils : analyse du comportement à l’aide des réseaux de Petri
6.2 Outils : analyse de l’exécutif à l’aide de la notation Z
6.3 Synthèse
7 Application sur un cas d’étude
7.1 Description globale
7.2 Description semi-formelle : spécification AADL
7.3 Vérification comportementale
7.4 Connexion avec l’exécutif
7.5 Synthèse
8 Conclusion
