Mise en avant de l’approche, éléments étudies

Aspect sûreté

Les aspects sûreté du cas d’étude integrated mettent en pratique les éléments suivants de notre approche : 1. L’utilisation de patrons de modélisation dédiés à la spécification d’architectures partitionnées et de leur politique de recouvrement. 2. La validation de l’architecture partitionnée et de ses mécanismes de recouvrement d’erreurs. 3. La génération automatique de l’implantation en respectant les mécanismes de sûreté spécifiés. 4. La validation du syst`eme généré et de l’implantation de sa politique de recouvrement par une analyse comportementale de l’exécution. 5. Le respect du standard de certification DO178B par une analyse de couverture de code.

Aspect sécurité

Le cas d’étude dédié à la sécurité met en valeur notre approche par : 1. L’utilisation des patrons de modélisation pour la spécification des niveaux de sécurité et de leurs mécanismes associés. 2. La validation de l’isolation des niveaux de sécurité par analyse de modèes AADL. 3. La génération automatique de l’implantation et de ses mécanismes de sécurité. 4. La validation de l’implantation des mécanismes de sécurité par une analyse du syst`eme à l’exécution. 5. Une analyse de couverture de code, élément requis par les standards applicables aux syst`emes critiques (tel DO178B). 

Plan de l’étude

Dans un premier temps, chaque cas d’étude est présenté séparément (sections 6.2 et 6.3). Nous décrivons le contexte d’utilisation de ces syst`emes, détaillons leurs exigences et les modèes AADL associés. Chacune de ces sections abordent les outils de certification utilisés pour analyser leur exécution (validation mécanismes de sûreté pour le cas d’étude « integrated » , supervision de l’isolation des données pour le cas d’étude MILS). La section 6.4 rapporte les taux de couverture de code des composants générés (noyau, partitions) dans chaque cas d’étude et met en relation les 181 Mise en avant de l’approche, éments Chapitre 6. Cas d’études résultats obtenus avec l’approche globale. En particulier, il explique la pertinence de la génération de code pour obtenir un haut niveau de couverture de code. Enfin, la section 6.5 présente une analyse de l’empreinte mémoire des applications générées et compare les résultats avec les travaux existants. 

Cas d’étude « integrated avionics » : gestionnaire de pilotage

Les sections suivantes décrivent le cas d’étude « integrated » , dédié à la sûreté. Il présente ces spécifications sous une forme textuelle, leur traduction à l’aide de nos patrons de modélisation et la validation des exigences de sûreté à partir du modèe. 6.2.1 Introduction Ce cas d’étude définit une application avionique de contrˆole de vol, dirigeant la trajectoire de l’avion, g`ere le matériel de vol, affiche les informations de navigation au pilote et détecte les erreurs potentielles. Son architecture suit la philosophie « Integrated Modular Avionics » (IMA) qui consiste à séparer les fonctions dans des partitions pour les isoler les unes des autres. Aper¸cu de l’architecture L’architecture proposée comprend 6 partitions inter-connectées, chacune remplissant une fonction bien définie : 1. Le Flight Manager calcule le plan de vol de l’avion. 2. Le Flight Director g`ere le matériel contrˆolant l’avion et répond aux demandes de contrˆole du contrˆole de vol (partition 1 — Flight Manager ). 3. Le Page Content Manager contient toutes les informations potentiellement affichables sur l’écran du pilote et les organise en différentes pages. Les informations proviennent de la partition 1 (Flight Manager ). 4. Le Display Manager affiche une page d’information de navigation parmi celles disponibles au sein de la partition 3. 5. Le Hardware Display contrˆole le périphérique affichant les pages (carte vidéo + écran) et affiche la page choisie par la partition 4. 6. Le Warning Annunciation Manager détecte de erreurs potentielles survenant lors du vol. Les connections entre les partitions utilisent le principe de la mémoire partagée : aucune valeur n’est mise en attente. Ce concept de communication correspond à celui des sampling port du standard ARINC653. Chaque partition est isolée temporellement et spatialement. Origine de ce cas d’étude Cet exemple a été défini dans un rapport technique [45] publié par le Software Engineering Institute pour la conception et l’analyse de syst`emes avioniques avec le standard AADL. Un rapport [45] détaille les patrons de modélisation utilisés ainsi qu’une analyse des flots de communication inter-partitions

 Cas d’étude « integrated avionics »

gestionnaire de pilotage (vérification que la latence de communication est inférieure au temps de communication demandé par le concepteur d’application). La version initiale de ce modèe a été créé en 2007. Il utilise donc la premi`ere version du langage AADL (la seconde version ayant été publiée un an apr`es), peu adapté à la spécification d’architecture partitionnée (composants et propriétés manquants — par exemple les virtual processor). Probl`emes de la spécification initiale En particulier, cette premi`ere version de la spécification ne permet pas d’analyser plusieurs éléments du syst`eme de par le manque de précision des patrons de modélisation utilisés. En particulier : 1. l’environnement d’exécution des partitions n’est pas spécifié, empˆechant leur analyse (simulation de l’ordonnancement des partitions et du syst`eme, fonctionnalités proposées suffisantes par rapport aux besoins de la couche applicative, etc.). 2. les connections entre partitions ne spécifient pas leurs contraintes de configuration (délai d’arrivée des données, etc.), ce qui restreint l’analyse de l’architecture (ces éléments ont un impact sur l’ordonnan¸cabilité) et empˆeche la génération de code (ces mécanismes doivent ˆetre spécifiés pour générer la configuration de chaque canal de communication). 3. les mécanismes de health monitoring ne sont pas spécifiés, ce qui empˆeche de générer la politique de détection et de reprise d’erreur. Afin de pallier ces probl`emes, nous avons adapté cet exemple à l’aide de nos patrons de modélisation afin de mieux décrire l’architecture et ses exigences. Utilisation de nos patrons de modélisation Afin de pallier ces manques, nous avons donc proposé une nouvelle version de cette spécification en utilisant les patrons de modélisation du chapitre 4. En particulier, les éléments suivants ont été apportés : – Des composants virtual processor et memory ont été ajoutés afin de modéliser l’isolation temporelle et spatiale : 1. Chaque partition est isolée dans des segments mémoire distincts ayant une taille minimale de 100 Ko (estimation de l’empreinte mémoire de chaque partition). 2. Les partitions sont exécutées périodiquement par un algorithme « Round-Robin » . La Major Frame du syst`eme (période à laquelle le cycle d’ordonnancement est répété) est de 120ms. Pendant une période, chaque partition est exécutée pendant 20ms. – Les connections, initialement spécifiées via des groupes de ports (port group, type d’interface inutilisée dans le cas des architectures partitionnées), ont été séparées en plusieurs data ports inter-connectés. Par ailleurs, la configuration de chaque port a été spécifiée afin d’ˆetre en mesure de générer leur code d’initialisation. Ainsi, le patron de modélisation utilisé correspond à un type de communication utilisé dans les syst`emes partitionnés (sampling port).