Modélisation des systèmes hybrides et notion de scénario

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

Méthodes d’analyse de la sûreté de fonctionnement

L’évaluation de la sûreté de fonctionnement d’un système consiste à analyser les défaillances des composants pour estimer leurs conséquences sur le service rendu par le système. Il existe des ateliers logiciels comme SOFIA [Sofia] destinés à simuler quantitativement l’effet d’une défaillance sur le comportement du système. Les principales méthodes utilisées lors d’une analyse de la sûreté de fonctionnement sont décrites ci-dessous.

L’analyse fonctionnelle

Une analyse fonctionnelle, en général, précède une étude de sûreté de fonctionnement. Une première analyse fonctionnelle dite externe permet de définir avec précision les limites matérielles du système étudié, les différentes fonctions et opérations réalisées par le système ainsi que les diverses configurations d’exploitation. L’analyse fonctionnelle interne permet de réaliser une décomposition arborescente et hiérarchique du système en éléments matériels et/ou fonctionnels. Elle décrit également des fonctions dans le système.

L’Analyse Préliminaire des Risques

L’Analyse Préliminaire des Risques (APR) est une extension de l’Analyse Préliminaire des Dangers (APD) qui a été utilisée pour la première fois aux Etats -Unis, au début des années soixante [Villemeur 88]. Depuis, cette utilisation s’est généralisée à de nombreux domaines tels que l’aéronautique, chimique, nucléaire et automobile.
Cette méthode a pour objectifs : 1) d’identifier les dangers d’un système et de définir ses causes. 2) d’évaluer la gravité des conséquences liées aux situations dangereuses et les accidents potentiels.
L’APR permet de déduire tous les moyens, toutes les actions correctrices permettant d’éliminer ou de maîtriser les situations dangereuses et les accidents potentiels. Il est recommandé de commencer l’APR dès les premières phases de la conception. Cette analyse sera vérifiée, complétée au fur et à mesure de l’avancement dans la réalisation de système. L’APR permet de mettre en évidence les événements redoutés critiques qui devront être analysés en détail dans la suite de l’étude de sûreté de fonctionnement, en particulier par la méthode des arbres de défaillances qui sera décrite par la suite.

L’Analyse des Modes de Défaillance, de leurs Effets et de leurs Criticités

L’Analyse des Modes de Défaillance, de leurs Effets et de leur Criticité (AMDEC) est une extension naturelle de l’Analyse des Modes de Défaillance et de leurs Effets (AMDE) utilisée pour la première fois à partir des années soixante pour l’analyse de la sécurité des avions [Villemeur 88]. L’AMDEC considère la probabilité d’occurrence de chaque mode de défaillance et la classe de gravité de ces défaillances, mais aussi les classes correspondantes de probabilités d’occurrence plus que les probabilités elles-mêmes. On peut ainsi s’assurer que les modes de défaillance ayant d’importants effets ont des probabilités d’occurrence suffisamment faibles, grâce aux méthodes de conception, aux diverses vérifications et aux procédures de test. Ce type d’analyse a été largement utilisé par la NASA et a été repris dans de nombreux domaines comme l’automobile.

Diagramme de Fiabilité

Un Diagramme de Fiabilité (DdF) permet le calcul de disponibilité ou la fiabilité du système modélisé, mais avec les mêmes restrictions qu’un Arbre de Défaillance (AdD) qui sera présenté dans le § 1.2.2.5), voir pires (pas d’événements répétés). Tous les chemins entre l’entrée et la sortie décrivent les conditions pour que la fonction soit accomplie. On suppose que les composants n’ont que deux états de fonctionnement (fonctionnement correct ou panne).

Les Arbres de Défaillances

L’analyse par Arbre de Défaillance (AdD) est une analyse déductive qui permet de représenter graphiquement les combinaisons d’événements qui conduisent à la réalisation de l’événement redouté. L’arbre de défaillance, dont la racine correspond à l’événement redouté, est formé de niveaux successifs tels que chaque événement soit généré à partir des événements du niveau inférieur par l’intermédiaire d’opérateurs logiques. Le critère d’arrêt de la décomposition arborescente d’un AdD est la connaissance que l’on a et l’appréciation de l’intérêt de la poursuite du processus de décomposition.
L’analyse qualitative par arbre de défaillance consiste à déterminer l’ensemble des coupes minimales. Une coupe est un ensemble d’événements entraînant l’événement redouté. Une coupe est minimale lorsque le retrait d’un événement de la coupe n’entraîne plus l’événement redouté (un arbre de défaillance a un nombre fini de coupes minimales). La recherche des coupes minimales se fait à partir d’une transformation de l’arbre en une expression booléenne et l’utilisation des lois de l’algèbre de Boole pour obtenir une expression booléenne réduite de l’événement redouté. Une autre méthode basée sur les diagrammes de décision binaire (BDD) est présentée dans [Sinnanmon et Andrew 97].
L’analyse quantitative consiste à assigner à chaque événement de base une probabilité d’occurrence. Une méthode d’évaluation de la probabilité d’occurrence de l’événement sommet, basée sur les diagrammes de décision binaire est présentée dans [Rauzy et Dutuit 97].
L’analyse par arbre de défaillance est largement utilisée dans les études de sûreté de fonctionnement car elle caractérise de façon claire les liens de dépendance, du point de vue dysfonctionnement, entre les composants d’un système. Bien que cette méthode soit efficace, elle présente des limites. L’une de ces limites est que l’ordre d’occurrence des événements menant vers l’état redouté n’est pas pris en compte. Or comme nous allons le voir par la suite, cette notion d’ordre dans les événements menant vers une défaillance est primordiale dans les systèmes pilotés par calculateurs qui sont hybrides. Nous présentons dans la section suivante ces systèmes.

Les systèmes pilotés par calculateurs

Un système piloté par calculateur est un système dont la dynamique d’évolution est contrôlée par un calculateur qui utilise des informations fournies par des capteurs pour élaborer sa commande qui sera appliquée au système piloté au moyen d’actionneurs. Aujourd’hui la majeure partie des procédés industriels et des systèmes embarqués est pilotée par calculateurs. On peut citer comme exemple les systèmes mécatroniques, les calculateurs de vols et les systèmes de contrôle des centrales nucléaires, etc.

Cas des systèmes mécatroniques

Un système mécatronique est un système combinant des technologies qui relèvent des domaines de la mécanique, de l’hydraulique, de la thermique, de l’électronique et des technologies de l’information. Il peut être décomposé en quatre entités en interaction (voir figure 1.1) : les capteurs, la partie opérative, le système de commande et de reconfiguration et les actionneurs.
Les capteurs mesurent des grandeurs physiques continues caractéristiques de la partie opérative. Le système de commande et de reconfiguration établit en fonction de ces mesures les actions à réaliser. Les actionneurs agissent sur la partie opérative.
Le système de commande a également pour objectif d’assurer que certaines grandeurs de la partie opérative soient maintenues dans un intervalle de sécurité. Lorsque certains événements relatifs à la sécurité du système se produisent, comme le franchissement d’un seuil de sécurité par une variable caractéristique de la partie opérative, des actions sont mises en œuvre de façon à reconfigurer la partie opérative pour ramener les grandeurs caractéristiques de celle-ci dans les limites permises. Ainsi, pour ce type de système, la sécurité est assurée par des reconfigurations sans interruption de la mission. Ces systèmes sont donc des systèmes à reconfigurations dynamiques.
La reconfiguration peut être de type matérielle ou logicielle. La reconfiguration matérielle consiste à réparer un équipement ou à choisir une nouvelle architecture physique pour réaliser la fonction considérée. La reconfiguration logicielle se base sur la redondance, comme par exemple la redondance analytique des capteurs [Moncelet 98]. La différence entre ces deux types de reconfiguration est dans la vitesse d’exécution et le coût : un changement de configuration matérielle est toujours plus long et plus risqué. Une telle reconfiguration a une probabilité d’échec généralement non négligeable (défaillance à la sollicitation d’un composant).
Les systèmes mécatroniques sont des systèmes hybrides2 dont la dynamique continue est associée à la partie énergétique (mécanique et hydraulique) et la dynamique discrète est liée à la commande numérique et à l’existence d’événements discrets (défaillances, dépassements de seuils).
Les spécificités des systèmes mécatroniques sont liées au fait que :
ƒ ils sont reconfigurables et la décision de reconfiguration est prise par le système lui même.
ƒ la réussite des reconfigurations dépend, dans le cas général, de la dynamique continue de la partie opérative, mais aussi du temps de réaction du système de pilotage.
Dans la partie de notre travail concernant la recherche de scénarios redoutés dans les systèmes mécatroniques nous supposerons que le système de commande et de reconfiguration (calculateur) est exempt de fautes. En effet ces fautes ne remettent pas en cause les bases de la démarche, mais ajouterait à la complexité du système étudié. Nous étudierons uniquement l’effet des défaillances des capteurs, des actionneurs qui causent la défaillance de la partie opérative. Dans le cadre de l’application à la vérification de propriétés il sera intéressant de considérer les fautes des calculateurs.

Exemple de systèmes mécatroniques

On peut énumérer plusieurs exemples de systèmes mécatroniques tels que : l’ABS (Anti Blocking System), l’EPS (Electronic Stability Program), l’ASR (Anti Slip Regulation) plus connu sous le nom Anti-patinage. Le TCS (Traction Control System), le MSR (Motor Schelepp Regulung), l’EBD (Electronics Brakeforce Distribution), le BAS (Braking Assistance System), l’ AFU (Assistance au Freinage d’Urgence), la suspension hydraulique, la suspension pneumatique, etc. Ces systèmes sont utilisés dans le cadre de la sécurité active3 [Kassaagi 01] des voitures d’aujourd’hui. Nous allons détailler ci-dessous quelques-uns de ces systèmes (les plus connus par les utilisateurs). Système d’anti-blocage des roues (ABS) : comme son nom l’indique, ce système empêche le blocage des roues en cas de freinage brutal. Des capteurs situés au niveau des quatre roues, détectent le blocage (ou le risque de blocage) de chacune d’elles et informent toutes les 3 ou 7 millisecondes un calculateur. Ce dernier compare alors la pression exercée sur la pédale de frein, la vitesse du véhicule (détectée par un capteur) et la vitesse des roues. Si une roue est bloquée, le calculateur commande la relâche de la puissance de freinage appliquée sur la roue concernée. Cette action est réalisée par l’utilisation d’électrovalves (ou électrovannes du bloc hydraulique). Une pompe électrique remet de la pression dès que la roue a repris sa vitesse (cette opération peut s’effectuer jusqu’à 12 fois par seconde) . Grâce à un temps de réaction très court, le système peut maintenir chaque roue à la limite du blocage du véhicule permettant alors une décélération maximale et une réduction des distances de freinage. Un deuxième avantage est que le véhicule conserve son adhérence et répond aux sollicitations de la direction. Le conducteur garde ainsi le contrôle de son véhicule. L’ABS a fait son apparition en 1952 sur les avions. Depuis son utilisation s’est élargie au domaine automobile dès 1978.
Afin d’assurer une grande fiabilité pour ce système vu sa criticité, sans compromettre ses performances et ses temps de réponse, les constructeurs l’ont doté de plusieurs stratégies de reconfiguration en cas de défaillance. Comme nous venons de le voir, le système ABS est composé d’un calculateur ABS, de cinq capteurs de vitesse, du système de freinage en parallèle avec quatre électrovannes. Les stratégies de reconfiguration sont nombreuses et complexes. Parmi les plus simples, celle qui consiste à estimer la vitesse de la roue lorsque le capteur associé est diagnostiqué défaillant (détection par le calculateur). La vitesse de la roue est donc estimée au travers des valeurs fournies par les autres capteurs. Selon le mode de défaillance du capteur (dérive, absence de signal, etc.), d’autres modes de reconfiguration sont prévus. Par exemple, en cas de dérive, le capteur est remis à zéro puis réactivé. La concordance de ses valeurs avec celles des trois autres permet de confirmer ou infirmer sa défaillance définitive et donc de poursuivre ou non l’estimation de la vitesse de la roue concernée. Le conducteur est averti à ce moment de la perte du capteur. Si deux capteurs sont défaillants, le voyant STOP est allumé.
Système de contrôle de trajectoire (EPS) : Ce système dit aussi de stabilité est une application récente de l’ABS. Il permet le contrôle de la stabilité du véhicule. L’EPS agit pour remettre la voiture dans une bonne trajectoire suite aux erreurs de conduite. Ce système détecte une tendance au dérapage et corrige en agissant indépendamment sur une ou plusieurs roues par l’intermédiaire des freins et /ou du moteur afin de rétablir la voiture dans son axe. Le système se déclenche suite à une perte d’adhérence du véhicule le plus souvent lors d’un sous-virage (l’avant chasse), d’un sur-virage (l’arrière chasse) ou en cas de manœuvre brutale. Un témoin lumineux signale la perte d’adhérence. De nombreux systèmes tels que l’ABS, EBD et AFU sont aujourd’hui intégrés à l’EPS avec éventuellement des capteurs supplémentaires pour corriger le dérapage du véhicule. L’EPS, comme de nombreux systèmes embarqués, illustre une forte interaction entre les sous-systèmes de l’automobile afin de réaliser une ou plusieurs fonctions. Par exemple le calculateur EPS contrôle le système ABS, le système de freinage et le couple moteur pour maintenir l’adhérence du véhicule.
En effet, l’interaction croissante entre les composants et les interconnections des fonctions pourraient être à l’origine de l’apparition de situations critiques (redoutées) non prévues du fait de la complexité croissante des systèmes automobiles. Ceci rend inefficaces les méthodes de travail des concepteurs basées sur des études et des validations séparées des différents sous-systèmes, auparavant indépendants mais fortement interconnectés aujourd’hui.
L’augmentation du nombre de composants et de fonctions, assurées par l’EPS, rend plus complexe l’élaboration des stratégies de reconfiguration. Une des plus simples, et qui est partagée avec le système ABS, est celle qui consiste à compenser une défaillance des électrovannes alimentant en pression hydraulique le circuit de freinage. Si une des électrovannes est bloquée en ouverture ou en fermeture, le système envoie des trains d’impulsions de forte intensité pendant un certain temps afin de secouer la bobine de commande de l’électrovanne et de la débloquer. Pendant ce temps, l’EPS continue de remplir sa mission dans un mode relativement dégradé en s’appuyant sur les autres électrovannes pour compenser l’excès ou le manque de pression dans le circuit hydraulique.
La réussite de certaines reconfigurations du système EPS est liée aux temps de réponse liés aux grandeurs énergétiques telle que la pression. Cette dépendance entre les aspects continus et discrets place les systèmes mécatroniques dans le cadre des systèmes dynamiques hybrides qui seront présentés dans la section qui suit.

L’aspect dynamique et hybride des systèmes pilotés par calculateurs

Un système hybride est un système qui nécessite dans sa description la prise en compte de sa dynamique continue et de sa dynamique discrète. La dynamique continue est représentée par des variables continues, la dynamique discrète représente les changements d’états dus à l’occurrence d’événements. Ces deux aspects rendent la modélisation hybride indispensable.
Dans son ouvrage [Zaytoon 01] a regroupé un grand nombre de travaux sur les systèmes dynamiques hybrides. Il donne quelques applications sur des systèmes industriels et présente plusieurs modèles dits « hybrides ». Ces modèles peuvent êtres classés selon deux approches : une approche intégrée qui intègre, au sein d’un même formalisme, les aspects continus et discrets ; une approche séparée qui sépare ces deux aspects en faisant coopérer deux modèles différents. L’approche intégrée englobe des modèles issus de l’extension de modèles continus comme les Bond Graphes à commutation [Buisson 93] et ceux issus de l’extension de modèles à événements discrets comme les réseaux de Petri hybrides [David et Alla 89]. L’approche séparée regroupe les modèles à base d’Automates hybrides, de Statecharts hybrides, de réseaux de Petri mixtes ou de réseaux de Petri Prédicats-Transitions-Différentiels (RdP PTD). Dans le chapitre suivant nous détaillerons les principales approches de modélisation de l’aspect hybride basées sur les réseaux de Petri, à savoir les RdP hybrides et les RdP PTD (les RdP Mixtes, peuvent être considérés comme une variante des RdP PTD)
Nous intégrons ainsi la connaissance des conditions d’apparition des défaillances et la réponse du système à ces défaillances dans notre modèle des systèmes pilotés par calculateurs. Ces défaillances agissent sur le processus continu et ce dernier joue un rôle important dans la réussite des reconfigurations et dans l’évaluation de la sûreté de fonctionnement de ces systèmes. Dans la section suivante, nous présentons la sûreté de fonctionnement des systèmes pilotés par calculateurs en évoquant les limites des méthodes classiques ainsi que les différentes méthodes d’analyse et de modélisation.

Sûreté de fonctionnement des systèmes pilotés par calculateurs

Limites des méthodes classiques

Les méthodes classiques de la sûreté de fonctionnement, comme celles présentées dans le §1.2.2 sont statiques. Ces méthodes basées sur la logique booléenne pour représenter le système étudié sont adaptées à des systèmes à configuration statique, c’est-à-dire des systèmes dont les relations fonctionnelles entre leurs composants restent figées.
Dans le cadre de nos travaux, la prise en compte des mécanismes de reconfiguration dans les systèmes pilotés par calculateurs est essentielle. Cet aspect n’est pas pris en compte par les méthodes classiques de sûreté de fonctionnement ce qui les rend inefficaces. Par exemple la méthode des Arbres de Défaillance ne tient pas compte de l’ordre d’apparition des événements dans un scénario. En effet, une séquence d’événements peut conduire à un événement redouté alors que les mêmes événements se produisant dans un ordre différent ou à des dates différentes peuvent l’éviter. Le temps séparant deux événements n’est pas pris en compte dans la méthode des Arbres de Défaillance, les reconfigurations ne peuvent donc pas être représentées. Les défaillances temporaires ne sont pas non plus prises en compte. Plusieurs extensions des méthodes classiques ont été proposées afin d’élargir leurs champ d’application. Citons par exemple les arbres de défaillance avec les portes « A avant B ». Ces méthodes restent combinatoires et incapables de prendre en compte les changements d’états et les reconfigurations dans les scénarios redoutés. D’autres méthodes ont été introduites, comme les Diagrammes de Séquences d’Evénements (Event Sequence Diagrams notés ESD) [Kermisch et Labeau 02] afin de permettre une meilleure représentation visuelle d’événements ordonnés dans le temps. Bien que les ESD représentent de manière claire les scénarios en compétition, ils ne peuvent pas être générés automatiquement et nécessitent une définition des états et des transitions. Tous les états de commande et de reconfiguration doivent donc être énumérés par le concepteur, or dans le cas des systèmes dynamiques hybrides, le nombre d’états est infini si on prend en compte la partie énergétique. Il en est de même pour les méthodes fondées sur les graphes de Markov. Les limites des méthodes basées sur la simulation [Moncelet 98] sont dues à l’explosion combinatoire du nombre d’états, elles simulent alors la plu part du temps le fonctionnement normal du système puisque l’événement redouté est rare en général. Il faut cependant mentionner l’existence de développements théoriques et de méthodes destinés à apporter une solution au problème posé par la simulation de systèmes en présence d’événements rares [Villen-Altamirano]. Il existe en effet des techniques d’accélération de la simulation, largement utilisées avec succès, dans l’ingénierie nucléaire notamment. Dans le cas des réseaux de Petri, cette explosion combinatoire affecte principalement le graphe d’accessibilité, mais épargne, les réseaux de Petri originaux.

Fiabilité des systèmes dynamiques hybrides

La fiabilité des systèmes dynamiques hybrides, dite aussi fiabilité dynamique (dynamic reliability) ou encore Probabilistic Dynamics [Devooght et Smidts 92a], [Smidts et Devooght 92b], [Kermisch et Labeau 02], est une discipline récente dans la sûreté de fonctionnement.
[Kermisch et Labeau 02] définit cette discipline comme « la partie de sûreté de fonctionnement qui étudie de manière intégrée le comportement des systèmes industriels complexes affectés par une évolution dynamique continue sous-jacente ». Le fonctionnement des systèmes pilotés par calculateurs est régi par deux phénomènes : la variation continue et déterministe des paramètres énergétiques et aussi par les sollicitations et défaillances des composants du système, de nature discrète ou stochastique. Ces deux phénomènes sont en interaction, ce qui influence les paramètres de la sûreté de fonctionnement tels que la fiabilité et la sécurité. Les méthodes classiques de sûreté de fonctionnement sont incapables de prendre en compte de manière satisfaisante la dynamique des variables continues correspondant aux paramètres énergétiques [Dufour et Dutuit 02].
Les méthodes de fiabilité des systèmes dynamiques hybrides doivent prendre en compte les interactions du système. Dans la section suivante nous présentons les méthodes de modélisation des systèmes hybrides.

Méthodes de modélisation

Les méthodes les plus adaptées à la modélisation et à l’analyse des systèmes dynamiques hybrides sont les modèles états transitions tels que les graphes d’états (les graphes de Markov et les automates) et les approches basées sur les réseaux de Petri.
Les méthodes de modélisation peuvent être classées selon deux aspects : l’aspect dysfonctionnel qui permet de décrire les défaillances et les réparations ainsi que le comportement du système en présence de dysfonctionnements, l’aspect comportemental qui s’intéresse au comportement des systèmes dynamiques hybrides. La séparation entre ces deux aspects est la plus grande cause de l’inefficacité des méthodes classiques de sûreté de fonctionnement concernant la fiabilité dynamique. Ces deux aspects doivent être intégrés dans un même modèle de fiabilité en respectant leur interaction.

Table des matières

Introduction générale
Chapitre 1 : Sûreté de fonctionnement des systèmes pilotés par calculateurs
1.1. Introduction
1.2. Sûreté de fonctionnement
1.2.1. Concepts de la sûreté de fonctionnement
1.2.2. Méthodes d’analyse de la sûreté de fonctionnement
1.2.2.1 L’analyse fonctionnelle
1.2.2.2 L’Analyse Préliminaire des Risques
1.2.2.3 L’Analyse des Modes de Défaillance, de leurs Effets et de leurs Criticités
1.2.2.4 Diagramme de Fiabilité
1.2.2.5 Les Arbres de Défaillances
1.3. Les systèmes pilotés par calculateurs
1.3.1. Cas des systèmes mécatroniques
1.3.2. Exemple de systèmes mécatroniques
1.3.3. L’aspect dynamique et hybride des systèmes pilotés par calculateurs
1.4. Sûreté de fonctionnement des systèmes pilotés par calculateurs
1.4.1. Limites des méthodes classiques
1.4.2. Fiabilité des systèmes dynamiques hybrides
1.4.3. Méthodes de modélisation
1.4.3.1 Modélisation de l’aspect dysfonctionnel
1.4.3.2 Modélisation de l’aspect fonctionnel
1.4.4. Méthodes d’analyse
1.4.4.1 L’analyse qualitative
1.4.4.2 L’analyse quantitative
1.5. La vérification de propriétés spécifiques
1.5.1. La vérification de modèle
1.5.1.1 Principe et Algorithme du model-checking
1.5.1.2 Les propriétés pouvant être vérifiées
1.5.1.3 Logique temporelle
1.5.1.4 Différents outils de model-checking
1.5.1.5 Limites du model-checking
1.5.2. La preuve
1.5.2.1 Preuve informelle
1.5.2.2 Preuve formelle
1.5.2.3 Quelques outils et environnements de preuve
1.5.2.4 Limites de la preuve
1.5.3. Le test
1.5.4. Couplage de techniques de vérification
1.6. Tour d’horizon : sûreté et recherche des scénarios
1.6.1. Travaux de J.L Chabot
1.6.2. Méthode des graphes de flux dynamiques
1.6.3. Travaux de G.Moncelet
1.6.4. Travaux de Raphaël Schoenig
1.6.5. Travaux de Claudia Betous-Almeida
1.6.6. Langage de modélisation AltaRica
1.6.7. Travaux de Nicolas Rivière
1.6.8. Travaux de Sarhane Khalfaoui
1.7. Conclusion et Analyse
Chapitre 2 : Modélisation des systèmes hybrides et notion de scénario
2.1. Introduction
2.2. Modélisation des systèmes temporisés et hybrides
2.2.1. Modélisation avec les RdP temporisés et les RdP temporels.
2.2.1.1 Les RdP t-temporisés
2.2.1.2 RdP P-temporisés
2.2.1.3 RdP t-temporels
2.2.1.4 RdP p-temporels
2.2.1.5 RdP arc-pt-temporels
2.2.2. Modélisation avec les RdP hybrides
2.2.2.1 RdP hybride
2.2.2.2 Les RdP Prédicats-Transitions Différentiels Stochastiques
2.3. Abstraction temporelle de fonctionnements hybrides
2.4. Notion de scénario redouté
2.4.1. Introduction
2.4.2. Exemple de constellation de satellites
2.4.3. L’approche classique
2.4.4. Scénario défini à partir d’un automate fini
2.4.5. Graphe de précédence et ordre partiel
2.4.6. Scénarios et logique temporelle linéaire
2.5. Scénario et logique linéaire
2.5.1. Modélisation logique
2.5.1.1 Introduction à la logique linéaire : fragment MILL
2.5.1.2 Traduction des RdP en logique linéaire
2.5.1.3 Equivalence entre accessibilité et preuve
2.5.2. Preuve d’un séquent caractéristique
2.5.3. Formalisation du scénario en RdP et en Logique Linéaire
2.5.3.1 Arbre de preuve canonique de l’exemple
2.5.3.2 Etiquetage de l’arbre de preuve canonique
2.5.3.3 Obtention du graphe de précédence
2.6. Définition et propriétés d’un scénario critique
2.6.1. Définition d’un scénario
2.6.2. Conditions suffisantes
2.6.3. Scénario minimal
2.7. Méthode d’extraction des scénarios redoutés
2.7.1. Principe
2.7.2. Les différentes étapes
2.7.2.1 Détermination des états nominaux
2.7.2.2 Détermination des états cibles
2.7.2.3 Raisonnement arrière
2.7.2.4 Raisonnement avant
2.7.3. Enrichissement de marquage
2.7.3.1 Définition
2.7.3.2 Mécanisme de contrôle de la cohérence
2.7.4. Limites
2.8. Conclusion
Chapitre 3 : Recherche de scénarios dans les systèmes hybrides
3.1. Introduction
3.2. Méthode d’extraction des scénarios dans un système hybride
3.2.1. Principe
3.2.2. Prise en compte du continu par des abstractions temporelles
3.2.2.1 Principe
3.2.2.2 Précédence et causalité directe et indirecte
3.2.2.3 Cas de priorités entre les franchissements des transitions
3.2.2.4 Retour sur le principe de l’amélioration de l’algorithme
3.2.3. Algorithme de recherche de scénarios dans un système hybride
3.2.3.1 Structure des données
3.2.3.2 Procédures
3.2.3.3 Différentes étapes du l’algorithme
3.3. Application de l’algorithme sur un cas d’étude
3.3.1. Présentation du cas d’étude
3.3.2. Application de l’algorithme
3.3.2.1 Raisonnement arrière
3.3.2.2 Raisonnement avant
3.3.3. Discussion
3.4. Conclusion
Chapitre 4 : Mise en oeuvre d’un prototype d’outil : ESA_PetriNet
4.1. Introduction
4.2. Description générale d’ESA_PetriNet
4.3. L’outil TINA
4.4. Interfaçage entre TINA et ESA_PetriNet
4.5. Récupération des informations nécessaires par ESA_PetriNet
4.6. Utilisation d’ESA_PetriNet
4.7. Exemple et comparaison avec l’ancienne version de l’algorithme
4.8. Conclusion
Chapitre 5 : Un exemple de recherche de scénarios redoutés
5.1. Introduction
5.2. Présentation de l’exemple
5.2.1. Description générale
5.2.2. Fonctionnement du système
5.2.3. Evénements redoutés
5.2.4. Composition du système
5.2.5. Modélisation du système
5.2.6. Modélisation de la sortie des trains d’atterrissage avec défaillance
5.2.6.1 Modèle réseau de Petri de l’ouverture d’une trappe
5.2.6.2 Modèle réseau de Petri de l’ouverture des trois trappes
5.3. Génération de scénarios par ESA_PetriNet
5.4. Comparaison des résultats
5.4.1. Avec l’aspect contiu
5.4.2. Sans l’aspect continu
5.5. Génération de scénarios dans le réseau global
5.6. Conclusion
Chapitre 6 : Deux exemples de vérification de propriétés temporelles
6.1. Introduction
6.2. Principe de l’utilisation d’ ESA_PetriNet pour la vérification
6.3. Exemple 1 : trains d’atterrissage
6.3.1. Modèle réseau de Petri pour la sortie d’un train
6.3.2. Modèle de réseau de Petri pour la rentrée
6.3.3. Première analyse et abstraction temporelle
6.3.3.1 Analyse des invariants
6.3.3.2 Délimitation des domaines des variables continues
6.3.3.3 Abstraction temporelle
6.3.4. Génération des scénarios et des réseaux de contraintes temporelles
6.3.5. Comparaison des scénarios
6.4. Exemple 2 : Calculateurs de vol
6.4.1. Spécification et modélisation du système
6.4.1.1 Description générale
6.4.1.2 Modèle global
6.4.1.3 Modélisation du comportement du calculateur Fr
6.4.1.4 Modélisation du comportement des calculateurs Fl et Fb
6.4.1.5 Modélisation du comportement de Clr
6.4.1.6 Modélisation du comportement de Clrb
6.4.2. Génération des scénarios par ESA_PetriNet et analyse
6.4.2.1 Analyse du système global par TINA
6.4.2.2 Recherche de scénarios par ESA_PetriNet
6.4.2.3 Prise en compte de priorités entre des transitions
6.5. Conclusion
Conclusion générale
Glossaire
Bibliographie

Télécharger le rapport complet