Model-checking dans un contexte avionique 

Télécharger le fichier pdf d’un mémoire de fin d’études

Systèmes de transitions temporisés

Dans le contexte des applications critiques, la prise en compte des contraintes temps réel est indispensable pour la vérification formelle des comportements. Plusieurs forma-lismes permettent la description de modèles temps réel, en particulier les automates tem-porisés (Timed automata) et les réseaux de Petri temporels (Time Petri Net) que nous présenterons dans cette section. Généralement les espaces d’états calculés à partir de ces modèles sont infinis. Pour pouvoir appliquer les techniques de model-checking, il est donc nécessaire d’introduire des abstractions permettant d’en construire des représentations fi-nies. Les abstractions considérées doivent bien sûr préserver les classes de propriétés que l’on cherche à vérifier. Nous présenterons deux de ces abstractions, le graphe des régions et le graphe de classe respectivement associées aux automates temporisés et aux réseaux de Petri temporels.
En préambule, nous définissons les systèmes de transitions temporisés [11] qui per-mettent de définir la sémantique des formalismes temporisés. Dans ce qui suit, on considère un alphabet Σ et R≥ ⊂ R l’ensemble des réels positifs ou nul.
Définition 1.2 (Système de Transitions Temporisé ). Un système de transitions temporisé est un système de transitions S = (Q, q0, →), où Q est l’ensemble des états, q0 ∈ Q est l’état initial et la relation de transition est composée de transitions de délai d 0, → q −→ q.
EF φ ≡ T rue EU φ AG φ ≡ ¬ EF ¬ φ.
AF φ ≡ T rue AU φ EG φ ≡ ¬ AF ¬ φ.

Réseau de Petri temporel

Les réseaux de Petri temporel (T P N) sont une extension des réseaux de Petri [14] où chaque transition est associée à un intervalle temporel qui est l’intervalle dans lequel la transition va être tirée.
Définitions
Nous commençons par définir les réseaux de Petri.
Définition 1.7 (Réseau de Petri). Un réseau de Petri est un tuple hP, T, Pre, Posti où :
— P est un ensemble fini non vide de places,
— T est un ensemble fini non vide de transition,
— Pre : T → P → N est la fonction de précondition,
— Post : T → P → N est la fonction de postcondition
Un réseau de Petri est généralement marqué, c’est à dire équipé d’un marquage initial.
Dans toute cette section, nous ne considérons que des réseaux marqués.
Définition 1.8 (Réseau de Petri marqué). Un réseau de Petri marqué est un réseau de Petri associé à un marquage initial m 0 qui à chaque place associe un marquage, une fonction de P dans N qui à chaque place associe une valeur dans N
Soit Σ un ensemble d’étiquettes, contenant l’étiquette vide . Un réseau de Petri étiqueté est un réseau de Petri associé à une fonction d’étiquetage qui à chaque transition du réseau associe une étiquette de Σ .
Définition 1.9 (Réseau de Petri étiqueté). Un réseau de Petri étiqueté est un réseau de Petri associé à une fonction λ : T → Σ qui à chaque transition associe une étiquette dans Σ .
Un Réseau de Petri Temporel (ou T P N) [15] est un réseau de Petri où chaque transition t est associée à deux réels a et b, tels que a ≤ b, l’intervalle [a, b] est appelé intervalle statique. Cet intervalle spécifie des dates de tirs possibles de t. Si t reste sensibilisée, sans interruption, après qu’elle ait été sensibilisée alors :
— a(0 ≤ a) est le temps minimum qui doit s’écouler, à partir de l’instant où t a été sensibilisée, avant que t ne puisse être tirée.
— b(a ≤ b) est la durée maximale pendant laquelle t peut rester sensibilisée sans tirée.
Les dates a et b, pour une transition t, sont relatives à la date où t a été sensibilisée. Soit τ cette date. Alors t ne peut être tirée avant τ + a et doit être tirée avant τ + b, à moins qu’elle ne soit désensibilisée avant. La Figure 1.5 montre un T P N.
Nous donnons maintenant une définition des T P N. Nous noterons II ⊆ IR≥ l’ensemble des intervalles réels non vides à bornes rationnelles non négatives.

Le problème de l’explosion combinatoire

La principale limite à l’utilisation du model-checking est liée au problème de l’explosion combinatoire : le nombre d’états augmente de façon exponentielle en fonction de la com-plexité du système. La taille de l’espace d’états peut alors excéder la quantité de mémoire disponible, rendant impossible la vérification de propriétés sur l’espace d’états.
Les systèmes que nous étudions sont généralement composés de processus qui inter-agissent. La description du système spécifie le comportement de chacun de ces processus et leurs interactions. L’explosion combinatoire est liée au nombre de processus qui compose le système : la taille de l’espace d’état est exponentielle par rapport au nombre de proces-sus. Par exemple, considérons un ensemble de n processus à deux états. L’état global du système peut-être représenté par un vecteur de n bits et le nombre maximum d’états dans le système est 2n.
Différentes techniques permettent de limiter l’explosion combinatoire. Nous présentons dans cette section quelques techniques de réductions parmi les plus connues.
Il est important de noter que la modélisation est une étape priviliégiée pour la préven-tion de l’ explosion combinatoire : Le choix des abstractions et des simplifications influe énormément sur la taille de l’espace d’états.
Une bonne abstraction est une abstraction qui ne conserve que le minimum de compor-tements nécessaires pour la vérification des propriétés. Il est alors important de ne vérifier qu’un nombre limité de propriétés. Les simplifications doivent n’éliminer, dans la mesure du possible, que les comportements inutiles à la vérification des propriétés. Finalement, il n’est pas possible de définir des abstractions ou simplification sans connaitre précisément la sémantique du langage de modélisation ni les comportements, souvent subtils, du sys-tème à vérifier.
Nous présentons dans le chapitre 2 un exemple de modélisation et vérification formelle par model-checking dans un contexte avionique.

Model-checking symbolique par les BDD

Le model-checking symbolique [20] est une technique où les états sont représentés symboliquement par des diagrammes de décision. Cette représentation symbolique permet une représentation plus compacte de l’espace d’états.
Les valeurs de vérité d’une proposition booléenne peuvent être représentées par un arbre de décision binaire. Dans cet arbre, une branche représente une assignation aux variables de la formule et la feuille de la branche porte la valeur de vérité de la formule étant donnée cette assignation. Cette représentation n’est pas optimale : l’arbre peut contenir des sous-arbres isomorphes et par définition il n’y a que deux valeurs de vérité possibles. La solution à ce problème est un graphe acyclique, appelé diagramme de décision binaire (BDD), qui identifie de manière unique les sous-arbres isomorphes et les feuilles identiques. Il a été démontré [21] qu’il existe un diagramme unique pour chaque ensemble d’états, représentés par des tuples booléens sur un ensemble de propositions atomiques ordonnées.
Un diagramme de décision binaire ordonné (OBDD) est un BDD avec un ordre total sur les noeuds. Pour tout chemin du graphe allant de la racine jusqu’à une feuille, les va-riables apparaîtront dans le même ordre. La taille d’un OBDD est fortement dépendante de cet ordre et décider si un ordre conduit à une taille polynomiale de l’OBDD est un pro-blème NP-complet [22]. Néanmoins, le model-checking symbolique peut-être très efficace en pratique pour les modèles non temporisés (ou en temps discret) [23].
Des structures analogues aux BDD, appelées diagrammes de différences d’horloges (CDD), ont été proposées pour la vérification des automates temporisés [24, 25]. Un CDD est un graphe orienté acyclique qui capture une union de zones (Section 1.2.2). Un noeud terminal représente une valeur booléenne. Un noeud non terminal est associé à une paire d’horloges. Chaque arc sortant est associé à un intervalle bornant la différence entre les horloges du noeud. Un chemin dans le CDD représente une zone définie par la conjonction des contraintes associées au chemin. Étant donnée une zone, elle appartient à l’union s’il existe un chemin dans le graphe qui se termine par une constante vraie. Comme pour les BDD, la taille d’un CDD est fonction de l’ordre (total) choisi pour les noeuds mais contrairement aux BDD il n’existe pas de CDD unique pour un ensemble d’horloges. L’ef-ficacité de cette approche dépend fondamentalement de l’ordre choisi pour ordonner les paires d’horloges. En fonction du modèle à vérifier, il n’est pas toujours possible de trouver un ordre pour lequel la méthode est efficace.

Ordres partiels

Une des causes de l’explosion combinatoire réside dans la représentation du parallélisme par l’ entrelacement d’actions. L’idée des ordres partiels est d’éliminer autant que se peut les entrelacements inutiles lors de la construction de l’espace d’états.
La méthode est basée sur une analyse structurelle préalable des relations de dépen-dances entre les différentes transitions. La réduction exploite la commutativité des transi-tions concurrentes indépendantes, pour lesquelles l’état obtenu est le même quel que soit l’ordre d’exécution. Suivant le cas, seul un sous-ensemble de transitions sera localement exploré stubborn sets [26], les persistent sets [27] et les ample sets [28], soit, sous certaines conditions, on franchira en un seul pas atomique un ensemble de transitions indépendantes pas couvrants [29].
Il est possible de combiner la technique des stubborn sets et des pas couvrants, puis de construire le graphe de pas persistants [30].
Les techniques de réduction ordres partiels préservent l’absence de blocage et, sous certaines conditions, la structure linéaire ou arborescente de l’espace d’états.

Exploitation des symétries

La notion de symétrie d’un objet peut se définir comme la stabilité de cet objet vis à vis de certaines transformations. On dit que l’objet est symétrique. En géométrie par exemple, un polygone régulier est invariant par rotation et réflexion. On retrouve ce concept dans de nombreux domaines scientifiques ou artistiques comme l’illustre la Figure 1.6. Elle repro-duit un tableau de Maurits Cornelis Escher, artiste peintre néerlandais du 20ème siècle, qui construisait ses oeuvres en utilisant des translations, rotations, réflections, . . . .
L’intérêt pratique des symétries est qu’elles simplifient l’étude des objets symétriques : puisque l’objet est stable vis à vis de certaines transformations, certaines de ses propriétés le sont aussi. On peut réduire l’étude des propriétés aux parties de l’objet qui ne sont pas stables par ces transformations.
Supposons par exemple que l’on veuille s’assurer que tous les oiseaux de la Figure 1.6 possèdent deux ailes. On peut compter toutes les ailes dans le tableau, ou bien remarquer que le tableau est stable par rotation d’un couple d’oiseaux blanc et noir, illustré dans la Figure 1.7. Il suffit alors de compter les ailes de chacun des oiseaux d’un couple, et par symétrie, on déduit que tous les oiseaux ont deux ailes.
Dans notre contexte, nous exploitons les symétries structurelles des systèmes. Intuitive-ment, un système est structurellement symétrique lorsque ses composants et leurs relations sont identiques modulo un identifiant. Nous pouvons utiliser ces symétries pour réduire l’espace d’états grâce au principe de symétrie [31] Ce principe énonce que :

Il y a au moins autant de symétries dans les effets que dans les causes

Par analogie, on identifie les causes avec la description du modèle du système et les effets avec les comportements du système, capturés dans l’espace d’états. Les symétries structurelles du système induisent des symétries sur le graphe de l’espace d’états. Les sy-métries du graphe, qui sont des automorphismes, induisent une relation d’équivalence sur ses sommets.
Les méthodes de réduction par symétries construisent un quotient de l’espace d’états par cette relation d’équivalence, réduisant sa taille par un facteur proportionnel à la quan-tité de symétries dans le système. Le cœur de cette thèse est une méthode de réduction par symétries pour les T P N, traitée en détail dans la Partie II.
Les méthodes de réduction par symétries préservent l’accessibilité, modulo symétrie, mais peuvent aussi préserver les formules de logique en temps linéaire [32].

FIACRE et TINA

Les sections 1.1 et 1.2.3 ont présenté les modèles formels permettant d’exprimer les propriétés ou les comportements. Dans cette section, nous présentons la boîte à outils TINA (TIme Petri Net Analyzer) permettant l’édition et l’analyse de réseaux de Petri temporels, le langage Fiacre – Format Intermédiaire pour les Architectures de Composants Répartis Embarqués – ainsi que la technique de vérification des descriptions Fiacre via TINA.

La boite à outils TINA

TINA (TIme Petri Net Analyzer 1) est un environnement logiciel pour l’édition et l’analyse de réseaux de Petri et de réseaux de Petri temporels étendus par des priorités et des données. Sur ces modèles, TINA permet la vérification de propriétés par model-checking pour, notamment, la logique temporelle à temps linéaire State/Event LTL. Cette section présente un panorama général des fonctionnalités offertes par cet environnement, son architecture et les principales applications de la boîte à outils. Une description plus détaillée est disponible dans [33].
En plus des fonctionnalités usuelles d’édition et d’analyse offertes par des environne-ments comparables, TINA permet de construire différentes abstractions de l’espace d’états préservant des classes de propriétés telles que les propriétés générales d’accessibilité (ab-sence de blocage, . . . ) ou des propriétés spécifiques telles que celles exprimables en logique temporelle à temps linéaire ou arborescent.
Pour les systèmes atemporels, les abstractions d’espaces d’états fournies permettent de limiter l’explosion combinatoire. Pour les systèmes temporisés, ces abstractions sont indispensables car leurs espaces d’états sont généralement infinis, TINA implémente ainsi différentes abstractions basées sur la notion de classes d’états.
Tina accepte en entrée des réseaux décrits sous forme textuelle, graphique ainsi que les descriptions P N M L (un format d’échange de réseaux de Petri, basé sur XML). En sortie, TINA produit des structures de Kripke étiquetées sous divers formats textuels ou binaires pour des vérificateurs de modèles natifs ou externes.

Systèmes avioniques

Les systèmes avioniques sont des systèmes électroniques, électriques et informatiques embarqués dans un avion et indispensable à son fonctionnement. Ce chapitre se concentre sur les systèmes informatiques qui sont, dans ce contexte, temps réel et critiques quant à leur sûreté de fonctionnement.
Les systèmes temps réel sont des systèmes où une opération est correcte si elle délivre le bon résultat et qu’elle le délivre au bon moment. La dimension temporelle est très im-portante. Par exemple, lorsqu’un pilote actionne une manette de gaz électrique, le système doit calculer la bonne puissance, toujours avec le même délai.
Les systèmes critiques sont des systèmes où une erreur peut avoir des conséquences catastrophiques : perte de mission ou perte de vies humaines. Une faute mal gérée dans un système avionique peut entraîner la perte de l’avion et des passagers. En conséquence la sûreté de fonctionnement, qui passe notamment par le respect des contraintes temporelles, est un objectif essentiel et structurant dans la réalisation de ces systèmes.

Contraintes règlementaires, processus de développement

Les systèmes avioniques et plus généralement les avions qui les embarquent ont un très fort impact social. La responsabilité des avionneurs est très importante et il est légitime que les citoyens exercent un contrôle sur eux. Ce contrôle se fait à travers des autorités de certification, l’European Aviation Safety Agency(EASA) en Europe et la Fededral Aviation Administration(FAA) aux États-Unis. Ces institutions s’assurent pour le compte de la société civile que les avions utilisés au quotidien par des millions de personnes sont sûrs.
Les autorités de certification définissent des objectifs de certification qui garantissent autant que possible la sûreté des avions construits. Dans l’aéronautique, l’approche utilisée est basée sur les standards. Elle repose sur la prise en compte de l’expérience accumulée par la communauté industrielle (notamment à travers les enquêtes après accident) [46].
Une des difficultés de l’activité de certification est que la qualité d’un avion est dif-ficilement quantifiable. Les autorités l’évaluent et la mesurent à travers un ensemble de contraintes sur chacun des processus impliqués. Ces contraintes doivent être respectées par l’avionneur tout au long du cycle de vie de l’avion.
Au niveau le plus haut, on trouve le système « avion » qui implémente des fonctions. La première des fonctions d’un avion est de voler. Le système avionique est directement impli-qué dans les fonctions de commande de vol, de pilote automatique, de gestion du carburant . . . L’évaluation de sûreté à ce niveau analyse les défaillances possibles des fonctions : dys-fonctionnement, fonctionnement intempestif ou perte. L’analyse, guidée par l’ARP-4761 [47], établit la criticité d’une fonction par rapport à la gravité de ses défaillances. C’est une analyse de sûreté du système. A chaque niveau de criticité est associée une probabilité d’occurrence tolérée. La Table 2.1 montre quelques exemples de niveau de gravité, leur conséquence et leur probabilité tolérée.
De nombreux critères influent sur la conception d’un avion : le poids, la consommation, le nombre de passagers qu’il peut embarquer,. . . Cependant et quelque soit ces critères, il est indispensable de garantir la sûreté de fonctionnement. En ce sens, la sûreté de fonctionnement est un critère structurant pour la conception du système avionique : le système est raffiné avec comme objectif de minimiser les risques identifiés. Il s’agit alors de réduire la fréquence d’occurrence ou la gravité des défaillances, en introduisant par exemple des mécanismes de tolérance aux pannes ou de redondances. Ce processus de raffinement est guidé par les recommandations de l’ARP-4754 [48]. Le raffinement s’arrête lorsque les éléments de base du système, appelés composants, sont tous identifiés. Ce processus produit un ensemble d’exigences de haut niveau (HLR), fonctionnelles ou de sûreté, qui spécifient les composants et leurs interactions. Chacun de ces composants hérite du niveau de criticité de la fonction qu’il contribue à réaliser. A ce niveau d’abstraction, les composants sont supposés corrects, c’est à dire conforme à leurs exigences. Nous ne nous intéresserons qu’aux niveaux d’abstraction inférieurs à la sortie du processus de raffinement. Le problème est alors de prouver que les composants sont corrects.
Dans ce chapitre, focalisé sur la dimension informatique d’un système avionique, un composant est soit matériel soit logiciel. Ici encore, le processus de réalisation des com-posants est guidé par des contraintes pour la certification. Un composant logiciel ne peut être certifié que s’il atteint les objectifs définis par la norme DO-178 [49] tandis qu’un composant matériel doit atteindre ceux définis par la norme DO-254 [50]. Nous ne nous intéressons qu’aux composants logiciels.
Comme pour le système, le processus de développement du composant est structuré par son niveau de criticité, appelé Design Assurance Level(DAL). La norme DO-178 définit 5 DALS, de A à E. Le niveau A, catastrophique, est le plus sévère. Une défaillance dans un logiciel de niveau A empêche le vol ou l’atterrissage. Par exemple, les composants impliqués dans la fonction de commande de vol ont un DAL A. A l’opposé, une défaillance dans un logiciel de niveau E n’a aucune conséquence.
A chaque niveau de criticité correspond un ensemble d’objectifs et de moyens de prou-ver que ces objectifs ont été atteints. La norme DO-178 proposait jusqu’à une évolution récente trois moyens de preuves: la revue, l’analyse et le test. Pour chaque objectif il faut prouver qu’il est atteint en utilisant une combinaison d’un ou plusieurs de ces moyens. Mais la norme n’est pas prescriptive, le choix du ou des moyens de preuve est laissé à l’industriel.
Le processus de développement est un processus de raffinement. La spécification du composant par ses HLR est successivement raffiné jusqu’au code objet qui sera exécuté sur un composant matériel embarqué. Dans un premier temps, les HLR sont raffinées jusqu’à des exigences de bas niveaux (LLR). Un des objectifs à atteindre est la traçabilité totale entre les HLR et les LLR. Cette traçabilité est généralement prouvée par des revues. Le code source est ensuite écrit à partir des LLR puis compilé vers du code objet. Un autre objectif de la DO est de montrer l’équivalence du code objet avec les LLR. Comme la norme n’est pas prescriptive, plusieurs options sont possibles. Une première option peut être de montrer par analyse l’équivalence du code source par rapport à ses LLR, puis de montrer que le code source est équivalent au code objet en utilisant un compilateur certifié. Une deuxième option est de montrer que le code objet est équivalent aux LLR par des tests. Dans ce cas, il faut prouver que les objectifs de couverture du code sont atteints.
Les outils utilisés dans ce processus (eg: le compilateur) sont eux aussi contraints par la norme. Deux types d’outils sont considérés :
— Les outils de développement sont les outils qui peuvent introduire des erreurs dans le programme, par exemple les compilateurs. Ces outils héritent du même niveau de criticité que les logiciels qu’ils aident à développer ;
— Les outils de vérification sont les outils qui peuvent échouer à détecter des erreurs, par exemple les simulateurs. La criticité est moins élevée et les contraintes de certification moins fortes.
Nous concluons cette section par un mot sur une évolution récente de la DO-178. La version B a été publiée en 1992 et ne tenait pas compte des méthodes de vérification for-melle. Les progrès de ces moyens au cours de ces vingt dernières années tout autant que l’évolution des pratiques des industriels dans ce sens ont fait évoluer la situation. Très ré-cemment, en 2011, la version C de la norme a été publiée. Cette version intègre l’utilisation des méthodes formelles comme moyen de preuve des objectifs de certification. L’utilisation des ces nouveaux outils est très encadrée mais cette évolution offre des opportunités aux méthodes formelles. Les conditions d’utilisation des méthodes formelles sont décrites dans un document compagnon, la norme DO-333. Nous présentons dans les sections suivantes différentes utilisations des méthodes formelles pour la vérification des systèmes avioniques.

Avionique Modulaire Intégrée

L’architecture avionique modulaire intégrée, aussi appelée IMA pour Integrated Modu-lar Avionic, permet à des composants logiciels, de partager des ressources de composants matériels. C’est une architecture constituée de composants matériels, de composants logi-ciels et d’un réseau de communication. Nous nous conformerons à la terminologie IMA en appelant fonctions les composants logiciels et modules les composants matériels. L’IMA est apparue dans les années 90 et est utilisée par Airbus depuis l’A380 et par Boeing depuis le B777.
Un des avantage d’IMA est de permettre à des fonctions de niveau de criticité différents de partager des modules. C’est ce que l’on appelle la ségrégation. La ségrégation des fonctions a permis de nombreux progrès dans l’avionique : gains de poids, optimisation du processus industriel, standardisation des modules, . . . La ségrégation des différentes fonctions repose sur les concepts de liens virtuels du réseau AFDX et partition du système d’exploitation ARINC-653.
Une partition s’exécute sur un module à travers le système d’exploitation ARINC-643. Elle est définie par une zone mémoire et une tranche de temps périodique, pendant la-quelle elle est la seule à s’exécuter sur le module [51]. Le temps d’exécution d’une partition est borné par un pire cas de temps d’exécution (WCET). Nous supposons, à des fins de simplification, qu’une fonction est toujours implémentée par une seule partition. Plusieurs partitions peuvent s’exécuter sur un module. Ces partitions sont ordonnancées statique-ment et de façon strictement périodique. Une trame cyclique englobante, appelée MAF (MAjor time Frame), décrit l’ordonnancement de toutes les partitions du module. La pé-riode de la MAF est l’hyper-période des périodes des partitions. L’onset d’une partition est la phase de la partition par rapport à celle de la MAF. L’ordonnancement est réalisé par le système d’exploitation du module.
Un lien virtuel est un mécanisme de communication offert par le réseau AFDX qui permet la ségrégation de flux provenant de fonctions de différents niveaux de criticité. Le réseau AFDX pour Avionics Full-DupleX, est un réseau dérivé de l’Ethernet commuté. Il est composé de commutateurs et à ses extrémités de producteurs/consommateurs de données, appelés abonnés. Un lien virtuel est vu par les fonctions comme un bus virtuel mono-émission/multi-réception qui garantit une bande passante, une latence et une gigue bornées.
Les partitions communiquent à travers des ports de communication unidirectionnels, appelés APEX. Il existe deux types de ports :
— Port queuing : le port se comporte comme une FIFO,
— Port sampling : seule la dernière donnée reçue est conservée.
Ces ports permettent aux partitions de communiquer via le réseau AFDX ou via des bus de terrain. Ces bus de terrain connectent les capteurs et actionneurs des systèmes méca-niques, électriques ou hydrauliques avec le reste du système avionique.
Les modèles d’exécution et de communication des architectures IMA sont spécifiés par les standards ARINC653 [52] et ARINC664 (partie 7) [53].

Système de gestion automatique de vol

L’objet de la vérification présentée dans cette section est une fonctionnalité d’un sys-tème de gestion automatique de vol.
Un système de gestion automatique de vol, ou AutoFlight Control System (AFCS), fournit un support opérationnel aux pilotes. Il vise à réduire la charge de travail des pilotes, stabiliser au mieux l’avion, améliorer le confort de vol et finalement augmenter les capacités opérationnelles (eg : atterrissage avec visibilité réduite). Ces services sont proposés à travers quatre sous-systèmes :
— Le pilote automatique(AP) commande les actuateurs, directement ou indirectement via le système de contrôle de vol ;
— La commande de gaz automatique commande la poussée moteur ;
— Le directeur de vol indique au pilote, sur l’horizon artificiel, la position que doit prendre l’avion par rapport à une trajectoire cible ;
— Le guidage de vol permet au pilote d’opérer l’avion à travers des scénarios de haut niveau, appelés modes. Ces modes contraignent les interactions possibles entre le pi-lote et l’avion. Des exemples de modes sont « maintenir une altitude cible », « atteindre une vitesse cible », . . .
Nous nous intéressons au sous-système de guidage de vol et plus particulièrement à une fonction de capture d’altitude cible dans le mode « atteindre une altitude cible ». Cette fonction permet au pilote, à partir d’un bouton rotatif placé dans le cockpit, de sélec-tionner la consigne d’altitude transmise au pilote automatique. Un exemple d’équipement installé dans le cockpit est montré dans la Figure 2.1. Le bouton est encadré en rouge.
L’architecture fonctionnelle répond à des exigences de sûreté via une architecture fonc-tionnelle COM/MON. Comme indiqué en Section 2.2, ces composants sont spécifiés fonc-tionnellement par une sémantique synchrone et déployés dans un environnement asyn-chrone. En conséquence des exigences non fonctionnelles émergent [81]. Les exigences aux-quelles nous nous intéressons sont des contraintes temporelles que les composants doivent respecter. Ces composants héritent du niveau de criticité DAL-B. Le pilote peut toujours désactiver le système de guidage de vol lorsque ce dernier tombe en panne, à condition que la panne soit détectée. D’où la nécessité d’utiliser l’architecture COM/MON et de s’assurer que le MON détecte bien les erreurs du COM.

Table des matières

I Model-checking dans un contexte avionique 
1 Vérification formelle par model-checking 
1.1 Logiques temporelles
1.1.1 Définitions
1.1.2 LTL
1.1.3 CTL
1.2 Modèles temporels
1.2.1 Systèmes de transitions temporisés
1.2.2 Automates temporisés
1.2.3 Réseau de Petri temporel
1.3 Le problème de l’explosion combinatoire
1.3.1 Model-checking symbolique par les BDD
1.3.2 Ordres partiels
1.3.3 Exploitation des symétries
1.4 FIACRE et TINA
1.4.1 La boite à outils TINA
1.4.2 Le langage Fiacre
2 Model-checking dans un contexte avionique 
2.1 Systèmes avioniques
2.1.1 Contraintes règlementaires, processus de développement
2.1.2 Avionique Modulaire Intégrée
2.1.3 Vérification formelle dans le contexte avionique
2.2 Un exemple de vérification par model-checking
2.2.1 Système de gestion automatique de vol
2.2.2 Modélisation de la capture d’altitude
2.3 Conclusion
II Symétries pour les réseaux de Petri temporels 
1 Rappels sur les groupes de permutations 
1.1 Groupes
1.1.1 Sous-groupes et cosets
1.1.2 Homomorphisme de groupes
1.2 Groupes de permutations
1.2.1 Action de groupe
1.2.2 Produits de groupes
1.2.3 Base et ensemble générateur fort
1.2.4 Recherche avec retour arrière
1.2.5 Symétries des graphes
2 Réduction par symétries 
2.1 Les symétries des réseaux de Petri
2.2 Identification des symétries
2.2.1 Les scalarsets
2.2.2 Détection automatique
2.2.3 Discussion
2.3 Méthodes de réduction par symétries
2.3.1 Itérer sur les symétries
2.3.2 Itérer sur les états
2.3.3 Calculer un représentant canonique
2.3.4 Classes de groupes simples
2.3.5 Discussion
2.4 Symétries pour les automates temporisés
2.4.1 Discussion
2.5 Conclusion
3 Construction des réseaux par composition symétrique 
3.1 Définitions et notations
3.2 Opérateur de composition symétrique
3.2.1 Union disjointe des réseaux
3.2.2 Synchronisation
3.3 Réseaux de composants disjoints
3.3.1 Définition
3.3.2 Conditions sur la composition symétrique
3.3.3 Produits
3.4 Conclusion
4 Exploitation des symétries des G-réseaux 
4.1 Symétries du graphe des classes d’états
4.1.1 Symétries du graphe d’états
4.1.2 Symétries du graphe des classes d’états
4.2 Réduction des G-réseaux
4.2.1 Méthodes par itération
4.2.2 Représentant canonique
4.3 Réduction des RCD
4.3.1 Un ordre sur les transitions de même intervalle statique
4.3.2 Un ordre total sur les classes d’états équivalentes
4.3.3 Canonisation des RCD
4.4 Conclusion
5 Implémentation et expérimentations 
5.1 Construction des G-réseaux
5.1.1 GAP
5.1.2 Implémentation d’un prototype
5.1.3 Unmot sur la complexité
5.2 Expérimentations avec Tina
5.2.1 Description des symétries
5.2.2 Expérimentations avec Tina
5.3 Conclusion
Conclusion générale, perspectives

Télécharger le rapport complet