Formalisation des exigences et du comportement du système

Télécharger le fichier original (Mémoire de fin d’études)

Architecture avionique modulaire intégrée

Les architectures avioniques modulaires intégrées sont apparues dans les années 90 pour exécuter un ensemble d’applications partageant des ressources de calcul, appelées modules, et communiquant par un réseau partagé lui-même connecté à un ensemble de capteurs/actionneurs embarqués par l’intermédiaire de passerelles appelées RDC (pour Remote Data Concentrator). Les modèles d’exécution et de communi-cation des architectures IMA sont définis par les standards ARINC653 [12] et ARINC664 (partie 7) [13] adoptés par Airbus depuis l’A380 et par Boeing depuis le B777. L’objectif de ces standards est d’assurer un niveau élevé de sûreté de fonctionnement, en particulier en garantissant à la fois la ségrégation des fonctions avioniques et un certain degré de prédictibilité temporelle, c’est-à-dire une capacité de preuve de la satisfaction d’un ensemble d’exigences temps réel. L’ARINC653 définit les règles de partage des modules entre les fonctions. L’ARINC664 (partie 7), aussi connu sous le nom d’AFDX (pour Avionics Full-DupleX switched ethernet), définit les règles de partage du réseau de communication inter-modules.
Ce chapitre n’a pas vocation à être une présentation exhaustive de ces standards, en revanche nous nous concentrons sur les propriétés pertinentes vis à vis de notre modèle et de nos objectifs. En particulier, nous décrivons plus en détail la notion de module IMA et le réseau AFDX.

Module IMA

Le concept IMA repose sur la séparation du développement des ressources et des fonctions avioniques. Les ressources de calcul sont des modules interconnectés par le réseau AFDX et potentiellement connectés à d’autres équipements, comme des capteurs ou des actionneurs, par diﬀérents moyens de communication tels que des bus de terrain. Pour garantir la ségrégation des fonctions avioniques, la notion de partition est utilisée.

Partition

Chaque fonction s’exécute au sein d’une partition. Une partition est caractérisée par une zone mémoire qui lui est propre et une tranche de temps, répétée périodiquement, pendant laquelle elle est la seule à pouvoir s’exécuter sur le module. Le partage des ressources de calcul du module est donc réalisé grâce à un découpage temporel. Les partitions d’un module sont ordonnancées statiquement et de façon strictement périodique : si une occurrence d’une partition démarre à un instant t et que la partition a une période T , alors le prochain démarrage de la partition aura lieu à l’instant t + T . L’ordonnancement de toutes les partitions d’un module est décrit par une trame cyclique, appelée la MAF (pour MAjor time Frame). Comme les périodes de ces partitions ne sont pas nécessairement identiques, la longueur de la MAF est égale à l’hyper-période des partitions du module, c’est-à-dire le ppcm (pour plus petit commun multiple) des périodes des partitions. Les partitions sont alors caractérisées par leur période, leur durée et un décalage relatif au démarrage de la MAF, appelé oﬀset. Ces notions sont représentées sur la figure 1.1. Les fonctions F1 et F2 de période T1 et T2 s’exécutent dans les partitions représentées par les boîtes notées F1 et F2. O2 correspond à l’oﬀset de la partition de F2. L’oﬀset de F1 coïncide avec le début de la MAF, il est donc nul et n’est pas représenté.
A noter que l’ARINC 653 permet d’attribuer plusieurs tranches de temps à une partition. Dans un souci de simplicité, nous nous restreignons à des partitions avec une unique tranche de temps.
A l’intérieur d’une partition, la fonction avionique est réalisée par un ensemble de processus qui sont ordonnancés localement à la partition : les processus de F1 peuvent par exemple être ordonnancés avec une politique à priorité fixe tandis que les processus de F2 peuvent être ordonnancés avec une politique EDF (pour Earliest Deadline First). Dans cette thèse, nous ne prenons pas en compte ce niveau de détail. Une fonction sera seulement caractérisée par son temps d’exécution pire cas (WCET pour Worst Case Execution Time).

Communication

Les communications entre les partitions s’eﬀectuent au travers de ports de communication, dit ports
APEX, qui peuvent être de type :
– sampling où seule la dernière donnée reçue est conservée,
– queuing où le port se comporte comme une file d’attente.
Les ports APEX sont unidirectionnels : ils sont utilisés soit en lecture, soit en écriture. Dans la suite, nous ferons l’hypothèse qu’une fonction lit l’ensemble de ses ports d’entrée au démarrage de sa partition et réalise l’ensemble des écritures sur ses ports de sortie à la fin de son traitement et avant la fin de la partition.

Remote Data Concentrator

Un RDC est un module spécialisé qui relie des équipements sans connexion AFDX, tels que des capteurs ou des actionneurs, à la plateforme IMA. La fonctionnalité d’un RDC est donc de convertir des données provenant d’une technologie de type bus (bus de terrain, ARINC429, CAN,. . . ) vers l’AFDX et réciproquement. La transformation consiste à traduire les données dans le format adéquat en modifiant leur encodage par exemple. Les RDC peuvent être considérés comme des passerelles sans OS dont tous les ports sont de type sampling.

Réseau AFDX

Le réseau AFDX est dérivé de l’Ethernet commuté. Ce réseau est composé principalement de com-mutateurs, qui sont les éléments clefs de l’architecture et de producteurs/consommateurs de données, qui sont appelés les abonnés. Dans cette thèse, les abonnés que nous considérons sont les modules IMA et les RDC. Le réseau doit :
– garantir la fiabilité des données.
– oﬀrir une disponibilité élevée. De nombreux équipements étant reliés au réseau, il est prévu un temps moyen entre panne (MTBF pour Mean Time Between Failure) très élevé, de l’ordre de 100000 heures.
– garantir l’ordre des paquets au sein d’un même flux, ainsi qu’un chemin unique de bout en bout pour tous ces paquets, c’est-à-dire que le routage des paquets doit être statique.
– fournir une isolation des erreurs, entre éléments consécutifs ou entre flux.
– fournir un service déterministe de transfert de données. La latence maximale de bout en bout, ainsi que la gigue, doivent être connues. Aucune perte de trame par congestion n’est tolérée.
Ce dernier point est très important dans le processus de validation du système avionique. En eﬀet, dans le cas d’un réseau Ethernet commuté Full-Duplex, le risque de perte de trames est présent. L’utilisation de liens Full-Duplex supprime le risque de collision sur les liens physiques. En revanche, les files d’attente internes aux commutateurs sont de taille limitée, un trafic trop important pourrait les faire déborder. En outre, l’occupation des files d’attente entraîne des délais dans les communications. La spécificité du réseau AFDX est la mise en place de mécanismes de contrôle de flux permettant de maîtriser l’utilisation des files d’attentes, et donc la qualité de service, oﬀerte par le réseau. Dans l’AFDX, cette maîtrise de la qualité de service est assurée par l’implémentation de la notion de liens virtuels (VL pour Virtual Link).

Lien Virtuel

Cette notion est centrale dans le réseau AFDX. La principale motivation derrière cette notion est de fournir une ségrégation des flux : le mauvais comportement d’un flux ne doit pas nuire aux autres flux. En d’autres termes, un lien virtuel permet de « virtualiser » un bus avionique classique pour chaque flux, où il serait le seul flux à émettre. Cette « virtualisation » a pour objectif de garantir à chaque flux une certaine bande passante, ainsi que des caractéristiques temps réel comme les temps de traversée du réseau pire et meilleur cas, quel que soit le comportement des autres flux. Un lien virtuel est défini par :
– un identifiant unique,
– une ou plusieurs adresses de destination,
– le chemin emprunté pour rallier ces destinations,
– la taille minimale et maximale d’un paquet,
– un temps minimum d’émission entre deux paquets consécutifs, appelé bag (pour Bandwidth Alloca-tion Gap).
Un émetteur ne peut donc émettre sur un VL qu’au maximum un paquet de taille maximale tous les bag. En notant smax cette taille maximale, le débit maximal d’un VL, noté , est donc : = smax (1.1) bag
Dans la suite, nous appelons lisseur de trafic le mécanisme en entrée d’un VL, forçant le temps minimum d’émission entre deux paquets. Nous représentons son fonctionnement sur la figure 1.2. A fin de chaque exécution, la fonction F1 produit des données qu’elle place dans les ports APEX correspondants. Sur cet exemple, 4 messages sont produits et placés dans 3 ports APEX, et ces ports émettent dans un même VL. Ensuite, ces messages sont placés dans la file d’attente du VL. Le lisseur de trafic cadence alors ces messages au rythme d’un tous les bag. La politique de service est « premier arrivé premier servi » (FIFO pour First In First Out). Le flux en sortie lisseur de trafic est alors mélangé aux autres VL produits par F1 ou par les autres fonctions du module. L’ordonnanceur des VL sera supposé utiliser une politique de service FIFO. L’agrégation de ces flux est alors transmise sur le réseau via le port Ethernet du module. Du fait de ce mélange, les paquets d’un VL ne sont potentiellement plus cadencés tous les bag, comme représentés sur la figure.

Conclusion

Nous avons présenté les principes fondamentaux des systèmes IMA, à savoir la mutualisation des ressources de calcul et de communication. Dans la suite, nous illustrons ces principes sur une étude de cas tirée d’un système de gestion de vol. Une description plus détaillée de la mise en œuvre de ces principes sera réalisée au chapitre 4, où nous présentons un modèle d’architecture pour ces systèmes.

Etude de cas : un système de gestion de vol

Dans cette section, nous introduisons l’étude de cas qui sera utilisée pour illustrer les diﬀérentes notions du mémoire. Il s’agit d’une sous-partie du système de navigation (FMS pour Flight Management System) dont l’objectif est de contrôler l’aﬃchage d’informations de navigation sur les écrans de pilotage. Nous présentons tout d’abord les fonctions avioniques impliquées dans la réalisation du FMS, ensuite l’architecture sur laquelle ces fonctions sont déployées et finalement les exigences de latence, fraîcheur et cohérence que doit satisfaire le système. La description formelle des fonctions et de l’architecture est réalisée au chapitre 4 (page 61). La formalisation des exigences est présentée au chapitre 6 (page 93).
Les diﬀérentes notions d’exigence ainsi que le fonctionnement du système sont illustrés à l’aide d’exemples d’exécution.

Fonctions

Le système de navigation interagit avec l’équipage au travers d’écrans et de claviers. Sur requête du pilote ou du copilote, entrée au moyen de leur clavier respectif, le système doit aﬃcher les informations du prochain point de navigation (on utilisera le terme commun waypoint dans la suite du mémoire) sur les écrans. Ces informations sont de deux types : des informations statiques sur le waypoint telles que les coordonnées du waypoint et la fréquence VOR qui permet de déterminer le cap en direction du waypoint, et des informations dynamiques mises à jour périodiquement telles que l’heure estimée d’arrivée (notée ETA pour Estimated Time of Arrival).
Pour des raisons de sûreté, le FMS repose sur une architecture redondante (composée de deux voies notées 1 et 2). Sur chaque voie i, le FMS est composé d’une fonction KU i (pour Keyboard and cursor control Unit) contrôlant le clavier et d’une fonction MFDi (pour Multi Functional Display) gérant l’aﬃ-chage des pages contenant les informations de navigation. Le pilote peut entrer une requête d’aﬃchage d’un waypoint. Cette requête est reçue par la fonction KU i (i = 1 pour le pilote, i = 2 pour le copilote). La requête est alors transmise aux gestionnaires de vol FM 1 et FM 2 (FM pour Flight Manager) qui questionnent en parallèle la base de données de navigation (NDB pour Navigation DataBase). Celle-ci retourne aux FM les informations statiques du waypoint qui sont ensuite périodiquement enrichies par chaque FM avec des informations dynamiques calculées en fonction des données de vol (vitesse, po-sition,. . . ) produites par les centrales inertielles (ADIRU pour Air Data Intertial Reference Unit). Au final, chaque FM i envoie périodiquement à chaque MFDi ces informations à aﬃcher. Chaque ADIRU élabore les données de vol à partir de données de base fournies par des mesures prises par des capteurs.
Nous décrivons cette architecture fonctionnelle sous la forme de chaînes fonctionnelles telles que re-présentées sur la figure 1.2.1. La figure 1.3(a) correspond aux chaînes impliquées dans l’aﬃchage des informations d’un waypoint suite à une requête du pilote, tandis que la figure 1.3(b) correspond aux chaînes impliquées dans la production de l’heure estimée d’arrivée (ETA pour Estimated Time of Ar-rival) par le FM1. Le système étant symétrique sur les deux voies, nous ne représentons ni les chaînes traitant les requêtes du copilote, ni les chaînes générant l’aﬃchage de l’heure estimée d’arrivée pour le copilote.
Les diﬀérentes variables échangées entre ces fonctions sont :
– reqi : la requête du pilote ou du copilote,
– wpIdi : l’identifiant du waypoint choisi par le pilote ou le copilote,
– queryi : la requête transmise à la NDB par FMi pour récupérer les informations du waypoint,
– answeri : la réponse transmise à FMi par la NDB contenant les informations du waypoint,
– wpInfoi : les informations du waypoint transmises entre FMi et MFDi,
– dispi : la page aﬃchée par MFDi regroupant les informations statiques du waypoint ainsi que l’heure estimée d’arrivée ETAi,
– presi : la valeur de la pression atmosphérique à l’extérieur de l’appareil,
– speedi : la valeur de la vitesse de l’appareil déduite de la pression extérieure,
– ETAi : l’heure estimée d’arrivée au waypoint, pres1 ADIRU1 speed1 ETA1 disp1 se lit de la façon suivante : la fonction ADIRU1 utilise la variable pres1 pour déterminer speed1 qui est transmise à la fonction FM1. Cette variable est utilisée dans le calcul d’ETA1 qui est prise en compte par la fonction MFD1 pour générer la variable disp1. Ces fonctions sont alors déployées sur une architecture IMA que nous décrivons dans la suite.

Architecture

Dans cette section, nous présentons une vue générale de l’architecture IMA sur laquelle est déployé le système de gestion de vol. L’ensemble des paramètres de l’architecture sera détaillé dans le chapitre 4 où nous formaliserons la description d’une telle architecture. A noter que le système présenté est un sous-système de l’appareil et donc que les ressources de calcul et de communication de cette architecture sont partagées avec d’autres fonctions. Cependant, nous ne décrivons que les éléments relatifs au système de gestion de vol FMS.
L’architecture du système de gestion de vol est composée d’un ensemble de modules de calcul intercon-nectés au travers d’un réseau AFDX. Cette architecture est représentée sur la figure 1.4. Sept modules, de Module 1 à Module 7 (nommés M1; : : : ; M7 dans la suite), sont utilisés pour héberger les fonctions avioniques. Le réseau AFDX est constitué de cinq commutateurs S1; : : : ; S5 représentés par les boîtes violettes sur la figure. Les ports des commutateurs ainsi que les ports des modules fonctionnent à 100 Mbits/s.
Les capteurs de pression sensor1 et sensor2 sont reliés aux centrales inertielles ADIRU1 et ADIRU2 au travers des Remote Data Concentrators RDC1 et RDC2. Les écrans display1 et display2 ainsi que les claviers key1 et key2 sont situés dans le cockpit et sont directement reliés aux modules M1 et M2 via un bus de terrain.
Les modules hébergent des fonctions qui s’exécutent périodiquement. Conformément au standard ARINC 653, ces exécutions ont lieu au sein de partitions afin de garantir la ségrégation des fonctions. Ainsi, chaque partition définit une tranche de temps qui lui est propre, c’est-à-dire qu’aucune autre partition ne peut s’exécuter durant cet intervalle de temps. Cet ordonnancement est statique et est défini hors-ligne. Les tranches de temps sont caractérisées par une période, une durée et un décalage relatif au démarrage de la MAF appelé oﬀset. Ces notions ont été présentées à la sous-section 1.1.1 (page 5). Le tableau 1.1 regroupe les paramètres des partitions utilisées dans l’étude de cas. Ces paramètres sont illustrés sur la figure 1.5 qui montre l’ordonnancement statique des partitions du module M1.
Comme présentés à la sous-section 1.1.2 page 7, les échanges de variables entre fonctions s’eﬀectuent au travers de liens virtuels (VL pour Virtual Links). Un VL définit une connexion multipoint entre une source et une ou plusieurs destinations, les sources et les destinations étant des partitions. Par exemple, la fonction KU1 utilise le lien VL1 pour communiquer avec FM1 et FM2. En entrée de chaque VL un mécanisme de lissage de trafic est implémenté. Il garantit une distance minimale entre chaque émission de message sur le VL, ce qui permet d’éviter l’engorgement du réseau. Cette distance minimale est appelée BAG (pour Bandwidth Allocation Gap) du VL. Le tableau 1.2 regroupe les paramètres des liens virtuels utilisés dans l’étude de cas. Les variables empruntant chaque VL sont précisées et le chemin du VL correspond à la séquence des commutateurs traversés par le VL. Si un VL a plusieurs destinations alors il peut exister plusieurs chemins pour ce VL.

Exigences

Pour illustrer les exigences que doit satisfaire le système, nous en présentons quatre.
Exigence de latence relative à une chaîne fonctionnelle : elle permet de garantir que le sys-tème répond suﬃsamment rapidement à une sollicitation,
E1 : l’écran du pilote doit aﬃcher les informations d’un waypoint au plus tard 700 ms après la saisie du pilote.
Exigence de fraîcheur relative à une chaîne fonctionnelle : elle permet de garantir qu’une va-riable du système dépend d’une variable suﬃsamment récente pour être pertinente,
E2 : l’heure estimée d’arrivée aﬃchée sur l’écran du pilote doit dépendre d’une valeur de pression qui a été mesurée au pire 400 ms plus tôt.
Exigence de cohérence sur chaînes fonctionnelles divergentes : elle permet de garantir qu’un événement en entrée du système génère plusieurs événements arrivant dans une même fenêtre tem-porelle,
E3 : les écrans du pilote et du copilote doivent aﬃcher les informations du waypoint saisi par le pilote dans une fenêtre de 500 ms. Autrement dit, la diﬀérence entre la latence d’une requête du pilote et l’aﬃchage des informations sur son écran et de la latence de cette même requête et l’aﬃchage sur l’écran du copilote doit être inférieure à 500 ms.
Exigence de cohérence sur chaînes fonctionnelles convergentes : elle permet de garantir que la valeur d’une variable dépend de valeurs mises à jour dans une même fenêtre temporelle,
E4 : l’heure estimée d’arrivée est déterminée à l’aide des valeurs de pression issues de deux capteurs diﬀérents. Pour que cette estimation ait du sens, il est nécessaire que ces valeurs soient mesurées dans un intervalle de temps de 300 ms.

Table des matières

I Contexte industriel et scientifique
1 Avionique Modulaire Intégrée
1.1 Architecture avionique modulaire intégrée
1.1.1 Module IMA
1.1.2 Réseau AFDX
1.2 Etude de cas : un système de gestion de vol
1.2.1 Fonctions
1.2.2 Architecture
1.2.3 Exigences
1.3 Conclusion
2 Méthodes de modélisation et de vérification
2.1 Modélisation d’architecture
2.1.1 Le langage de description d’architecture AADL
2.2 Modélisation de comportement
2.2.1 Approche avec automates temporisés et model checking
2.2.2 Le tagged signal model
2.2.3 Clock Constraint Specification Language
2.3 Evaluation de performances des réseaux embarqués
2.3.1 Network Calculus
2.3.2 Approche par trajectoire
2.4 Evaluation d’exigences de bout en bout
2.4.1 Evaluation de latence
2.4.2 Evaluation de fraîcheur
2.4.3 Evaluation de cohérence
2.5 Conclusion
3 Contribution
3.1 Démarche suivie
3.1.1 Description de l’architecture
3.1.2 Formalisation des exigences et du comportement du système
3.1.3 Abstraction
3.1.4 Vérification
3.1.5 Publications
3.2 Développements réalisés
3.2.1 Un outil de vérification d’exigences temps réel
3.2.2 Intégration dans le projet SATRIMMAP
II Modèle et sémantique
4 Modèle d’architecture d’un système IMA
4.1 Architecture fonctionnelle
4.2 Architecture matérielle
4.3 Allocation sur la plateforme
4.3.1 Allocation des fonctions
4.3.2 Allocation des variables
4.3.3 Allocation des dépendances
4.4 Conclusion
5 Modèle comportemental d’un système IMA
5.1 Définition des signaux utilisés
5.1.1 Signaux pour les activations de fonction
5.1.2 Signaux pour les copies de variable
5.1.3 Domaine de définition des signaux
5.2 Définition des processus utilisés
5.2.1 Module
5.2.2 Fonction
5.2.3 Lisseur de trafic
5.2.4 Port
5.2.5 Capteur
5.2.6 Actionneur
5.2.7 Remote Data Concentrator
5.3 Comportements du système complet
6 Exigences
6.1 Définitions préliminaires
6.1.1 Chaîne fonctionnelle
6.1.2 Dépendance étendue
6.2 Exigences
6.2.1 Latence
6.2.2 Fraîcheur
6.2.3 Cohérence
6.2.4 Exigences de l’étude de cas
6.3 Conclusion
III Vérification des exigences
7 Formalisation du problème
7.1 Abstraction du problème
7.1.1 Principes généraux
7.1.2 Particularités du tagged signal model
7.1.3 Abstraction des lisseurs de trafic
7.1.4 Abstraction du réseau : canaux temporisés
7.2 Intuitions pour la méthode de vérification
7.3 Mise en oeuvre et outillage
7.3.1 Présentation générale
7.3.2 Acquisition et création des objets
7.3.3 Analyse réseau
7.3.4 Constitution de l’ensemble des contraintes relatives à une exigence
8 Résolution
8.1 Encodage sous la forme d’un programme linéaire mixte
8.1.1 Domaine de définition des variables
8.1.2 Particularité pour la cohérence
8.1.3 Représentation de l’infini
8.1.4 Fonction objectif
8.2 Fonctions objectifs par type d’exigence
8.2.1 Exigence de latence
8.2.2 Exigence de fraîcheur
8.2.3 Exigence de cohérence entre chaînes fonctionnelles divergentes
8.2.4 Exigence de cohérence entre chaînes fonctionnelles convergentes
8.3 Application à l’étude de cas
8.3.1 Exigence de latence
8.3.2 Exigence de fraîcheur
8.3.3 Exigence de cohérence entre chaînes fonctionnelles divergentes
8.3.4 Exigence de cohérence entre chaînes fonctionnelles convergentes
8.3.5 Conclusion
9 Discussions
9.1 Passage à l’échelle
9.1.1 Expérimentations sur une étude de cas paramétrée
9.1.2 Options du solveur
9.1.3 Conclusion
9.2 Ouverture vers des formules analytiques plus précises : application à la latence
9.2.1 Un exemple simple
9.2.2 Extension aux chaînes fonctionnelles emboîtées
Conclusion et perspectives
A Langage de description d’architecture du prototype
B Programmes linéaires des exigences de l’étude de cas
C Méthode analytique locale
Bibliographie