Soutenance mémoire
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.
Modélisation de l’aspect dysfonctionnel
Graphes de Markov : cette méthode est utilisée pour analyser et évaluer la sûreté de fonctionnement des systèmes réparables. La construction d’un graphe de Markov consiste à identifier les différents états du système (défaillants ou non défaillants) et chercher comment passer d’un état à un autre lors d’un dysfonctionnement ou d’une réparation. A chaque transition, de l’état Ei vers l’état Ej, est associé un taux de transition Lij défini de telle sorte que Lij.dt est égal à la probabilité de passer de Ei vers Ej entre deux instants très proches t et t+dt sachant que l’on est en Ei à l’instant de temps t.
La modélisation avec les graphes de Markov permet de prendre en compte les dépendances temporelles et stochastiques plus largement que les méthodes classiques. En dépit de leur simplicité conceptuelle et leur aptitude à pallier certains handicaps des méthodes classiques, les graphes de Markov souffrent de l’explosion du nombre des états, car le processus de modélisation implique l’énumération de tous les états possibles et de toutes les transitions entre ces états. Ce problème peut se poser même dans le cas de la modélisation du seul aspect dysfonctionnel, mais il devient un handicap énorme si on souhaite rajouter la description de l’aspect fonctionnel à celui de l’aspect dysfonctionnel. Pour surmonter ce problème, on peut alors s’orienter vers les réseaux de Petri stochastiques.
Réseaux de Petri stochastiques : les réseaux de Petri stochastiques [Molloy 82], [Natkin 80], [Chiol et al 93] sont obtenus à partir des réseaux de Petri classiques en associant des durées de franchissement aléatoires aux transitions. Ils permettent de prendre en compte, de manière plus structurée que les graphes de Markov, l’occurrence des défaillances et leur influence sur le comportement du système. En effet, le parallélisme étant pris en compte ils permettent d’expliciter l’architecture du système en décrivant indépendamment les états des divers objets composant le système et leurs interactions.
Une extension nommée « Réseaux de Petri Stochastiques Généralisés « (RDPSG) [Marsan et al 84] permet de prendre en compte, en plus de transitions avec des lois exponentielles, d’autres transitions dites « immédiates » tirées sans délai et qui sont prioritaires par rapport aux transitions à délai aléatoire. On peut citer d’autres extensions telles que les Réseaux de Petri Stochastiques Etendus (RdPSE) [Dugan et al 84] et les Réseaux de Petri Stochastiques et Déterministes (RdPSD) [Marsan et Chiola 86]. Les RdPSE permettent de prendre en compte des lois de distribution quelconques et les RdPSD combinent des délais exponentiellement distribués et des délais constants.
Dans le paragraphe ci-dessous, nous présentons les formalismes de modélisation de l’aspect fonctionnel : il s’agit donc de décrire le fonctionnement normal du système.
Modélisation de l’aspect fonctionnel
La prise en compte de l’aspect hybride des systèmes dynamiques hybrides est essentielle pour évaluer leur sûreté de fonctionnement en explicitant l’aspect fonctionnel.
Les automates : les automates sont l’un des formalismes états transitions les plus utilisés dans la description des systèmes à événements discrets. Ce formalisme a été étendu sous la forme des automates hybrides pour modéliser correctement les systèmes dynamiques hybrides. Les automates hybrides sont une extension des automates temporisés4 [Alur et al 95]. Informellement, un automate hybride est l’association d’un automate à états finis et d’un ensemble d’équations dynamiques continues pilotées par ce dernier.
Le point faible de ce formalisme est l’explosion combinatoire du nombre d’états du graphe. Pour éviter ce problème, dans le cas de la modélisation des systèmes complexes pouvant être découpés en sous-systèmes, il est possible de construire un modèle d’automate pour chacun d’eux et de les composer ensuite pour élaborer l’automate correspondant au système global. La composition se fait par synchronisation entre les automates des différents sous-systèmes, soit par messages, soit par variable partagées. Toutefois cette composition entre automates rend difficile l’analyse de leurs propriétés. D’où le besoin de disposer de mécanismes de structurations plus puissants offerts par des modèles de plus haut niveau comme les Statecharts [Harel 87].
Les relations de cause à effet menant vers l’état redouté ne sont pas représentées d’une façon claire et homogène avec les automates. En effet au sein d’un automate représentant un objet séquentiel (élément d’un produit d’automates ou d’un ensemble d’automates communicants), les relations de cause à effet sont représentées par les événements qui relient, chacun, un état origine et un état destination. Chaque événement correspond à une causalité explicite entre deux états. Par contre entre deux automates, ces relations de cause à effet sont la conséquence directe ou indirecte de synchronisations par messages ou de communication par variables partagées. L’existence d’une relation de causalité ou non dépendra de la valeur du message ou de la façon suivant laquelle la variable partagée est modifiée et testée. Cela donne une représentation non unifiée des relations de cause à effet inter et intra automates. Dans le paragraphe suivant, nous verrons que ce n’est pas le cas dans le formalisme des réseaux de Petri.
Les réseaux de Petri et l’approche hybride : les réseaux de Petri sont très utilisés dans la modélisation des systèmes à événements discrets et dans les études de sûreté de fonctionnement des systèmes dynamiques. Ils sont caractérisés par une évolution asynchrone dans laquelle les transitions des composantes parallèles sont franchies les unes après les autres, et par une représentation explicite des synchronisations et des mécanismes d’allocation. Plusieurs extensions des réseaux de Petri ont été élaborées pour répondre à la modélisation des problèmes spécifiques et pour maîtriser la taille et la lisibilité des modèles. L’un des points forts des réseaux de Petri par rapport aux autres formalismes comme les Statecharts, repose sur ses fondements théoriques qui lui permettent de vérifier les propriétés générales d’un modèle (vivant, réinitialisable, sans blocage ou borné, etc.,) ainsi que l’accessibilité de certains marquages. Les méthodes de recherche de propriétés dans les réseaux de Petri sont basées sur l’élaboration du graphe des marquages accessibles, sur l’algèbre linéaire (calcul des invariants de places et des transitions), la réduction des réseaux ainsi que sur la logique linéaire qui permet de caractériser les relations d’ordre partiel.
Parmi les diverses extensions des réseaux de Petri pour prendre en compte l’aspect hybride, on peut citer les réseaux de Petri de haut niveau, les réseaux de Petri hybrides et les réseaux de Petri couplés avec les équations algébro-différentielles qui seront détaillés dans le chapitre suivant.
Nous abordons dans la section suivante les méthodes d’analyse qualitatives et quantitatives des systèmes dynamiques hybrides.
Méthodes d’analyse
Les études de sécurité des systèmes pilotés par calculateur sont souvent basées sur une analyse qualitative ayant pour objectif la détermination des scénarios aboutissant à l’occurrence de l’état redouté, suivie d’une analyse quantitative pour estimer la probabilité de leur apparition.
L’analyse qualitative
Cette analyse a pour but de caractériser les scénarios redoutés par des changements d’états et des enchaînements d’événements qui conduisent le système vers un état dit redouté. Quel que soit le formalisme choisi pour la modélisation du système, nous pouvons procéder par exploration des états. On génère les trajectoires possibles du système : les exécutions de l’automate ou les séquences de tirs du réseau de Petri. On détermine ensuite toutes les séquences permettant l’accessibilité d’un état donné par exploration du graphe des états.
Bien que cette approche ait l’avantage d’être exhaustive, elle souffre de deux inconvénients majeurs. Le premier, est qu’elle est limitée par le problème classique de l’explosion combinatoire du nombre d’états due d’une part à la taille des systèmes et d’autre part à l’augmentation du nombre d’états suite à la discrétisation des variables continues. Notons quand même que sans hypothèses ajoutées, le nombre de scénarios possibles est infini. Le second inconvénient est dû au traitement du parallélisme dans le graphe des marquages accessibles par entrelacement qui a pour conséquence l’obligation de ne décrire le comportement discret que par des séquences. Or dans une séquence, ce n’est pas parce qu’un franchissement de transition t2 suit un franchissement de t1 que t1 est la cause nécessaire de t2. Ce n’est le cas que si un jeton produit par t1 est consommé par t2. On ne trouve pas cette information dans le graphe des marquages ce qui rend difficile l’automatisation de l’extraction des scénarios minimaux et des ordres partiels.
Il y a donc un besoin, celui de trouver un autre outil permettant de prendre en compte le parallélisme sans entrelacement et de décrire le comportement discret sans énumérer des séquences. Nous essaierons de répondre à ce besoin en introduisant, dans le chapitre suivant, la notion de scénario.
L’analyse quantitative
Méthodes analytiques : Ces méthodes consistent à résoudre les équations de Chapman-Kolmogorov associées au graphe de Markov. Celles- ci donnent l’évolution temporelle de la probabilité d’être dans un état, sous l’hypothèse que les processus de défaillance et de réparation des composants du système suivent une loi exponentielle à taux constant (hypothèse Markovienne).
Méthodes de discrétisation : Le problème majeur des systèmes pilotés par calculateurs provient de leur nature hybride. Une approche possible consiste à discrétiser les variables continues. Le temps peut également être discrétisé ou non. On peut citer la méthode la plus utilisée en fiabilité dynamique : les Arbres Dynamiques Discrets (Discrete Dynamic Event Trees ou DDET).
Cette méthode a pour but de générer les scénarios redoutés obtenus par propagation des défaillances des composants élémentaires du système. Elle est basée sur la partition de l’espace des variables continues en cellules disjointes. A partir d’un modèle qui prédit la réponse du système aux défaillances, l’évolution des variables physiques est calculée à chaque pas du temps. A cet instant on calcule de même la probabilité de toutes les combinaisons des états des composants et on génère toutes les séquences d’événements constituant les scénarios possibles, et ainsi de suite jusqu’à ce qu’un état absorbant soit atteint. Une présentation détaillée de cette technique est donnée dans [Moncelet 98] et [Kermisch et Labeau 02].
Les méthodes comme DYLAM (Dynamic Logical Analytical Methodolgy) et DETAM (Dynamic Event Tree Analysis Method) s’inscrivent dans le cadre des DDET et ont été appliquées à des systèmes de taille industrielle [Devooght et Smidts 94] [Acosta et Siu 93]. Ces méthodes ont été développées afin de mieux gérer les multiples scénarios générés.
Simulation de Monte Carlo : Quand l’hypothèse Markovienne n’est pas vérifiée, ce qui est le cas d’un grand nombre de systèmes industriels complexes, les évaluations se font par la simulation de Monte Carlo. La simulation de Monte Carlo est une méthode numérique basée sur le tirage de nombres aléatoire [Kermisch et Labeau 02]. Elle permet d’estimer l’espérance mathématique d’une variable aléatoire qui est une fonction de plusieurs paramètres. Elle permet également d’estimer toute quantité, déterministe ou stochastique, dont la valeur a pu être associée à l’espérance mathématique d’une variable aléatoire qui n’est pad directement liée à la physique du problème étudié. Citons par exemple l’exemple historique de l’estimation du nombreπ . L’utilisation de la simulation Monte Carlo dans l’étude de sûreté de fonctionnement, permet de lever l’hypothèse markovienne et permet de traiter des systèmes industriels. Différentes méthodes ont été développées, comme les méthodes de transition forcées depuis le milieu des années 80 qui permettent de réduire le nombre d’histoires à simuler qui est un problème majeur dans le cadre des systèmes mécatroniques [Moncelet 98]. D’autres techniques se sont basées sur la réduction de temps d’une histoire. Des méthodes pour accélérer la simulation ont été développées dans [Champagnat 98].
D’autres approches, couplant la simulation de type DDET à du Monte Carlo, ont également été développées afin d’investiguer de manière plus efficace l’ensemble de l’arbre d’événements consécutif à un événement initiateur. Citons dans ce cadre l’approche Monte Carlo Dynamic Event Tree (MCDET) développée et testée par [Hofer et al 01] et les skeleton-based techniques. L’approche MCDET permet un traitement approximatif des transitions aléatoires continues et également des transitions aléatoires discrètes. Une évaluation de l’erreur d’approximation est fournie par cette méthode.
Discussion: Une idée récurrente est qu’il faut travailler avec des probabilités conditionnelles et donc déterminer des états, ou des classes d’états, de probabilité connue, et qui sont tels qu’à partir d’eux le système a une grande probabilité d’évoluer vers un état redouté. La détermination de tels états (ou de telles classes d’états) s’apparente fortement à un problème de vérification (pour la vérification, la grande probabilité est remplacée par la certitude). C’est pourquoi nous allons étudier les techniques de vérification et de preuve dans la section suivante.
La vérification de propriétés spécifiques
La vérification consiste à déterminer si le système satisfait certaines propriétés. La vérification a pour but de révéler les fautes de conception qui ont pu être introduites au cours de n’importe quelle phase du cycle de développement. Pour des raisons de coût et d’efficacité, il est important de les révéler au plus tôt, et les vérifications doivent être intégrées dès le début et tout au long du processus de développement.
On distingue quatre grandes classes de techniques de vérification : l’analyse statique, la vérification de modèle (ou model-checking), la preuve et le test. Ces techniques sont en général utilisées d’une manière indépendante : une technique est choisie selon l’étape de développement pour un problème de vérification donné. On ne présente dans la suite que les techniques qui nous intéresse. Certains travaux présentés au paragraphe 1.5.4 ont choisi un couplage entre techniques pour exploiter leur complémentarité au sein d’un même problème de vérification.
La vérification de modèle
La vérification de modèle ou le model checking [Schnoebelen 99] est une technique de vérification formelle qui est développée afin de permettre une vérification automatique et exhaustive de systèmes. Elle s’applique à une large classe de systèmes : protocoles de communication, réseaux téléphoniques, industrie manufacturière, systèmes embarqués, etc.
Principe et Algorithme du model-checking
Le principe du model-checking, ou vérification de modèle, est de vérifier de façon exhaustive des propriétés portant sur un modèle du système étudié. La vérification d’un système par la méthode du model -checking nécessite trois étapes : la modélisation formelle du système sous forme d’un automate fini (ou une variante de cette représentation), l’expression formelle de la propriété souhaitée par une formule dans une logique temporelle et l’algorithme de model-checking qui parcourt de façon exhaustive l’automate en vérifiant la formule pour chacun de ses états. On montre en fait que l’automate est un modèle (au sens logique du terme) de la formule. Cet algorithme est implémenté dans le model- checker (outil). La plupart des model-checkers sont capables de générer une réponse positive si la propriété est garantie pour tous les comportements du modèle et une réponse négative complétée par un contre-exemple illustratif en cas de violation de la propriété. Une fois la vérification faite, elle n’est valable que pour un modèle donné. Si une modification est apportée au modèle, il faut reconstruire tous les états pour pouvoir de nouveau affirmer que la propriété vérifiée est vraie.
Les propriétés pouvant être vérifiées
Nous distinguons dans les travaux sur le model-checking, plusieurs types de propriétés qui peuvent être classées différemment. Nous présentons dans ce paragraphe une classification des propriétés temporelles souvent rencontrées dans les travaux de spécification des systèmes temps réel.
Propriétés d’atteignabilité (reachability) : certains auteurs parlent d’accessibilité, elles énoncent que, sous certaines conditions, un état du système peut être atteint ou non, par exemple, une défaillance peut survenir, possibilité de revenir à l’état initial du système, possibilité d’effectuer certaines commandes, etc.
Propriétés de sûreté (safety) : qui énoncent que, sous certaines conditions, quelque chose n’arrive jamais. Par exemple, un état non souhaité ne se produit jamais, deux systèmes ne seront jamais simultanément en état critique. Les propriétés de sûreté peuvent être exprimées sous d’autres formes, par exemple la non atteignabilité.
Propriétés de vivacité (liveness) : qui énoncent que, sous certaines conditions, quelque chose finit par avoir lieu. Plusieurs formes de vivacité sont distinguées entre autre, la vivacité de progrès ou simple et la vivacité bornée : 1) Propriétés de vivacité simple (ou de progrès) qui énoncent qu’un état est toujours atteignable. Par exemple, une commande sera nécessairement émise, le système peut toujours retourner à l’état initial. 2) Propriétés de vivacité bornée (bounded liveness) qui énoncent que, sous certaines conditions, quelque chose finit par avoir lieu avant un certain temps. Par exemple : une panne arrivera dans la journée, toute requête finira par être satisfaite en moins de 5min.
Model-checker quantitatif à temps continu
Les model-checkers à temps continu ont été introduits pour la vérification des systèmes temps réel temporisés ou hybrides. Ils sont considérés à temps continu, car ils utilisent des variables d’horloge valuées réellement. Nous citons les model-checkers les plus répandus :
UPPAAL [Larsen et al 97] : est développé par P.Pettersson à l’université d’UPPsala (UPP) en Suède et Kim Larsen à l’université d’AALborg au Danemark (AAL), d’où son nom. Cet outil présente l’avantage d’offrir une interface graphique de bonne qualité. D’autre part, il permet de simuler le fonctionnement des automates temporisés, ce qui peut être utile dans la phase de modélisation. Cependant, cet outil utilise uniquement un fragment de TCTL et celui-ci ne permet de vérifier que des propriétés d’accessibilité sur des automates temporisés et ne permet pas de vérifier l’ensemble des formules TCTL, les opérateurs de temps ne pouvant pas être imbriqués. Un exemple de succès de UPPAAL a été de permettre le diagnostic, et la correction, d’une faute de conception dans un protocole audio/vidéo [Havelund et al 97]. Ce protocole, utilisé depuis plusieurs années dans l’électronique grand public, manifestait parfois un comportement erroné mais il n’avait pas été possible jusque là d’en déterminer la cause.
KRONOS [Yovine 97], [Bogza et al 98] : a été développé au laboratoire VERIMAG (Grenoble, France). Il permet de déterminer si un système temporisé, décrit comme la composition parallèle de plusieurs automates temporisés, satisfait une propriété exprimée par une formule dans la logique TCTL. Le point fort de KRONOS est l’expressivité de sa logique : KRONOS implante un algorithme de model-checking pour la logique TCTL. Il peut ainsi vérifier des propriétés d’atteignabilité, de sûreté et il est l’un des rares outils permettant de spécifier et vérifier des propriétés temporelles qui ne se ramènent pas à une propriété d’atteignabilité, comme la vivacité.
KRONOS propose des techniques de réduction de l’espace d’états afin d’optimiser les vérifications. Il intègre des techniques d’ordre partiel [Pagani 96] et propose d’optimiser le nombre d’horloges dans un système [Daws et Yovine 96]. L’idée est d’éliminer les horloges inutiles en fonction des gardes et remises à jour des transitions. Seules certaines réductions sont implantées dans KRONOS puisque trouver le nombre minimal d’horloges nécessaires pour un automate temporisé est un problème indécidable et que l’heuristique proposée est NP-Complète. Un outil, TAXYS [Closse et al 01], a été développé intégrant KRONOS avec le langage ESTEREL [Berry et Gonthier 92].
HYTECH [Henzinger et al 97] : est développé à l’université de Berkeley (Californie, USA). Il est conçu pour la vérification des systèmes hybrides linéaires, (et donc utilisable pour les automates temporisés), pour lesquels la loi d’évolution de certaines variables réelles est régie par une équation différentielle linéaire. Dans le cas hybride il y a toujours des variables discrètes et des horloges. Ainsi HYTECH permet de vérifier des propriétés exprimées en TCTL à partir d’une spécification du comportement par des automates hybrides linéaires. Les analyses sont limitées à des propriétés d’atteignabilité. HYTECH a été utilisé dans plusieurs cas d’étude, principalement des systèmes de contrôle [Stauner et al 97].
CMC [Laroussinie et Larsen 98] : (Compositional Model Checking) est un outil dédié aux automates temporisés. Ce model-checker propose une approche de vérification de formules par composition. CMC a pour but d’utiliser la structuration des spécifications en un réseau d’automates temporisés communiquant pour éviter l’explosion combinatoire de l’espace de recherche.
Mec [Arnold 90], [Arnold et Brlek 95] : est développé au LaBRI (Bordeaux, France). Il est utilisé pour la recherche de points de blocage, ou d’autres propriétés d’un système de transitions donné. Le formalisme utilisé pour décrire les systèmes est le modèle de Arnold-Nivat [Arnold et Nivat 82], qui est suffisamment général pour s’adapter à de nombreux formalismes. Une extension MecV [Vincent 03] a été réalisée pour manipuler les modèles du langage Altarica qui sera présenté dans le paragraphe 1.6.6.
TINA [Berthomieu et Menasche 83], [Berthomieu et al 03] (Time Petri net Analyzer): si la représentation du système est fondée sur des réseaux de Petri, la prise en compte des contraintes temporelles dans un contexte de vérification se fait, à l’heure actuelle, le plus souvent sous la forme des réseaux de Petri t-temporels. Bien qu’il soit possible de développer des techniques permettant la traduction d’un réseau de Petri t-temporel, qui sera présenté dans le paragraphe 2.2.1.3, en un automate temporisé pour utiliser les outils décrits ci-dessus, il semble plus efficace de constituer directement une structure de Kripke (développée dans les années 60 par Saul Kripke), adaptée à la propriété à vérifier. Comme nous sommes en présence de système ayant un ensemble infini d’états (à cause de temps dense) ces structures sont formées d’un ensemble fini de classes d’états. L’outil TINA offre actuellement la possibilité de construire deux types de graphe de classes d’état : le type W est suffisant pour la vérification de propriétés exprimées en LTL alors que le type A, qui génère plus de classes, est nécessaire pour la vérification de propriétés exprimées en CTL. Dans les deux cas, les classes sont représentées par un marquage et un ensemble d’inéquations temporelles.
Limites du model-checking
Une des limites du model-checking est la représentativité du modèle formel du système dont le niveau d’abstraction ne permet pas de prendre en compte tous les aspects liés au système et à son environnement, en particulier ceux concernant les fautes physiques. Une autre limite du model-checking est l’explosion du nombre d’états du modèle formel utilisé. Certains auteurs ont apporté des solutions pour limiter l’explosion combinatoire. A titre d’exemple, une stratégie combinant deux approches d’exploration partielle est présentée dans [Ribert et al 02]. D’autres approches ont été proposées par [Merz 01]. Le model-checking symbolique [Burch et al 92] utilise des représentations compactes d’ensembles d’états, on évite ainsi d’avoir à les énumérer. En particulier, la représentation d’ensembles d’états par des BDD (Binary Decision Diagrams) [Bryant 86], [Bryant 92] est très utilisée dans ce cadre. Les techniques d’ordre partiel évitent, dans un système composé d’automates en parallèle, d’avoir à parcourir tous les chemins d’exécutions possibles (voir par exemple [Holzmann et Peled 94], [Ribet et al 02]). Le principe sous-jacent est que pour vérifier la propriété, certains entrelacements d’événements équivalents ne sont pas construits.
Comme nous l’avons déjà écrit, il y a une grande similitude entre la vérification d’une propriété par model-checking et la recherche des comportements redoutés. Dans le premier cas on cherche à montrer qu’un état est inaccessible et l’on obtient un comportement y menant s’il est en fait accessible. Dans le deuxième cas on désire caractériser tous les comportements menant à un état redouté avec une probabilité d’occurrence d’un tel comportement. S’il y a similitude, cela ne veut pas forcément dire que la recherche des comportements redoutés peut facilement se faire en utilisant le model-checking. En effet, si le comportement recherché est « événement a » en parallèle avec « événement b », l’outil de model-checking peut très bien produire des séquences comme « événement a » puis « événement c » puis « événement b », ou bien « événement b » puis « événement d » puis « événement a » où b et d correspondent à des événements qui se sont produits par hasard, sans lien de causalité avec le fait d’atteindre l’état redouté. Non seulement ces comportements risquent de ne pas être très clairs pour le concepteur, mais il sera de plus bien difficile de passer à une évaluation quantitative de la probabilité d’occurrence. En résumé il sera difficile de garantir la complétude des comportements et surtout d’obtenir une caractérisation simple et minimale de l’ensemble des comportements redoutés.
La preuve
La preuve consiste à établir par une suite finie d’étapes de raisonnement (par mécanisme déductif ou par un système de réécriture) appelées inférence, qu’une certaine propriété est la conséquence logique d’axiomes ou d’un ensemble d’hypothèses décrivant le système étudié.
La preuve peut être appliquée à toutes les phases de développement du système, on peut par exemple chercher à prouver :
Qu’une spécification satisfait certaines bonnes propriétés
Qu’une étape de conception est correcte : une spécification détaillée satisfait une spécification plus abstraite (preuve de raffinement)
Qu’un programme est correct par rapport à une spécification détaillée (preuve de programme), ou qu’il termine toujours sous certaines conditions (preuve de terminaison).
Une preuve peut être formelle ou informelle.
Preuve informelle
Une preuve informelle est une démonstration donnée en langage naturel, en utilisant éventuellement quelques notions mathématiques pour faciliter le discours. Dans le domaine informatique, la plupart des algorithmes de tolérance aux fautes sont publiés avec une preuve informelle. Une preuve informelle est validée par consensus : elle est lue et acceptée par les pairs. Ceci la distingue de la preuve formelle, qui peut être vérifiée automatiquement par des outils car le problème de vérification a été entièrement exprimé à l’aide des mathématiques.
Preuve formelle
L’assistance d’outil de preuve dans la preuve formelle nécessite la formalisation complète du problème de vérification. La description de l’algorithme, les hypothèses sur son environnement, et les propriétés attendues doivent être exprimées dans un langage ayant une syntaxe et une sémantique formelles, s’appuyant sur un cadre logique bien défini. Dans ce cadre, une preuve se ramène alors à des manipulations syntaxiques de formules. Les règles d’inférence indiquent comment produire des formules à partir des formules déjà produites, et une preuve peut être vue comme la construction d’un arbre de formules, dont les feuilles sont des axiomes et la racine la formule à prouver. Un cadre classique de preuve est le calcul des prédicats du premier ordre : il permet de raisonner sur des formules qui comportent des variables. Deux exemples de systèmes de déduction pour ce calcul sont la déduction naturelle et le calcul des séquents [Monin 00].
Il n’existe pas de procédure de décision qui, pour toute formule, déterminerait s’il existe une preuve ou non. Les démonstrateurs de théorèmes doivent donc mettre en œuvre des heuristiques, sans garantie d’aboutissement. En pratique, l’intervention d’un opérateur humain est souvent nécessaire pour guider la construction de la preuve. Malheureusement, il y a toujours le risque de se retrouver dans un cas d’échec de preuve : on ne peut arriver à déterminer si la formule à prouver est vraie ou non. L’investissement qu’a représenté la preuve a alors été inutile, ce qui constitue un sérieux inconvénient à l’utilisation de cette technique de vérification.
Pour permettre à l’utilisateur de comprendre la structure de la preuve, et faciliter l’analyse des parties en échec, il est souhaitable que l’environnement offre des facilités pour visualiser l’arbre de preuve. L’outil doit offrir une certaine visibilité sur les heuristiques qu’il a essayé de mettre en œuvre. L’arbre peut être montré à différents niveaux d’abstraction, par exemple en détaillant ou non les tactiques utilisées et les preuves de certains lemmes intermédiaires. Une étude des caractéristiques souhaitables des environnements de preuve peut être trouvée dans [Rushby 93]
Nous présentons ci-dessous quelques outils et environnements de preuve existants.
Quelques outils et environnements de preuve
Il existe de nombreux systèmes de preuve. Selon le degré d’automatisation de la preuve, on parlera de vérificateur de preuve qui se contente de vérifier une preuve déjà construite, d’outil d’assistance à la preuve, ou de démonstrateur de théorèmes. Parmi ces outils nous citons :
Boyer-Moor : est un des ancêtres des démonstrateurs de théorèmes. Il est basé sur un système formel particulier, la logique de Boyer-Moor [Boyer et Moor 79] dans laquelle sont exprimées les propriétés à démontrer. Boyer-Moore comporte plusieurs heuristiques puissantes lui permettant de trouver des preuves non triviales, comme des preuves par introduction de lemmes. Il a été utilisé dans le projet SIFT [Wensly et al 78] dans les années 80.
LP (Larch Prover) [Garland et Guttag 91] : la spécification dans cet outil de vérification de preuve se fait en langage Larch [Guttag et al 85]. Le système est fondé sur un ensemble de fonctions déclarées, des propriétés et des axiomes sont exprimés sous forme d’équations, des règles de réécriture, des règles de déduction et des règles d’induction. La construction des preuves est assistée par le système TLP ( Temporal Logic Prover) [Engberg 95] qui offre une extension du langage Larch pour la logique temporelle TLA (Temporal Logic of Action).
LCF (Logic of Computable Functions) [Gordon et al 79] : est un des premiers démonstrateurs de théorèmes. Il a été programmé en ML et son langage sert également à écrire des stratégies de preuve. LCF a aussi introduit le terme de tactique et l’idée de preuve à l’envers : un utilisateur commence avec le but désiré et divise ce but en sous-buts plus simples en appliquant des tactiques. C’est l’inverse de la façon dont les preuves mathématiques sont traditionnellement écrites.
Hol (Higher Order Logic) [Gordon et Melham 93] : il a été développé principalement à l’université de Cambridge. Ce démonstrateur de théorèmes a été utilisé essentiellement pour des preuves de conception de matériel notamment celle du microprocesseur tolérant aux fautes Viper pour le RSRE (Royal Signals and Radars Establishment du ministère de la défense Britannique). Un des aspects les plus attrayants de ce système est la possibilité de définir des tactiques de démonstration adaptées à certains problèmes et à certains langages de spécification. Le système HOL a aussi été utilisé dans les domaines de la vérification matérielle [Kropf 99] et de la vérification de systèmes distribués [Prasetya 95].
PVS (Prototype Vérification Système) [Owre et al 95] : est développé au SRI (International Computer Science Laboratory) à Palo Alto (USA). Le démonstrateur de théorème PVS a été appliqué à de nombreux problèmes réels tel que la spécification et la modélisation des systèmes de contrôle de vol tolérants aux fautes de la navette spatiale [Crow et Vito 96]. La majorité des travaux de preuve se font au niveau de la spécification. Ces travaux peuvent concerner les propriétés temporelles comme les travaux de Dutertre qui portent sur la preuve en PVS du PCP (Priority Ceiling Protocol) [Dutertre 00]. Il s’est intéressé aux propriétés de synchronisation et de respect d’échéance de tâche.
B [Abrial 96] : est une méthode formelle utilisée avec succès en milieu industriel notamment dans le domaine ferroviaire comme le projet Météor (ligne de métro automatisé) [Behnia et Waeselynck 99]. Elle couvre toutes les étapes de développement du logiciel, de la spécification jusqu’à la génération de code exécutable. L’intérêt principal de la méthode B est dans la possibilité de raffiner une spécification de haut niveau en une spécification suffisamment détaillée pour pouvoir être automatiquement traduite dans un langage de programmation.
Les démonstrateurs de théorème AUTOMATH [De Bruijn 68], COQ [Barras et al 99] et le prover ISABELLE [Paulson 94] sont également utilisés avec succès en milieu industriel notamment au niveau de la vérification de programme.
Limites de la preuve
La vérification par preuve est difficile à utiliser et à automatiser. Particulièrement, en méthode B, la vérification des contraintes dynamiques d’un système est effectuée par une technique de preuve, ce qui requiert que l’utilisateur, en plus d’être un expert en spécification, soit également un expert dans l’utilisation de cette technique. En effet la vérification des contraintes dynamiques est confiée à un outil informatique de démonstration de théorèmes, mais dès que cet outil n’arrive plus à progresser seul vers la solution, il fait appel à l’utilisateur pour continuer à avancer. En pratique, la vérification par preuve de contraintes dynamiques est rarement obtenue de manière automatique. De plus, le démonstrateur de théorème est confronté d’une part à la vérification de la correction partielle d’une propriété, et d’autre part à une vérification de terminaison pour certains schémas de contrainte dynamique.
Une autre façon d’attaquer le problème de vérification par preuve (formelle) des propriétés de haut niveau est de décomposer ces dernières en des propriétés de bas niveau (locales) et de les vérifier séparément. Mis à part le problème de faisabilité d’une telle décomposition, des hypothèses implicites sur l’environnement peuvent être rajoutées sans pour autant être satisfaites en vie opérationnelle.
Pour les systèmes de contrôle/commande, une modélisation détaillée de ces derniers, reproduisant les interactions entre le programme de contrôle et l’environnement physique, en prenant en compte les lois physiques du procédé contrôlé, les dispositifs matériels pour assurer ce contrôle et les occurrences possibles de fautes pouvant affecter ces dispositifs, est généralement infaisable. L’utilisation des approches formelles pour la vérification des propriétés de haut niveau s’avère insuffisante. En effet, deux cas d’école, très utilisés par les approches formelles, ont montré leurs limites : la cellule de production [Lewerentz et Lindner 95] et la chaudière à vapeur [Abrial 96]. Ces deux études de cas ont servi d’illustration et de comparaison de plusieurs méthodes de spécification et de vérification formelles. Sur ces deux études de cas, certaines propriétés ont été prouvées par des approches formelles et ont pu être violées au cours de test sur simulateur de l’environnement physique en exécutant un code conforme à sa spécification [Waeselynck et Fosse 99], [AtelierB]. Ceci est dû au fait que la vérification formelle est effectuée sur un modèle du logiciel en formulant des hypothèses sur l’environnement qui ne sont pas nécessairement satisfaites en réalité.
Les outils de preuve actuels ne sont pas orientés vers une description simple et une preuve directe de la dynamique discrète de systèmes complexes. Ils cherchent à traiter simultanément les données et la structure de contrôle et ne sont donc pas adaptés à l’analyse des relations de cause à effet d’un système modélisé sous la forme d’un réseau de Petri ou d’un ensemble d’automates communicants. Les travaux de [Rivière 03], et de [Khalfaoui 03] que nous allons présenter brièvement dans la suite de ce chapitre peuvent être vus comme une réponse à ce manque. En s’appuyant sur une logique non classique (la logique linéaire) ils ont construit une démarche de preuve [Rivière 03] qui à travers l’analyse des relations de cause à effet permet d’élaborer des scénarios menant à des situations critiques [Khalfaoui 03]. Avant d’aborder ce point nous allons présenter un tour d’horizon des techniques de preuve qui se posent en alternative pragmatique lorsque vérification et preuve sont en échec.
Le test
Le test se pose effectivement en alternative pragmatique de la vérification et de la panne, pourvu que l’environnement de test reproduise le plus fidèlement possible l’environnement opérationnel. En pratique, le programme de contrôle sera exécuté sur matériel cible en connexion avec un simulateur de l’environnement physique, offrant des possibilités d’injection de fautes, si la propriété ciblée doit être vérifiée en présence de telles fautes.
Le test est une technique de vérification dynamique qui consiste à exécuter un programme en lui fournissant des entrées valuées, appelées les entrées de test, et à vérifier la conformité des sorties par rapport au comportement attendu pour déterminer leur correction s’il y a lieu [Laprie et al 95]. Sa mise en œuvre nécessite de résoudre deux problèmes :
Le problème de la sélection d’entrées de test.
Le problème de l’oracle [Weyuker 82] ou comment décider de l’exactitude des résultats observés, fournis par le programme en réponse aux entrées de test.
Sauf cas exceptionnel, le test exhaustif d’un programme sur toutes les entrées possibles n’est pas praticable. Le testeur est donc amené à sélectionner de manière pertinente un petit sous-ensemble du domaine d’entrée. Cette sélection s’effectue à l’aide de critères de test, qui peuvent être liés à un modèle de la structure du programme : on parle alors de test structurel, ou à un modèle des fonctions que doit réaliser le programme : on parle alors de test fonctionnel.
Quel que soit le critère de sélection, la génération des entrées peut être déterministe ou probabiliste. Le premier cas définit le test déterministe où les entrées sont déterminées par un choix sélectif de manière à satisfaire le critère de test retenu. Le deuxième cas définit le test statistique où les entrées sont générées de manière aléatoire selon une distribution probabiliste sur le domaine d’entrées, la distribution et le nombre des données de test étant déterminés à partir du critère retenu [Waeselynk 93].
Les solutions les plus satisfaisantes pour le problème d’oracle sont basées sur l’existence d’une spécification formelle du programme sous test. La spécification est alors utilisée pour déterminer les résultats attendus, soit lors de la sélection des entrées de test, soit à posteriori.
Le test orienté Propriété utilise la spécification de la propriété pour guider le processus de test [Fink et Bishop 97]. L’objectif est de valider le programme par rapport à une propriété cible en l’exécutant et en observant si cette propriété est violée ou pas. Etant donné que l’accent est mis sur la propriété et non pas sur la spécification entière, l’oracle se limite ainsi à la vérification du respect de la propriété, ce qui rapproche ce type de test des techniques de vérification.
Couplage de techniques de vérification
Le couplage entre les quatre grandes classes de techniques de vérification (analyse statique, model-checking, preuve de systèmes complexes et test) présentées précédemment est possible. Plusieurs travaux de recherche exploitent leur complémentarité pour résoudre le problème de la vérification. Les couplages les plus étudiés se situent autour du model-checking.
Couplage autour du model-checking : Un exemple réussi de couplage est l’intégration de techniques de model-checking dans l’environnement de preuve PVS [Rushby 99]. Le principe de l’approche est d’utiliser une interaction étroite entre la preuve de théorèmes, et la génération d’abstractions pour le model-checking. Chaque étape consiste à appliquer alternativement l’une des deux techniques (preuve ou model-checking), en exploitant les informations obtenues lors des étapes précédentes. La preuve est utilisée pour justifier les abstractions réalisées pour le model-cheking. Le model-checking aide à trouver les invariants à intégrer dans la preuve. A la fin de ce processus itératif, il donne un contre-exemple indiquant comment la propriété est violée, ou une preuve que cette propriété est satisfaite.
Besoin de scénarios : Lorsque l’on associe de la vérification ou de la preuve au test, cela veut dire que l’on a un modèle, soit des spécifications du système, soit de sa conception. La vérification ou la preuve peut permettre de déterminer des comportements dangereux du système final, susceptibles de violer une propriété qui doit être vérifiée. Lorsque l’on s’intéresse plus particulièrement à l’aspect discret du comportement, on va être amené à s’exprimer sous la forme de séquences d’événements. Face à l’explosion combinatoire des séquences induites par le parallélisme, on ressent le besoin de se fonder sur des ordres partiels pour décrire de façon compacte un grand nombre de séquences. Mais dans le domaine du test, tout comme dans celui de la vérification ou de la preuve, cette notion n’est prise en compte que de façon ponctuelle, l’outil de base restant la notion de séquence.
Avant de détailler notre travail, nous allons présenter rapidement un certain nombre de travaux qui comme nous s’intéressent à la sûreté de fonctionnement et la vérification des systèmes pilotés par calculateurs et qui d’une façon ou d’une autre se sont focalisés sur l’aspect discret du comportement dynamique.
|
Table des matières
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
