Brevet FR3024567A1 — publié le 20160205

Procédé de détermination automatique de causes de dysfonctionnement d'un système composé d'une pluralité de composants matériels ou logiciels La présente invention concerne un procédé de détermination automatique de causes de dysfonctionnement d'un système composé d'une pluralité de composants matériels ou logiciels et un dispositif associé. L'invention se situe dans le domaine de l'analyse des dysfonctionnements des systèmes comportant plusieurs composants logiciels ou matériels, ou combinant composants logiciels et matériels, qui interagissent. Diverses applications utilisent des composants matériels et/ou logiciels interconnectés, répartis sur plusieurs sous-systèmes, et éventuellement embarqués. Par exemple, dans le domaine des appareils médicaux, des systèmes de traitement sont composés d'appareils interconnectés, par exemple les pacemakers ou les perfuseurs connectés à des systèmes de surveillance. Dans le domaine du transport, de nombreux systèmes de contrôle et de surveillance mettent en oeuvre des composants interconnectés, comme par exemple les régulateurs de vitesse. Dans de tels systèmes complexes, il est important, en cas de dysfonctionnement du système, d'identifier automatiquement la cause du dysfonctionnement, c'est-à-dire le ou les composants du système responsables du dysfonctionnement, afin de prendre des mesures adéquates, par exemple pour rétablir la sécurité d'utilisation du système, pour identifier les composants à rappeler en usine ou pour déterminer les responsabilités des parties impliquées. En effet, dans certains systèmes comme les systèmes médicaux ou de contrôle et de surveillance de véhicule, un dysfonctionnement peut avoir de graves conséquences et il est utile d'en déterminer la cause automatiquement. Dans les systèmes distribués et complexes, comprenant plusieurs composants matériels et logiciels, il arrive fréquemment, en cas de dysfonctionnement du système, de constater le dysfonctionnement de plusieurs composants. Dans ce cas, la détermination du ou des composants qui sont effectivement la cause du dysfonctionnement est d'autant plus difficile. L'article "A general trace-based framework of logical causality" de G. Gôssler et D. Le Métayer, publié dans FACS- 10th International Symposium on Format aspects of Component Software, 2013, présente une méthode de détermination de causalité de dysfonctionnement des composants d'un système. Cette méthode nécessite le calcul de cônes d'influence entre évènements observés, et utilise un graphe d'exécution pour la mise en oeuvre. Elle est complexe d'un point de vue calculatoire et implique une sur-estimation de l'influence des défaillances de certains composants sur l'ensemble du système. De plus, cette méthode n'est pas adaptée au cas de l'analyse des causes de dysfonctionnement d'un système temps-réel. Afin de remédier aux inconvénients des méthodes existantes, l'invention propose, selon un premier aspect, un procédé de détermination automatique de causalité nécessaire ou suffisante de dysfonctionnement d'un système composé d'une pluralité de composants matériels ou logiciels, chaque composant ayant une spécification de bon fonctionnement associée, ledit dysfonctionnement étant observé sous la forme de la violation d'une propriété globale du système pendant une exécution dudit système. Le procédé est mis en oeuvre par un processeur ou un circuit programmable et caractérisé en ce qu'il comporte les étapes de : - pour chacun des composants du système, obtention d'une trace d'exécution comportant une séquence d'évènements observés pendant l'exécution du système ; -obtention d'un sous-ensemble de composants testé comprenant au moins un composant dont la trace d'exécution présente au moins une non-conformité avec la spécification de bon fonctionnement dudit composant, et d'un sous-ensemble de composants traité en fonction dudit sous-ensemble de composants testé ; - pour un sous-ensemble de composants traité, obtention d'un ensemble de préfixes de traces d'exécution, chaque dit préfixe comportant des évènements conformes à la spécification de bon fonctionnement du composant associé ; - calcul, pour chacun des composants du système, d'un préfixe de trace d'exécution non affecté par des évènements non-conformes à la spécification observés pour les composants du sous-ensemble de composants traité ; - détermination d'un modèle d'exécution, dit modèle contrefactuel du sous-ensemble traité, permettant de générer l'ensemble des comportements possibles, commençant par les préfixes non affectés, en l'absence de dysfonctionnement des composants du sous-ensemble de composants traité ; - détermination de la causalité nécessaire ou suffisante des composants du sous-ensemble de composants testé pour le dysfonctionnement du système en fonction de la vérification du respect de ladite propriété globale du système par ledit modèle contrefactuel du sous-ensemble de composants traité. Avantageusement, le procédé de l'invention permet de déterminer un ou plusieurs composants dont le dysfonctionnement est nécessaire ou suffisant pour provoquer un dysfonctionnement du système dans un système de composants pour lesquels une spécification de bon fonctionnement est connue, grâce à la génération d'un modèle contrefactuel, calculé à partir de traces d'exécution observées et apte à générer des traces d'exécution conformes aux spécifications de bon fonctionnement des composants. Le procédé selon l'invention peut présenter une ou plusieurs des caractéristiques ci-dessous. L'étape de calcul, pour chacun des composants du système, d'un préfixe de trace d'exécution non affecté par des évènements non-conformes à la spécification observés pour les composants du sous-ensemble de composants traité comporte : - une étape de calcul, pour chacun des composants du système, d'un modèle d'extension permettant de générer ledit préfixe de trace d'exécution, et - une étape de composition des modèles d'extension calculés. Le calcul d'un modèle d'extension, pour un composant donné, permettant de générer un préfixe de trace d'exécution comporte, pour un dit préfixe de trace d'exécution comportant un nombre k d'éléments, la génération d'un modèle générateur permettant de générer les k-1 premiers éléments dudit préfixe de trace d'exécution et la combinaison dudit modèle générateur avec un modèle conforme à la spécification de bon fonctionnement dudit composant. L'étape de calcul comporte en outre une étape de composition des modèles d'extension calculés. Le calcul d'un préfixe de trace d'exécution non affecté par des évènements non- conformes à la spécification, observés pour les composants du sous-ensemble de composants traité, utilise un résultat de la composition des modèles d'extension calculés. La spécification de bon fonctionnement de chaque composant est modélisée sous la forme d'un modèle d'automate à états finis, les états du modèle étant liés par des transitions, lesdites transitions étant définies à partir de ladite spécification de bon fonctionnement. Les modèles d'extension et ledit modèle contrefactuel sont modélisés sous la forme d'automates à états finis. Pour déterminer la causalité nécessaire dudit sous-ensemble de composants testé, ledit sous-ensemble de composants traité est égal au sous-ensemble de composants testé et à l'étape de détermination de causalité, le sous-ensemble de composants testé est déterminé comme cause nécessaire de dysfonctionnement du système si et seulement si le modèle contrefactuel déterminé respecte ladite propriété globale du système. Pour déterminer la causalité suffisante dudit sous-ensemble de composants testé, ledit sous-ensemble de composants traité est égal au sous-ensemble de composants complémentaire audit sous-ensemble de composants testé, et à l'étape de détermination de causalité, le sous-ensemble de composants testé est déterminé comme cause suffisante de dysfonctionnement du système si et seulement si le modèle contrefactuel déterminé viole inévitablement ladite propriété globale du système. Le procédé selon l'invention s'applique notamment lorsque le système comporte des composants matériels et/ou des composants logiciels. Selon un autre aspect, l'invention concerne un dispositif de détermination automatique de causalité nécessaire ou suffisante de dysfonctionnement d'un système composé d'une pluralité de composants matériels ou logiciels, chaque composant ayant une spécification de bon fonctionnement associée, ledit dysfonctionnement étant observé sous la forme de la violation d'une propriété globale du système pendant une exécution dudit système, comportant un processeur ou un circuit programmable. Le dispositif comporte des unités adaptées pour : - pour chacun des composants du système, obtenir une trace d'exécution comportant une séquence d'évènements observés pendant l'exécution du système ; - obtenir un sous-ensemble de composants testé comprenant au moins un composant dont la trace d'exécution présente au moins une non-conformité avec la spécification de bon fonctionnement dudit composant, et un sous-ensemble de composants traité en fonction dudit sous-ensemble de composants testé ; - pour un sous-ensemble de composants traité, obtenir un ensemble de préfixes de traces d'exécution, chaque dit préfixe comportant des évènements conformes à la spécification de bon fonctionnement du composant associé ; - calculer, pour chacun des composants du système, un préfixe de trace d'exécution non affecté par des évènements non-conformes à la spécification observés pour les composants du sous-ensemble de composants traité ; - déterminer un modèle d'exécution, dit modèle contrefactuel du sous-ensemble traité, permettant de générer l'ensemble des comportements possibles, commençant par les préfixes non affectés, en l'absence des dysfonctionnements des composants du sous-ensemble de composants traité ; - déterminer la causalité nécessaire ou suffisante des composants du sous-ensemble de composants testé pour le dysfonctionnement du système en fonction de la vérification du respect de ladite propriété globale du système par ledit modèle contrefactuel du sous-ensemble de composants traité. Selon un autre aspect, l'invention concerne un programme d'ordinateur comportant des instructions pour mettre en oeuvre les étapes d'un procédé de détermination automatique de causalité nécessaire ou suffisante de dysfonctionnement d'un système composé d'une pluralité de composants matériels ou logiciels tel que brièvement présenté ci-dessus lors de l'exécution du programme par un processeur ou un circuit programmable d'un dispositif programmable. Selon un autre aspect, l'invention concerne un support d'enregistrement d'informations, caractérisé en ce qu'il comporte des instructions pour l'exécution d'un procédé de détermination automatique de causalité nécessaire ou suffisante de dysfonctionnement d'un système composé d'une pluralité de composants matériels ou logiciels tel que présenté ci-dessus, lorsque ces instructions sont exécutées par un dispositif programmable. D'autres caractéristiques et avantages de l'invention ressortiront de la description qui en est donnée ci-dessous, à titre indicatif et nullement limitatif, en référence aux figures annexées, parmi lesquelles : - la figure 1 est un exemple de système mettant en oeuvre l'invention ; - la figure 2 est un organigramme d'un procédé de détermination de causalité nécessaire et/ou suffisante de dysfonctionnement selon un mode de réalisation de l'invention ; - les figures 3, 4 et 5 illustrent schématiquement des modèles de représentation de composants selon un exemple de mise en oeuvre ; - la figure 6 représente un exemple de trace d'exécution d'un système comportant des composants modélisés selon les modèles des figures 3 à 5 ; - la figure 7 est un organigramme d'un procédé de détermination de causalité nécessaire selon un mode de réalisation de l'invention ; - la figure 8 représente un ensemble de traces d'exécution tronquées ; - la figure 9 représente une pluralité de modèles d'extension calculés à partir des traces d'exécution tronquées de la figure 8 ; - la figure 10 représente un ensemble de préfixes d'exécution non affectés calculés en appliquant les modèles d'extension de la figure 8 ; - la figure 11 illustre schématiquement un modèle contrefactuel calculé ; - la figure 12 est un organigramme d'un procédé de détermination de causalité suffisante selon un mode de réalisation de l'invention. L'invention sera décrite ci-après dans le cas général d'un système à multiples composants, qui sera illustré par un cas schématique de système de surveillance industrielle. Il est entendu que l'invention ne se limite pas à cet exemple d'application et peut s'appliquer à tout type de système à base de composants aptes à communiquer entre eux selon un modèle de communication donné. L'invention trouve des applications notamment dans les systèmes d'appareils médicaux intégrant des composants logiciels, dans les systèmes embarqués dans des véhicules ou des trains, dans l'aéronautique et l'aérospatiale, dans les centrales électriques, dans les réseaux de distribution d'énergie et dans les services web. L'invention peut être appliquée pendant ou après l'exécution d'un système. Elle peut aussi être appliquée au moment de la validation d'un système ; dans ce cas elle permet d'identifier les composants qui ont causé les dysfonctionnements observés lors de tests. Dans une application particulière, l'invention peut être appliquée en cours d'exécution d'un système lorsqu'un dysfonctionnement est observé, permettant ainsi une identification du ou des composants ayant causé le dysfonctionnement. La figure 1 illustre un système 1 mettant en oeuvre l'invention, comportant un système de communication 2 à trois composants 4, 6, 8, qui sont aptes à communiquer entre eux par des messages de communication, représentés par des flèches sur la figure. Le nombre de composants est limité à trois dans la figure 1 pour faciliter l'explication, mais en pratique, l'invention permet de traiter un nombre quelconque de composants. De plus, bien que les composants 4, 6 et 8 illustrés à la figure 1 soient tous connectés les uns aux autres par des connexions émission/réception, une telle architecture n'est pas nécessaire, les composants pouvant être seulement partiellement connectés entre eux. Pour chacun des composants, une séquence d'évènements est mémorisée dans un journal d'exécution stocké dans un fichier respectif 10, 12, 14. Dans l'exemple de la figure 1, chaque composant a un journal d'exécution associé, mémorisé séparément. En variante, un seul journal d'exécution est mémorisé pour l'ensemble ou un sous-ensemble des composants du système 2. Les composants sont considérés comme des « boîtes noires », dont seules les entrées et les sorties sont connues, ainsi qu'une spécification de bon fonctionnement, et ce sont ces informations qui sont utiles pour la détermination de causalité de dysfonctionnement. Ainsi, l'invention s'applique de manière générique à tout type de composants qui interagissent, chacun ayant une spécification de bon fonctionnement associée. Les évènements et données mémorisés dans les journaux d'exécution portent par exemple sur les communications, c'est-à-dire les messages envoyés et reçus, sur des appels de fonctions, sur l'écriture et la lecture de variables partagées, et/ou sur un résumé de pas de calcul internes comme par exemple les fonctions exécutées avec les valeurs des paramètres et les valeurs de retour. Les journaux d'exécution mémorisés, comportant les séquences d'évènements observés pour chaque composant, sont ensuite utilisés dans un dispositif 16 de détermination automatique de causes de dysfonctionnement. Le dispositif 16 met en oeuvre un procédé de détermination de causalité nécessaire et/ou suffisante selon l'invention, et indique en sortie 18 un ou plusieurs composants défaillants parmi tous les composants du système. Le dispositif 16 est un dispositif programmable et comporte notamment un processeur ou un circuit programmable apte à mettre en oeuvre des modules de détermination automatique de causes de dysfonctionnement nécessaire et/ou suffisante du système analysé. La figure 2 illustre un mode de réalisation d'un procédé de détermination de causalité nécessaire et/ou suffisante de dysfonctionnement d'un système selon l'invention, dans le cas où un dysfonctionnement est observé, en cours d'exécution du système ou après exécution du système. Le procédé est mis en oeuvre par un dispositif programmable tel un ordinateur, comportant notamment un circuit programmable ou un processeur apte à exécuter des instructions de programme de commande lorsque le dispositif est mis sous tension et des moyens de stockage d'informations, aptes à stocker des instructions de code exécutable permettant la mise en oeuvre de programmes aptes à mettre en oeuvre le procédé selon l'invention. Pour un système S comportant une pluralité de n composants d'indices i, i E {1,...,n}, dans une étape préliminaire 20 de caractérisation du système, des spécifications du système sont obtenues et mémorisées. En effet, le procédé de détermination de causes de dysfonctionnement selon l'invention utilise une formalisation mathématique du comportement d'un système, permettant ainsi une application à tout type de système à composants matériels ou logiciels. L'invention s'applique à tout modèle de comportement de système, mais sera décrite ci-après dans un mode de réalisation, dans lequel le comportement d'un tel système et de ses composants est modélisé par un système de transitions étiquetées (labeled transition system, LTS). Il existe des outils informatiques pour effectuer automatiquement les opérations décrites ci-dessous sur les LTS. Un LTS B = (Q,E,,q0) consiste en un ensemble d'états Q, un alphabet d'évènements E, une relation de transition notée où QxExQ et go un état initial. On écrit q q' pour le triplet (q, a, q') qui représente une transition étiquetée par l'évènement a entre un premier état q et un deuxième état q' . Pour un système S comportant une pluralité de composants, la spécification de bon fonctionnement de chaque composant i est donnée par un LTS C, , , q(,) ) . Le modèle de bon fonctionnement du système S est obtenu par une composition des modèles des composants du système. La composition de modèles est notée 11 . On note : C = 11C2...K = (Q1 x Q2 x , Et ,---, q'°)) Où les transitions sont définies comme suit : )) a Vi n: (a E Ei A iq;) y (a e Ei A qi = En d'autres termes, l'alphabet de la composition des modèles C, est l'union des alphabets des modèles ; C peut effectuer une transition étiquetée par a si et seulement si tous les modèles qui ont a dans leur alphabet sont prêts à faire une transition a dans leur état actuel. Soit P une propriété globale de bon fonctionnement du système S, dont la violation constitue un dysfonctionnement, telle que si tous les composants de S satisfont leur spécification, alors P est respectée. Afin de faciliter l'explication, considérons l'exemple d'un système comprenant trois composants : une usine Plant utilisant un réacteur dont la température doit être maintenue à un certain niveau ; un composant de supervision Supervisor qui mesure la température et qui active soit un chauffage soit un refroidissement ; un composant Env qui modélise l'évolution de la température en fonction des actions du composant de supervision. Le système S est donc formé de trois composants qui sont respectivement le composant de supervision Supervisor, l'usine à réacteur Plant et le composant d'environnement Env. Les figures 3, 4 et 5 illustrent schématiquement, pour l'exemple traité, les spécifications de bon fonctionnement des composants Supervisor, Plant et un modèle d'environnement Env incluant un état indiquant une violation de propriété de bon fonctionnement, noté 1. Le modèle de fonctionnement du composant Supervisor est illustré à la figure 3. Le composant Supervisor interagit avec le composant Env pour recueillir la température courante du réacteur dans l'état Q. . Si la température est comprise entre des seuils prédéfinis Tmin, Tmax, notée med pour température médium, le composant Supervisor effectue une transition med vers un état Qs2, attend une durée de temporisation (transition t), et retourne dans l'état Qs1 ; aucune action auprès du composant Plant n'est requise. Si la température captée est inférieure au seuil minimal de bon fonctionnement, le composant Supervisor effectue une transition low vers l'état Qs3 , suivie d'une transition heat vers l'état Q. Si la température captée est supérieure au seuil maximal de bon fonctionnement, le composant Supervisor effectue une transition high vers l'état Qs4 , suivie d'une transition cool vers l'état Q. Depuis l'état Qs2 la transition t effectue la temporisation et le retour à l'état Qs1 de réception de température captée. Le modèle associé au composant Plant est illustré à la figure 4, et montre les états et les transitions autorisés selon la spécification de bon fonctionnement de ce composant. Le composant Plant est, dans un premier état VE, dans un mode où la température du réacteur augmente. Le composant Plant effectue une transition t vers l'état Qp2 d'où une transition inc, représentant une augmentation de température, permet de repasser au premier état VE. Dans le cas d'une commande cool reçue du composant Supervisor, le composant Plant effectue une transition vers l'état Q. . Dans l'état QI,' , une transition t mène vers l'état Qp4, d'où une transition dec permet de repasser à l'état Q; ; ceci modélise une diminution de la température du réacteur à chaque unité de temps. De l'état QE3 , l'état Q. peut être atteint par une commande heat reçue du composant Supervisor. Le modèle du composant Env , équipé d'un état noté 1 qui modélise une violation de fonctionnement correct, notée 1 est illustré à la figure 5. Le composant Env a six états de bon fonctionnement associés, notés VE, QE2 , Q3E , Q5E QE Les états VE et Qp4 sont associés à une température captée Temp fournie par des capteurs. Si la température Temp est dans l'intervalle de bon fonctionnement [Tmin, 'maxi, l'état QE1 est maintenu par une séquence de transitions med (transmission de la température captée au Supervisor) suivie de t. Dans le cas où la température diminue, le composant passe à l'état QE2 par une transition dec. Tant que la température captée est inférieure à Tmin, le composant reste dans les états QE2 et QE5 (transitions /ow t). Si la température augmente, une transition inc vers l'état QE1 est appliquée. Dans le cas où la température captée à l'état QE1 augmente, le composant passe de l'état QE1 à l'état QE3 par une transition inc. Tant que la température captée est supérieure à Tm', le composant reste dans les états QE3 et QE6 (transitions high ; t). Si la température baisse, une transition dec de l'état QE3 vers l'état QE1 est appliquée. Si la température diminue davantage (transition dec) dans l'état QE2 ou si la température augmente davantage (transition inc) dans l'état QE3 , alors le système est en violation d'une propriété de bon fonctionnement et l'état noté 1 est atteint. De retour à la figure 2, après l'étape de mémorisation préliminaire 20 de caractérisation du système, une exécution du système fournissant un journal d'exécution comprenant un ensemble de traces tr1 pour chacun des composants du système est appliquée. En effet, lors d'une exécution du système, chaque composant a un journal d'exécution associé, appelé également trace du composant et noté tr1. Le journal d'exécution comporte une séquence d'évènements observés, chaque évènement correspondant à une transition entre états du composant comme défini ci-dessus. On appelle, pour chaque composant, une première portion de la trace du composant un préfixe de ladite trace. On note qu'un préfixe d'une trace d'exécution est une troncature de la trace. Dans le mode de réalisation utilisant un modèle LTS, pour une définition formelle, considérant un système LTS B = (Q,E, qo ) , une trace d'exécution : tr a2....ak est une séquence d'évènements. Elle est acceptée par B s'il existe une séquence de transitions faisant passer B d'un état initial q à un état q' tel a2 ak que : qk-1.7' les états a E Selon un mode de réalisation, les journaux d'exécution ou traces tr, sont mémorisés au fil d'une exécution du système et sont lus dans une mémoire du dispositif programmable mettant en oeuvre l'invention. Selon une variante, les journaux d'exécution ou traces tr, sont utilisés en cours d'exécution du système. Lorsque l'analyse de causalité est effectuée en cours d'exécution, les séquences d'évènements qui se sont produits jusqu'au moment de l'analyse sont utilisées. Dans ce mode de réalisation, des journaux d'exécution tr, séparés sont obtenus pour chacun des composants. Selon une variante possible, les traces d'exécution tr, sont enregistrées dans un même fichier pour tous les composants ou pour des groupes de composants. Dans ce cas, l'étape 22 comprend l'extraction des journaux d'exécution tr, par composant à partir d'un ou plusieurs tels fichiers enregistrant des séquences d'évènements pour plusieurs composants. Le procédé de l'invention est utilisé lorsqu'une exécution du système est incorrecte, ou, en d'autres termes, lorsque pour l'exécution du système se produit un dysfonctionnement, qui est une non-conformité au niveau d'une ou plusieurs des propriétés globales du système P. Un exemple de journal d'exécution du système S pris en exemple, dont les modèles des composants sont illustrés aux figures 3, 4 et 5, est illustré à la figure 6. Un tableau T illustre des traces d'exécution respectives des composants Supervisor, Plant, Env, notées tr S, tr P, et tr E. Dans cet exemple, la trace d'exécution tr S du composant Supervisor comporte un évènement qui n'est pas conforme au modèle illustré à la figure 3 : il s'agit de l'évènement t entouré dans le tableau T. En effet, d'après le modèle de la figure 3, un évènement high devrait être suivi d'un évènement cool et non d'une temporisation t. De même, la trace d'exécution tr P du composant Plant comporte un évènement qui n'est pas conforme au modèle illustré à la figure 4 : il s'agit de l'évènement t entouré dans le tableau T. En effet, d'après le modèle de la figure 4, il n'est pas possible de rencontrer deux transitions t successives. Ainsi, le système S présente un dysfonctionnement et une violation de la spécification, puisque pour le composant Env, la transition high est suivie de inc, ce qui est contraire à la propriété globale de bon fonctionnement (voir figure 5). De retour à la figure 2 , l'étape 22 d'obtention de traces d'exécution est suivie d'une étape 24 de détection de dysfonctionnement, c'est-à-dire de non-conformité avec une propriété globale P du système, qui s'applique quelle que soit la modélisation du comportement du système. En cas de détection de dysfonctionnement à l'étape 24, cette étape est suivie d'une étape 26 de sélection d'un sous-ensemble I de composants, comportant chacun une trace d'exécution comportant un évènement non conforme au modèle. Le sous-ensemble I comporte R indices, 1, et N, N étant le nombre total de composants du système S observé. Le sous-ensemble / de composants est le sous-ensemble dont la causalité nécessaire et/ou suffisante vis-à-vis du dysfonctionnement observé est testée, et est appelé sous-ensemble de composants testé. Le procédé analyse la causalité jointe des composants du sous-ensemble / testé. Il est à noter que la méthode de l'invention est applicable théoriquement avec un sous-ensemble / de composants ne comportant pas de non-conformité dans la trace d'exécution, mais un tel cas est sans intérêt en pratique. En effet, la méthode a pour objectif de déterminer lequel ou lesquels des composants du système étudié est la cause du dysfonctionnement observé. Ensuite, les étapes 28 de détermination de causalité nécessaire des composants du sous-ensemble / et 30 de détermination de causalité suffisante des composants du sous-ensemble / sont mises en oeuvre. Ces étapes peuvent être mises en oeuvre sensiblement simultanément ou séquentiellement. En variante, seule l'une des étapes de détermination de causalité nécessaire 28 ou de détermination de causalité suffisante 30 est mise en oeuvre pour un sous-ensemble de composants / testé. Ainsi, l'invention permet de déterminer, en testant plusieurs sous-ensembles de composants /, de manière précise, les composants dont le dysfonctionnement est nécessaire et/ou suffisant pour constater le dysfonctionnement global du système par rapport à la propriété P. La figure 7 illustre un mode de réalisation de l'étape de détermination de causalité nécessaire du sous-ensemble / de composants. Le procédé illustré schématiquement à la figure 7 est mis en oeuvre par un dispositif programmable tel un ordinateur, comportant notamment un circuit programmable ou un processeur apte à exécuter des instructions de programme de commande lorsque le dispositif est mis sous tension et des moyens de stockage d'informations, aptes à stocker des instructions de code exécutable permettant la mise en oeuvre de programmes aptes à mettre en oeuvre le procédé selon l'invention. Lors d'une première étape 32, considérant le sous-ensemble de composants /, un journal d'exécution tronqué est obtenu. Il est à noter que pour la détermination de la causalité nécessaire du sous- ensemble de composants testé, les étapes 32 à 40 s'appliquent à ce sous-ensemble de composants, comme expliqué ci-dessous. Pour chaque composant d'indice ik E /, la trace d'exécution tri, est tronquée pour n'en retenir que le préfixe tri, conforme au modèle du composant Cik. En pratique, le préfixe tri,' comprend la séquence d'évènements de tri, qui précède l'évènement non conforme au modèle détecté, appelé également erreur par rapport à l'exécution du composant considéré. Pour chaque composant d'indice i1 e Ic, où Ic est le sous-ensemble d'indices complémentaire de sous-ensemble /, les traces d'exécution sont inchangées : tr, =t La figure 8 illustre le journal d'exécution tronqué, représenté dans un tableau T', pour l'exemple développé et pour le sous-ensemble / comprenant le composant Supervisor. Comme on le voit sur la figure 8, le préfixe tr' _S ne comporte que les trois premiers éléments de la trace d'exécution tr _S pour le composant Supervisor, et les traces/préfixes tr` _P et tr' _E sont inchangés pour les deux autres composants. Ensuite, lors d'une étape 34 d'obtention de modèles d'extension, pour chacun des préfixes tr', du journal d'exécution tronqué, on détermine un modèle d'extension, permettant de générer l'ensemble des traces d'exécution comportant le préfixe tr', et conformes au modèle du composant Ci. Dans le mode de réalisation utilisant un modèle LTS, pour une trace tr = a, a2....ak , on note T(tr) un modèle LTS permettant de générer exactement la trace tr , appelé modèle générateur de tr . Le modèle générateur T(tr) est défini comme suit : T(tr) = Un modèle d'extension, noté M(tr), d'une trace tr = a, a2 ....ak conforme au modèle LTS B = (Q,E,,q0) est défini à partir du modèle générateur du préfixe tr' = al. a2....ak_i et du modèle B . On note T(tr') = (Q' ) . On note le modèle d'extension de la trace tr = ai - a2....ak Refine B(tr)=(Q",E, ) , avec : Q" Q' et {"=u 'LJ (qk-i,c1k,q) Le modèle d'extension de la trace tr = ai - a2....- ak_i - ak est obtenu par composition du modèle générateur T(trp) du préfixe trp de la trace tr , correspondant à la trace tr sans son dernier évènement ak et de l'ensemble des transitions conformes au modèle B permettant de passer de l'état qk_1 du modèle générateur T(trp) à un état q du modèle B . Si, au contraire, un préfixe trp de la trace tr d'un composant n'est pas conforme à son modèle de bon fonctionnement, alors son modèle d'extension est égal au modèle générateur T(trp). L'obtention du modèle d'extension de trace s'applique quelle que soit la modélisation du comportement du système. Il est à noter que l'obtention d'un modèle d'extension pour une trace tr expliquée ci-dessus est applicable de manière analogue à tout préfixe d'une trace tr , dans la mesure où un préfixe d'une trace est également une trace tronquée, comportant moins d'éléments qu'une trace tr complète. Ainsi, à l'étape 34 de génération de modèles d'extension, un modèle d'extension M t(tri') est obtenu pour chaque préfixe tr; du journal d'exécution tronqué. La figure 9 illustre les modèles d'extension Ms, Mp, ME obtenus à partir des préfixes du journal d'exécution tronqué illustré à la figure 8. Les notations sont analogues aux notations des figures 3, 4, 5 et ne sont pas ré-expliquées en détail ici. Comme illustré à la figure 9, pour les composants respectifs Plant et Env, les modèles d'extension sont en fait les modèles générateurs des traces tr' _P et tr' _E respectives. Pour le composant Supervisor, le modèle d'extension est une combinaison du modèle générateur de la trace tr' S, privé de la dernière transition {high} (on note tr' S\{ high} ), et de la transition high vers le modèle correspondant Cs illustré à la figure 3. tr qo L'étape 34 de génération de modèles d'extension est suivie d'une étape 36 de construction d'un ensemble de préfixes non affectés par l'erreur ou les erreurs des composants du sous-ensemble I , notés {tr*,}. La construction de cet ensemble est réalisée par troncature de tous les préfixes {tri) obtenus à l'étape 32 en fonction de la combinaison des modèles d'extension calculés à l'étape 34. La combinaison des modèles d'extension g(tr;) calculés à l'étape 34 fournit un modèle : M = Mi(tri) M2 ( tr; ) . Mn(tr'n) Deux modes de réalisation sont envisagés pour l'étape 34. Selon un premier mode de réalisation, la troncature est effectuée simultanément : pour chaque i =1,...,n . On obtient tr* comme préfixe le plus long de tr' qui peut être produit par M (tr;) dans la composition : Mi (tri ) Mi-1(tr-i) T (t r) .. .11M (t r ,)1113 Où B est un modèle de comportement du système global. La combinaison avec B est optionnelle. Selon un deuxième mode de réalisation, les composants sont considérés dans un ordre prédéterminé, par exemple l'ordre croissant des indices ; après l'obtention de chaque préfixe non affecté son modèle d'extension est mis à jour dans la composition avant de calculer le préfixe non affecté de la trace suivante. La figure 10 illustre l'ensemble T* de préfixes non affectés {tr*;} obtenu dans l'exemple de réalisation, obtenu en utilisant les modèles d'extension de la figure 9 selon le premier mode de réalisation de l'étape 36 décrit ci-dessus. L'ensemble T* obtenu est l'ensemble des préfixes de longueur maximale que l'on aurait pu observer en l'absence des erreurs d'exécution du système S. De retour à la figure 7, l'étape 36 de construction de l'ensemble de préfixes non affectés est suivie d'une étape 38 de construction d'un modèle MC(/), appelé modèle contrefactuel construit par rapport au sous-ensemble de composants I. Le modèle MC(I) est obtenu par composition des modèles d'extension de chacun des préfixes non affectés {tr;*}, fonction des modèles LTS respectifs de chacun des composants. Pour un composant d'indice i, on note 13,(tr,*) le modèle d'extension correspondant, obtenu comme expliqué ci-dessus à l'étape 34. Le modèle contrefactuel MC(I) est la composition des modèles d'extension 13,(tr,*) avec le modèle B de comportement global du système : MC(I) = Bi (tri* ) B2(tr; )..11B'(tr: )0B En variante, le modèle contrefactuel MC(I) est la composition des modèles d'extension 13,(tr,*) sans modèle B de comportement global du système. Le modèle contrefactuel MC(I) est un modèle des traces d'exécution fictives, qui auraient pu être observées en l'absence d'erreurs des composants du sous-ensemble / considéré. Ainsi, le modèle contrefactuel du sous-ensemble traité permet de générer l'ensemble des comportements possibles commençant par les préfixes non affectés, en l'absence de dysfonctionnements des composants du sous-ensemble de composants traité. Ensuite, lors de l'étape de test du modèle contrefactuel MC(I) il est vérifié si le modèle contrefactuel satisfait la propriété P qui n'a pas été respectée lors de l'exécution du système S. Dans le mode de réalisation utilisant une modélisation LTS, une propriété P est également représentée par un modèle LTS : P = (Qp, 10,1710()) On construit un modèle d'observation de la propriété P, noté 0(P) : 0(P) = (Qp u 111E, P q°P) Avec {'pe =pe U (q, a,1) qeQActeEAVq'eQ:-1(q4 q')} Où la relation de transition est la relation de transition du modèle testé, ici MC(/). En d'autres termes, les transitions du modèle d'observation comportent les transitions définies pour le modèle de la propriété P et les transitions qui, acceptant un évènement qui n'est pas conforme à la propriété testée, aboutissent à un état d'erreur. Le modèle testé MC(/) satisfait la propriété P si et seulement si il n'existe pas d'état qe Qx tel que (q0,qp° ) *q où est la fermeture transitive de En d'autres termes, le modèle contrefactuel MC(/) satisfait la propriété P si aucune séquence d'évènements générés par le modèle n'aboutit à l'état d'erreur 1. En pratique, la satisfaction de la propriété P est vérifiée par un algorithme d'atteignabilité - tel qu'implémenté dans des logiciels de model-checking comme CADP (« Construction and Analysis of Distribution Processes » , disponible en ligne à l'adresse http://cadp.inria.fr/) , NuSMV (logiciel OpenSource disponible en ligne) et Uppaal (logiciel développé par l'Université d'Uppsala, Suède et par l'Université d'Aalborg, Danemark, disponible en ligne) - qui vérifie si l'état 1 est atteignable. En fonction du résultat de l'étape de vérification de la satisfaction de la propriété P par le modèle contrefactuel MC(/), une décision concernant la causalité nécessaire des erreurs de composants du sous-ensemble / est rendue à l'étape 42, quelle que soit la modélisation du système. Si le modèle contrefactuel MC(/) satisfait la propriété P, alors il est décidé que les erreurs des composants du sous-ensemble / sont une cause nécessaire de dysfonctionnement du système S. Si au contraire le modèle contrefactuel MC(/) généré ne satisfait pas la propriété P, alors les erreurs des composants du sous-ensemble / ne sont pas une cause nécessaire de dysfonctionnement du système S. La figure 11 illustre le modèle contrefactuel obtenu pour l'exemple développé, considérant le composant Supervisor comme sous-ensemble de composants testés. Le modèle contrefactuel est obtenu par composition des modèles d'extension. Le modèle contrefactuel obtenu satisfait la propriété P, ce qui permet de déduire que l'erreur constatée dans la trace d'exécution du composant Supervisor est une cause nécessaire du dysfonctionnement du système. La figure 12 illustre un mode de réalisation de l'étape de détermination de causalité suffisante du sous-ensemble / de composants. Le procédé illustré schématiquement à la figure 12 est mis en oeuvre par un dispositif programmable tel un ordinateur, comportant notamment un circuit programmable ou un processeur apte à exécuter des instructions de programme de commande lorsque le dispositif est mis sous tension et des moyens de stockage d'informations, aptes à stocker des instructions de code exécutable permettant la mise en oeuvre de programmes aptes à mettre en oeuvre le procédé selon l'invention. Lors d'une première étape 50 de détermination d'un sous-ensemble complémentaire de composants, un sous-ensemble f comportant les indices des composants du système S et qui ne font pas partie du sous-ensemble / est déterminé. Les étapes suivantes 52, 54, 56, 58 sont analogues aux étapes 32, 34, 36, 38 précédemment décrites, en considérant le sous-ensemble F comme sous-ensemble de composants traité à la place du sous-ensemble /. A l'issue de ces étapes, un modèle contrefactuel MC(f) est obtenu. L'étape de vérification 60 consiste à vérifier si le modèle contrefactuel MC(f) viole systématiquement la propriété P, donc si toutes les traces obtenues conformément à ce modèle comportent un enchaînement d'évènements non conforme à P. Une telle vérification est effectuée par la mise en oeuvre d'un procédé systématique appelé vérification d'inévitabilité - tel qu'implémenté dans des logiciels de model-checking comme CADP, NuSMV et Uppaal - de la violation de P. Si le modèle contrefactuel MC(f) viole inévitablement la propriété P, il est déterminé à l'étape 62 que le sous-ensemble de composants / est une cause suffisante de dysfonctionnement du système. Si au moins certaines des traces qu'on peut obtenir en appliquant le modèle contrefactuel MC(f) satisfont P, alors il est déterminé à l'étape 62 que le sous-ensemble de composants / n'est pas une cause suffisante de dysfonctionnement du système. L'invention a été décrite ci-dessus plus particulièrement dans un mode de réalisation dans lequel le système est modélisé sous forme de LTS. Dans une variante, le comportement du système et de ses composants est modélisé par des automates temporisés. L'invention s'applique plus généralement à toute modélisation d'un système et de ses composants qui permet de construire des outils pour : construire un modèle T(tr) , modèle générateur d'une trace tr ; construire un modèle d'extension de la trace tr, conforme à un modèle B donné ; calculer une composition de modèles C, donnés, C = CIC211...11Cn vérifier si une trace tr peut être produite par un modèle M, et si une trace tr peut être produite par un modèle M composé avec les modèles d'autres composants ; vérifier la satisfaction d'une propriété P donnée par un modèle ; vérifier si un système viole inévitablement une propriété P donnée. Il est à noter que l'invention a été illustrée par un exemple simple, afin d'en faciliter la compréhension. L'invention s'applique néanmoins à des systèmes complexes à composants multiples, et permet de déterminer automatiquement et systématiquement des causes de dysfonctionnement nécessaires et/ou suffisantes dans ces systèmes complexes. Le procédé décrit ci-dessus en référence à la figure 2 a été décrit pour l'analyse d'un sous-ensemble des composants défini par des indices /. De manière générale, le procédé est utilisable dans une recherche systématique de causalité, dans laquelle tous les évènements ou séquences d'évènements susceptibles d'être causes d'un dysfonctionnement parmi les évènements observés sont analysés. Dans cette utilisation, le procédé décrit est mis en oeuvre pour chaque sous- 1 0 ensemble / considéré comme susceptible d'être cause nécessaire et/ou suffisante de dysfonctionnement, ou pour une partie de ces sous-ensembles, et permet de déterminer notamment le sous-ensemble minimal de composants dont le comportement observé est une cause nécessaire et/ou suffisante pour le dysfonctionnement observé. 15 REVENDICATIONS1.- Procédé de détermination automatique de causalité nécessaire ou suffisante de dysfonctionnement d'un système composé d'une pluralité de composants matériels ou logiciels, chaque composant ayant une spécification de bon fonctionnement associée, ledit dysfonctionnement étant observé sous la forme de la violation d'une propriété globale du système pendant une exécution dudit système, le procédé étant mis en oeuvre par un processeur ou un circuit programmable et caractérisé en ce qu'il comporte les étapes de : -pour chacun des composants du système, obtention (22) d'une trace d'exécution comportant une séquence d'évènements observés pendant l'exécution du système ; -obtention (26) d'un sous-ensemble (/) de composants testé comprenant au moins un composant dont la trace d'exécution présente au moins une non-conformité avec la spécification de bon fonctionnement dudit composant, et d'un sous-ensemble de composants traité (/, /c) en fonction dudit sous-ensemble de composants testé ; - pour un sous-ensemble (/) de composants traité, obtention (32, 52) d'un ensemble de préfixes de traces d'exécution, chaque dit préfixe comportant des évènements conformes à la spécification de bon fonctionnement du composant associé ; -calcul (36, 56), pour chacun des composants du système, d'un préfixe de trace d'exécution non affecté par des évènements non-conformes à la spécification observés pour les composants du sous-ensemble de composants traité ; -détermination (38, 58) d'un modèle d'exécution, dit modèle contrefactuel du sous-ensemble traité, permettant de générer l'ensemble des comportements possibles, commençant par les préfixes non affectés, en l'absence de dysfonctionnement des composants du sous-ensemble de composants traité (/) ; -détermination de la causalité nécessaire (28, 40, 42) ou suffisante (30, 60, 62) des composants du sous-ensemble (/) de composants testé pour le dysfonctionnement du système en fonction de la vérification du respect de ladite propriété globale du système par ledit modèle contrefactuel du sous-ensemble de composants traité. 2.- Procédé selon la revendication 1, caractérisé en ce que l'étape de calcul (36, 56), pour chacun des composants du système, d'un préfixe de trace d'exécution non affecté par des évènements non-conformes à la spécification observés pour les composants du sous-ensemble de composants traité comporte : -une étape de calcul (34, 56), pour chacun des composants du système, d'un modèle d'extension permettant de générer ledit préfixe de trace d'exécution, et- une étape de composition des modèles d'extension calculés. 3.- Procédé selon la revendication 2, caractérisé en ce que la spécification de bon fonctionnement de chaque composant est modélisée sous la forme d'un modèle d'automate à états finis, les états du modèle étant liés par des transitions, lesdites transitions étant définies à partir de ladite spécification de bon fonctionnement. 4.- Procédé selon la revendication 3, caractérisé en ce que les modèles d'extension et ledit modèle contrefactuel sont modélisés sous la forme d'automates à états finis. 5.- Procédé selon l'une quelconque des revendications 1 à 4, caractérisé en ce que, pour déterminer la causalité nécessaire(40, 42) dudit sous-ensemble (/) de composants testé, ledit sous-ensemble de composants traité est égal au sous-ensemble (/) de composants testé et en ce qu'à l'étape de détermination de causalité, le sous- ensemble (/) de composants (/) testé est déterminé comme cause nécessaire de dysfonctionnement du système si et seulement si le modèle contrefactuel déterminé respecte ladite propriété globale du système. 6.- Procédé selon l'une quelconque des revendications 1 à 4, caractérisé en ce que, pour déterminer la causalité suffisante (60, 62) dudit sous-ensemble (/) de composants testé, ledit sous-ensemble de composants traité est égal au sous-ensemble (f) de composants complémentaire audit sous-ensemble (/) de composants testé, et en ce qu'à l'étape de détermination de causalité, le sous-ensemble (/) de composants testé est déterminé comme cause suffisante de dysfonctionnement du système si et seulement si le modèle contrefactuel déterminé viole inévitablement ladite propriété globale du système. 7.- Dispositif de détermination automatique de causalité nécessaire ou suffisante de dysfonctionnement d'un système composé d'une pluralité de composants matériels ou logiciels, chaque composant ayant une spécification de bon fonctionnement associée, ledit dysfonctionnement étant observé sous la forme de la violation d'une propriété globale du système pendant une exécution dudit système, comportant un processeur ou un circuit programmable, caractérisé en ce qu'il comporte des unités adaptées pour : -pour chacun des composants du système, obtenir une trace d'exécution comportant une séquence d'évènements observés pendant l'exécution du système ;-obtenir un sous-ensemble de composants testé comprenant au moins un composant dont la trace d'exécution présente au moins une non-conformité avec la spécification de bon fonctionnement dudit composant, et un sous-ensemble de composants traité (/, /c) en fonction dudit sous-ensemble de composants testé ; - pour un sous-ensemble (/) de composants traité, obtenir un ensemble de préfixes de traces d'exécution, chaque dit préfixe comportant des évènements conformes à la spécification de bon fonctionnement du composant associé ; -calculer, pour chacun des composants du système, un préfixe de trace d'exécution non affecté par des évènements non-conformes à la spécification observés pour les composants du sous-ensemble de composants traité ; -déterminer un modèle d'exécution, dit modèle contrefactuel du sous-ensemble traité, permettant de générer l'ensemble des comportements possibles, commençant par les préfixes non affectés, en l'absence de dysfonctionnement des composants du sous-ensemble de composants traité (/) ; -déterminer la causalité nécessaire ou suffisante des composants du sous- ensemble (/) de composants testé pour le dysfonctionnement du système en fonction de la vérification du respect de ladite propriété globale du système par ledit modèle contrefactuel du sous-ensemble de composants traité. 8.- Produit programme d'ordinateur comportant des instructions pour mettre en oeuvre les étapes d'un procédé de détermination automatique de causalité nécessaire ou suffisante de dysfonctionnement d'un système composé d'une pluralité de composants matériels ou logiciels selon l'une des revendications 1 à 6 lors de l'exécution du programme par un processeur ou un circuit programmable d'un dispositif programmable.25