FR 2935500 A1 20100305 FR 0804812 A 20080902 PROCEDE ET SYSTEME PERMETTANT DE GENERER UN DISPOSITIF DE CONTROLE A PARTIR DE COMPORTEMENTS REDOUTES SPECIFIES L'invention concerne un procédé et un système permettant, à partir de la spécification en un langage formel d'un comportement redouté, de générer automatiquement un agent observateur, appelé moniteur, capable, en ligne, pendant une durée arbitraire et sans perte de perforrnance, de signaler toute occurrence dudit comportement redouté spécifié lors du fonctionnement d'un système susceptible de produire ce comportement. Elle permet la génération automatique de détecteurs de comportements spécifiés en logique temporelle linéaire métrique, ayant une mémoire bornée, capable de fonctionner en ligne et pendant un temps arbitrairement long. Elle est notamment utilisée pour le contrôle et la surveillance de systèmes simulés ou encore de systèmes physiques. Elle permet aussi d'effectuer des diagnostiques en ligne de systèmes de contrôle-commande, des surveillances d'environnements en domotique ou robotique. Elle est aussi mise en oeuvre pour la preuve de propriétés sur des exécutions/simulation finies. Différentes industries sont concernées par l'invention, comme : les industriels du transport, des télécoms, des services Internet, de la robotique ou encore de la domotique. Sur le marché des équipements industriels et grand public, les demandes de performances et de fonctionnalités s'accroissent continuellement. Pour faire face à ces demandes, les industriels ont été conduits à concevoir et à produire des systèmes dits complexes, c'est-à-dire constitués d'entités de natures différentes (mécanique, électronique, informatique, etc.) fonctionnant en forte interaction. Cet accroissement de complexité des systèmes va de pair avec l'augmentation du risque d'erreurs commises lors des phases de conception et de réalisation. Or ces erreurs se répercutent bien souvent sous la forme d'anomalies de fonctionnement du produit final. II est donc crucial, pour des raisons évidentes de sécurité des personnes, d'économie et de préservation de l'image de marque, de détecter des erreurs de conception et/ou de réalisation avant qu'un produit soit mis sur le marché. Les industriels qui produisent des systèmes complexes sont à la recherche de méthodes et d'outils permettant de minimiser le nombre d'erreurs commises lors du cycle de développement de leurs produits, que ce soit en amont lors des phases de conception ou bien en aval lors des phases de test de validation. Les méthodes formelles connues de l'art antérieur permettent, sur un périmètre limité, de remplir en partie au moins cet objectif. En général, elles proposent des langages de spécification et des structures de modélisation mathématiquement fondés, grâce auxquels, il est possible de prouver mathématiquement qu'un modèle proche de la réalisation d'un produit est conforme à la spécification de ce produit. Principalement, deux approches techniques se sont imposées à l'heure actuelle. Tout d'abord, les techniques de preuve, basées sur les spécifications algébriques. Ces techniques, si elles permettent de traiter des fonctions complexes, algorithmiques, ne sont pas complèternent automatiques. Les outils dédiés sont des assistants de preuve et la partie subtile des preuves est confiée à des experts qualifiés. L'autre type de technique plus connue sous l'abréviation anglo-saxonne � model-checking � est totalement automatique, mais présente comme inconvénient d'être limitée au traitement d'une classe de modèles simples, orientés flot de contrôle (sans algorithmes). De surcroît, les modèles analysés par la technique de � model-checking � doivent être limités en taille. A défaut, les outils consomment des ressources en espace mémoire et temps de calcul inaccessibles en pratique. Par ailleurs, les méthodes formelles proposent également des techniques de test qui automatisent la génération de tests à partir de modèles exécutables. Mais souvent, les tests ne répondent pas nécessairement aux objectifs intuitifs de l'utilisateur. Ces tests n'aident donc pas l'utilisateur à accroître sa confiance dans la correction du système qu'il a réalisé. Face à ces difficultés les techniques dites de monitoring permettent d'apporter des réponses pertinentes. Ces techniques sont qualifiées de techniques � boîte noire � en ce sens qu'elles ignorent la structure interne d'un système, pour ne s'intéresser qu'à ses productions observables. L'avantage de telles techniques est qu'elles peuvent être mises en oeuvre quel que soit le système puisque sa complexité intrinsèque n'est pas prise en compte. En revanche ce sont des techniques de falsification : elles peuvent apporter la preuve qu'un système ne satisfait pas une exigence, mais non que le système satisfera toujours une exigence. Le monitoring au sens le plus général consiste à observer un système, un processus, en vue de détecter un évènement plus ou moins complexe. Le monitoring formel se présente quant à lui comme une technique permettant de générer automatiquement des moniteurs à partir de spécifications en langages formels de comportements redoutés. Schématiquement un outil de monitoring formel est donc un outil qui accepte en entrée une expression spécifiant un comportement redouté et produit en sortie un moniteur capable de détecter l'occurrence du comportement redouté. Dans l'art antérieur il existe principalement deux approches de monitoring formel connues du Demandeur. Une première approche est due à Prasanna Thati et Grigore Rosu. Cette approche est décrite dans l'article intitulé � Monitoring Algorithms For Metric Temporal Logic Specifications �. Cette approche propose de générer un moniteur pouvant fonctionner en ligne, à partir d'une logique métrique linéaire. Le procédé de Thati et Rosu est basé sur la réécriture et l'évaluation dynamique de formules et engendre de fait plusieurs limitations. Le principe de cette approche consiste à exploiter l'expression même du problème du monitoring à savoir � est-ce qu'un comportement observé satisfait cl) � où cl) est une formule qui spécifie un comportement redouté. Problème que l'on peut noter plus brièvement : CI=cD? (Lire : est-ce que le comportement observé C valide (D ?) Avant d'avoir observé le système, le problème se pose donc comme suit : 01_ (D ? où 0dénote le comportement vide Le procédé de Thati et Rosu fonctionne ainsi : il maintient l'expression du problème de la satisfaction à mesure que les observations arrivent, en tenant compte de celles-ci. Si, à un certain stade, le problème du monitoring s'exprime sous la forme � C 1= cä ? � et qu'une nouvelle observation o est disponible, il calcule (Dä+1, une nouvelle formule, telle que l'on ait : C1=fin C.o1=cDä+1 où C.o est le comportement défini comme le comportement C suivi de l'observation o. Par transitivité : 0I_(D ~...~C1=(Dn C.oI=c4n+1 Le principe consiste donc à réécrire l'expression du comportement redouté en fonction des évènements déjà observés du système, tout en maintenant la problématique initiale, à savoir � 0 1_ (D ? �. Ce que les auteurs � appellent résoudre le passé et dériver le futur �. Pour ne pas stocker la trace d'exécution (afin que le moniteur garde une mémoire bornée), il est nécessaire de maintenir en permanence une table de vérité de toutes les formules qui peuvent potentiellement apparaître lors du procédé de réécriture. De la sorte, il est possible de calculer la valeur de vérité de la formule principale en utilisant les valeurs contenues dans la table. Mais, pour que le moniteur ait une mémoire bornée, il faut que cette table soit finie et par conséquent que l'ensemble des sous-formules pouvant apparaître soit lui-même fini. Or ceci n'est possible que si les pas d'exécution permis sont en nombre finis et connus à l'avance. Ainsi ce procédé présente notamment les inconvénients suivants : • La logique de spécification ne supporte que des intervalles dont les 30 bornes sont des entiers naturels, • Les pas d'exécution permis pour le système doivent être en nombre finis et connus à l'avance. Dans l'article précité, les pas d'exécution permis sont des entiers naturels (ainsi que l'indiquent les définitions de F+O) et F-((D)), • Enfin, l'algorithme est très consommateur de temps puisque la complexité estimée est de l'ordre de m323m où m est le nombre total de sous-formules obtenues à partir de la formule principale (l'ordre de grandeur de m par rapport à la formule principale n'étant quant à lui pas donné dans l'article). Une deuxième approche connue du Demandeur est décrite dans le document intitulé � Monitoring Temporal Properties of Continuous Signais � de Oded Maler et Dejan Nickovic. Le moniteur de Oded Maler et Dejan Nickovic se base sur le calcul des intervalles de validité d'une formule. Pour une formule donnée, et un comportement donné, le procédé de Maler et Nickovic calcule un ensemble d'intervalles de temps qui dénotent les dates où la formule est vraie et en dehors desquels la formule est fausse. Le calcul est fait d'abord pour les formules de base (propositions) puis pour les formules plus complexes. Pour cela, les auteurs définissent une correspondance entre les opérateurs de la logique de spécification et les opérations classiques sur les ensembles d'intervalles (intersection, union ...). Par exemple, en connaissant les intervalles de validité de deux formules d), et (132, il est possible de déduire qu'un intervalle i est dans l'ensemble des intervalles de validité de la formule (DI A 0132 Si et seulement s'il existe un intervalle j de (D, et un intervalle k de (D2 tels que i = j n k. Cette technique permet le calcul des intervalles pour une logique temporelle qui supporte des intervalles dont les bornes ne sont plus limitées aux entiers et l'analyse d'exécutions dont le pas est libre. Outre le fait qu'il n'existe pas d'opérateurs sur le passé dans la logique présentée, l'approche souffre d'un défaut essentiel, indiqué par les auteurs. Le moniteur de Oded Maler et Dejan Nickovic travaille hors ligne, sur une exécution enregistrée. Ceci représente une limitation importante car, sur un temps d'exécution long, le stockage de l'exécution peut ne pas être praticable (système autonome, embarqué ...). Ceci limite donc les temps de surveillance et de fait aussi les applications. Définitions Dans la suite de la description, certains termes seront utilisés pour mieux 5 comprendre et définir l'objet de l'invention, certaines définitions sont données ci-dessous. Notion de processus Le comportement d'un modèle de système ou d'un système physique est représenté par l'évolution dans le temps d'un certain nombre de variables 10 caractéristiques. Par exemple le comportement d'un corps, en physique des solides, est caractérisé par l'évolution de ses variables caractéristiques que sont sa position, sa vitesse, son accélération, son moment cinétique, etc. Proposition. A l'égard d'un système le terme � proposition � désigne toute expression 15 faisant référence aux variables caractéristiques du système et pouvant être vraie ou fausse. Par exemple � la vitesse du corps k vaut 10 m/s �, � la vitesse du corps k est strictement positive �, sont des propositions classiques en physique des solides. Mathématiquement, ces propositions seraient notées � vk == 10 �, � vk > 0 �. Nous voyons que ces expressions peuvent 20 être vraies ou fausses. Par exemple, si la vitesse observée du corps k est de 5m/s, alors la proposition � vk == 10 � est fausse puisque � 5 == 10 � est fausse. Dans la suite le terme proposition désigne toute expression langagière, portant sur les variables caractéristiques d'un système, pouvant être soit vraie, soit fausse. 25 Instantané. Le terme instantané relativement à un ensemble A de propositions est utilisé pour désigner un couple composé d'un ensemble inclus dans l'ensemble A de propositions et d'une date (un réel positif, c'est-à-dire un élément de R+). IA, l'ensemble de tous les instantanés relativement à A est donc P(A) x R+ 30 (où P(A) dénote l'ensemble des sous-ensembles de A). En comptant pour 1 chaque donnée, la taille maximale d'un instantané est donc 1AI + 1 (où IAI dénote le cardinal de l'ensemble A). Par exemple ({po, pl}, 1.3465) est un instantané relativement à A = {po, pi, p2}. Intuitivement un tel instantané peut se lire : à la date 1.3465, les propositions po et pi sont vraies et p2, absente de l'instantané, est fausse. Intuitivement un instantané donne l'état des propositions d'intérêt à une certaine date : c'est une photographie d'un système à une certaine date. Processus. Dans le contexte de la présente invention le terme processus est utilisé relativement à un ensemble A de propositions pour désigner toute suite indicée par les entiers naturels d'instantanés relatifs à A. Mathématiquement un processus est donc une application de S dans IA où S c N, est un segment initial de N (pour tout i E S, si i>0 alors i-1 E S). Par convention le premier instantané porte la date O. En tant que suite d'instantanés, un processus est donc intuitivement une sorte de � film � du fonctionnement du système. Liste de validité Une liste de validité est une liste dont les éléments sont des intervalles de R+, tous disjoints, rangés dans l'ordre croissant (chronologique). La notation (il, i2, ..., in) sera utilisée pour désigner une liste de validité contenant les intervalles il, i2, ... in. Par exemple : ([0, 2.43 [, [3.27, 5.04] ) est une liste de validité qui contient deux intervalles, [0, 2.43 [ et [3.27, 5.04]. Ils sont rangés dans l'ordre croissant ou chronologique. Il sera exposé par la suite qu'une liste de validité est par destination attachée à une expression et permet de définir, sur une plage temporelle donnée, les dates où cette expression est vraie et les dates où elle est fausse, en se conformant à la convention suivante : les dates qui sont à l'intérieur des intervalles de la liste de validité sont les dates où l'expression est vraie ; en dehors de ces intervalles l'expression est fausse. L'objet de la présente invention concerne un procédé et un système permettant de remédier au moins aux imperfections des méthodes précitées. L'invention concerne notamment un procédé permettant de générer automatiquement, à partir de la spécification formelle d'un comportement redouté écrite en logique temporelle linéaire métrique, un agent automatique, appelé moniteur, à mémoire bornée, capable d'analyser � en ligne � la simulation d'un modèle de système ou le fonctionnement d'un système physique afin d'y détecter l'occurrence du comportement redouté spécifié. Le procédé peut donc être utilisé dans les phases de conception pour analyser un modèle, ou dès les phases de test pour analyser le fonctionnement du système réalisé. Synthétiquement la présente invention repose sur l'utilisation d'un langage formel permettant de spécifier des comportements redoutés et d'un procédé permettant de transformer n'importe quelle expression de ce langage en un moniteur performant, fonctionnant en ligne, sans limite de durée. L'objet de la présente invention concerne un procédé permettant de générer un détecteur de comportements redoutés spécifiés en logique temporelle linéaire métrique d'un système dont le comportement est à surveiller caractérisé en ce qu'il comporte au moins les étapes suivantes : • définir des variables caractéristiques du système à surveiller, • définir un certain nombre de propositions p sur ces variables, • allouer en mémoire du détecteur un espace suffisant pour mémoriser un instantané I relatif à ces propositions, • définir une formule principale cl), construite sur lesdites propositions p, traduisant un comportement redouté en utilisant un langage composé d'opérateurs logiques et d'opérateurs temporels portant sur le futur et le passé, • de façon régulière ou périodique faire l'acquisition de la valeur des variables caractéristiques du système observé et mémoriser la date 30 de cette acquisition, • en fonction des valeurs des variables caractéristiques issues de l'acquisition réalisée à l'étape précédente, évaluer les propositions p rafraichir l'instantané I en conséquence et attribuer à I la date d'acquisition mémorisée, • Pour chaque rafraichissement de l'instantané I : o calculer la fenêtre de continuation cw de la formule principale c et les fenêtres de continuation respectives de toutes ses sous-formules au moyen d'une fonction Cert définie comme une fonction qui pour toute formule 40' passée en argument renvoie un nombre réel tel que [0, t-Cert(c')] soit l'intervalle de certitude de la formule .13', où t est la date portée par l'instantané courant, o Appel d'un algorithme récursif de calcul de la continuation de la liste de validité d'une formule CALCUL LV W sur la formule principale pour prolonger le calcul de sa liste de validité sur sa fenêtre de continuation cl)w, o exploiter les informations contenues dans la liste de validité LV de la formule principale (D et émettre un signal associé. L'invention concerne aussi un système permettant de générer un détecteur de comportements redoutés spécifiés en logique temporelle linéaire métrique, à mémoire bornée, caractérisé en ce qu'il comporte au moins les éléments suivants : o Une entrée recevant un ou plusieurs paramètre(s) caractéristique(s) de l'état du système à surveiller, et une horloge H indiquant la date d'acquisition de ce(s) paramètre(s), o Un processeur adapté à exécuter les étapes du procédé selon l'invention en utilisant le(s) paramètre(s) mesuré(s) et la date associée, o Une mémoire adaptée à o mémoriser l'instantané courant o mémoriser les listes de validité LV déterminées par la mise en oeuvre du procédé pour la formule principale et ses sous-formules, o une ou plusieurs sorties émettant un signal S correspondant aux 5 informations contenues dans la liste de validité pour la formule principale et émettre ledit signal. D'autres caractéristiques et avantages du dispositif selon l'invention apparaîtront mieux à la lecture de la description qui suit d'un exemple de 10 réalisation donné à titre illustratif et nullement limitatif annexé des figures qui représentent : • La figure 1 un synoptique du procédé selon l'invention, et • la figure 2 un exemple d'architecture du système permettant sa mise en oeuvre, 15 • La figure 3, un algorithme de calcul de la liste de validité d'une proposition ou d'une formule dite purement propositionnelle, • Les figures 4, 5 et 6 illustrent le calcul de la liste de validité d'une formule en fonction de celles de ses sous-formules, • La figure 7, l'illustration du calcul de la date de certitude d'une formule 20 en fonction de celle de sa sous-formule (pour l'opérateur unaire portant sur le futur), • La figure 8A, illustration de la définition d'une zone d'influence prise en compte pour la mise en oeuvre du procédé selon l'invention, • La figure 8B, illustration de l'inutilité des sous-formules directes d'une 25 formule étant donnée la date d'inutilité fixée pour celle-ci, et • La figure 9 un exemple d'application pour la surveillance du comportement d'un système masse-ressort. L'idée de la présente invention consiste notamment à générer un moniteur 30 capable d'observer le comportement d'un système dans un environnement donné et plus particulièrement l'évolution d'un processus au sens défini précédemment au début de la description. La figure 1 est un synoptique d'un exemple du procédé selon l'invention comprenant un système S dont le comportement est à observer, une horloge temporelle H permettant de déterminer la date à laquelle un instantané a été acquis, un processeur qui va traiter les données issues du système à surveiller, par exemple une variable observée à un instant donné et qui va être capable d'évaluer la valeur des propositions où cette variable apparaît, de calculer ensuite les listes de validité attachées à ces propositions puis les io listes de validité des formules plus complexes jusqu'à la liste de validité de la formule principale spécifiant le comportement redouté. Sur la figure 2 est représenté un exemple de système selon l'invention qui comporte, le système S dont le comportement est surveillé. Le système comprend un ou plusieurs capteurs 10 permettant de déterminer la valeur de 15 chaque paramètre représentatif du comportement surveillé. Par exemple, il est possible d'avoir un capteur de température et de vérifier si une proposition portant sur la température est vraie. Des exemples sont donnés ci-après. Le ou les capteurs de paramètres équipant le système S sont reliés à un dispositif 11 comprenant une entrée 12 et un processeur 13 qui va 20 traiter les différentes données ainsi qu'une mémoire 14 stockant l'instantané courant et les listes de validité de chaque formule. Le dispositif 11 comprend aussi une entrée 15 recevant une horloge spécifiant une date associée à un paramètre mesuré. Le processeur 13 va délivrer via une ou plusieurs sorties 16i un signal S contenant des données permettant, par exemple : 25 • Soit l'affichage des résultats sur un dispositif d'affichage 17, • Soit la génération d'un signal à un dispositif de régulation du système, • Soit la génération d'un signal d'alarme. Le signal obtenu est transmis à un dispositif de génération d'une alarme et/ou à un système de contrôle ou de régulation du système placé sous la 30 surveillance d'un moniteur généré par le procédé selon l'invention. Le système dont le comportement est surveillé peut être un modèle exécuté en simulation. Ce modèle peut parfaitement être très complexe et/ou de grande taille étant donné que le moniteur généré selon l'invention ne dépend pas de la structure interne de ce modèle. Dans ce cas le procédé peut être considéré comme une technique de débogage de modèles. Le système peut aussi être un dispositif ou un système physique dont on souhaite contrôler le comportement en fonctionnement et notamment vérifier son comportement. Le procédé peut alors être considéré comme une sous-partie d'un système plus vaste de contrôle-commande. Ainsi, le système selon l'invention peut être appliqué comme dispositif permettant de détecter des erreurs dans le fonctionnement d'un système, plus connu sous l'expression � débogueur � de systèmes simulés, ou comme moniteur de systèmes physiques pour en détecter les disfonctionnements ceci dans tout domaine industriel (transport, domotique, robotique). Un moniteur selon l'invention est constitué notamment de plusieurs éléments qui vont être explicités ci-après. Les notions de processus, de proposition, de liste de validité et d'instantané ont été définis précédemment. Un des éléments entrant dans la génération du moniteur est la notion de liste 20 de validité qui est représentée par exemple dans les Figures 4, 5, 6. La manière dont une liste de validité peut être déduite d'un processus (au sens défini plus haut) est illustrée de la manière suivante. Pour cela examinons l'information qui est délivrée par un processus à un observateur 25 ou à un capteur ou à un dispositif de surveillance au sein d'un procédé. Pour cet observateur l'information I; délivrée par un instantané du processus subsiste jusqu'à ce que l'instantané suivant 1i+1 rafraichisse cette information. Autrement dit l'information délivrée par un instantané de date t vaut jusqu'à t' où t' est la date de l'instantané suivant. Si le dernier instantané du processus 30 porte la date z, ce principe permet de définir la validité d'une proposition à toute date de [0, z] et donc une liste de validité sur cette plage. Pour l'illustrer, les étapes de création d'une liste de validité pour la proposition po tel que le ferait un observateur placé face au processus sont déroulées ci-dessous. Le processus commence avec l'instantané 0. L'observateur remarque que la proposition po est présente, c'est-à-dire vraie. II ajoute à la liste de validité de po un premier intervalle soit [0.0, 0.0]. La liste de validité de po est donc ([0.0, 0.0]). Arrive l'instantané 1. po est toujours vraie. La valeur date est 1.71. Le procédé prolonge l'intervalle de validité précédent. La liste devient ([0.0, 1.71]). A l'Instantané 2, po disparaît, ce qui signifie que cette valeur est fausse. La valeur date est 2.43. Mais n'ayant pas eu d'information entre 1.71 et 2.43 il doit considérer que po était vraie jusque là. Donc l'observateur ou le procédé modifie l'intervalle précédent qui devient [0.0, 2.43 [. Noter que l'intervalle est ouvert à droite, puisqu'en 2.43 la proposition po est fausse. La liste de validité de po devient ([0.0, 2.43 [ ). A l'instantané 3, po redevient vraie. La valeur date est 3.27. Or elle était fausse à l'instantané précédent. L'observateur considère que jusque là elle était fausse. Il va donc créer un nouvel intervalle de validité pour po. Ainsi, en 3, la liste de validité de po est ([0.0, 2.43 [, [3.27, 3.27] ). Cet exemple montre qu'étant donné un processus il est possible d'associer à une proposition p une liste d'intervalles [Vd, Vf[ ou [Vd, Vf] qui dénotent les dates où la proposition est vraie. Alqorithme de calcul de la liste de validité d'une proposition A toute proposition p est associée une variable booléenne p.val et une variable de type liste d'intervalles p.Lv (� Lv � pour liste de validité). C'est p.Lv qui représente la liste de validité pour p. Si I est un instantané, I.t correspond à la date portée par I et I.p à la valeur de vérité que I attribue à la proposition p (I.p vaut faux si p n'est pas dans l'ensemble de propositions de I et vaut vrai si p est dans cet ensemble). L'algorithme est décrit par le diagramme illustré à la figure 3. La première étape, étape 20, est une étape d'initialisation des valeurs de p.val et de p.Lv. La variable p.val est initialisée à faux et la variable p.Lv est initialisée par la liste vide. L'étape qui suit, étape 21, est un état d'attente de rafraichissement de l'instantané I. Lorsque ce rafraichissement intervient l'algorithme passe à l'étape 22 où la valeur de I.p est testée. Si la valeur de vérité de I.p est à vrai le procédé teste, étape 23, la valeur de p.val. Si p.val est à vrai alors, étape 24, le procédé prolonge le dernier intervalle de p.Lv jusqu'à I.t compris (intervalle fermé sur la valeur I.t). Si la valeur p.val est à faux alors, étape 25, le procédé ajoute à la fin de p.Lv le nouvel intervalle [I.t, I.t]. Si au contraire, à l'étape 22, I.p est faux, alors le procédé teste p.val. Si p.val est à vrai , étape 26, alors le procédé prolonge le dernier intervalle de p.Lv jusqu'à I.t non compris (ouvert sur I.t) (étape 28). Si p.val est à faux, alors le procédé laisse p.Lv inchangée (étape 27). A la suite des étapes 24, 25, 27 et 28, le procédé affecte à p.val la valeur de I.p (étape 29). Puis le procédé retourne à l'étape 21 d'attente de rafraichissement de I, le calcul se prolongeant tant que le procédé est maintenu en fonctionnement. En tant que tel, il n'existe pas de condition d'arrêt pour cet algorithme de calcul puisqu'il se met en attente d'un nouvel instantané. Il peut néanmoins être facilement modifié si l'indication qu'un instantané est le dernier est disponible. Dans ce cas le retour à l'étape 21 serait soumis à la condition que l'instantané soumis ne soit pas le dernier. La condition d'arrêt sera déterminée par une stratégie d'utilisation du procédé complet c'est-à-dire par une stratégie d'exploitation des listes de validité. A partir de l'algorithme de calcul des listes de validité pour les propositions détaillées ci-dessus, le procédé peut générer un moniteur simple, pour un langage restreint aux propositions. Un premier exemple de mise en oeuvre du procédé est donné à titre non limitatif, pour un comportement redouté spécifié par une seule proposition. Dans cet exemple, il est proposé de générer un moniteur permettant d'observer le compte en banque d'un client, en posant comme comportement redouté que le solde soit négatif autrement dit que la proposition � solde langage permettant de décrire des comportements plus évolués, faisant intervenir plusieurs propositions et permettant de décrire des notions complexes d'ordre, de concomitance, ou d'occurrence dans des délais stricts, sur les propositions. Spécification formelle des comportements redoutés Nous donnons d'abord la syntaxe du langage du procédé selon l'invention. Le sens des opérateurs introduits sera explicité ensuite, lors de l'exposé de la sémantique de ce langage. La syntaxe dudit langage formel de spécification des comportements redoutés selon l'invention est la suivante : ^ Tout symbole de proposition est une expression du langage selon l'invention • Si a) est une expression dudit langage, que a et b sont des réels positifs tels que b >_ a, alors sont aussi des expressions de ce langage : 0 -,J o F[a,b] CD o P[a,b] CD o P[a,>] o (cl) ) • Si ED1 et 02 sont deux expressions dudit langage et que a et b deux réels positifs tels que b a alors sont aussi des expressions de ce langage o (D1 n 432 ^ (D1 U[a,b] (D2 25 O I1 S[a,b] t2 o (D1 S[a,>] (D2 En notation BNF (Backus-Naur Form) le langage s'écrit de façon concise : 1::= p I , ' I a:)1 A (D2 I F[a,b] q P[a,b] (I P[a,>] C I (D, U[a,b] 1112 I I1 S[a,b] I2 I 30 S[a,>102I () où p dénote tout symbole de proposition, a, b dénotent des réels positifs tels que b ? a. Dans la suite de la description, une expression de ce langage sera appelée une formule. Les parenthèses sont utilisées pour désambiguïser une formule. En effet, si l'on écrit C1 A 02 U[a,b] 03 on ne sait s'il faut lire ((D1 A )2) U[a,b] (D3 ou bien lire (D1 n (I 2 U[a,b] CI33). Or ces formules ne sont pas équivalentes, d'où l'importance des parenthèses. Quelques exemples de formules : • P1AP2 • P3 U[0, 12] ((-i (P[143,5.64] (P1 A-i P2 )) A (-i F[2.43, 7.85] P2)) Les opérateurs v (disjonction) et - (implication), peuvent aussi être utilisés, puisque ce ne sont que des abréviations exprimables dans le langage. • (D1 v (D2 est une abréviation de û, ((-4 i) A (û02)) • ~1 (D2 est une abréviation de (-, (D1) v CD2 et donc de ûi(cD1 A(- 4 2)) L'ensemble des sous-formules d'une formule est donné par la fonction SF définie de la façon suivante : • SF(p) = 0 (l'ensemble vide) • SF(û1 (D)={ED} uSF(c) • SF((D1 n (2) = { (P1, ED2 } u SF((D1) u SF(cP2) • SF(F[a,b] (D) = { ( } u SF(ED) • SF(P[a,b] (D) = { (D } u SF((D) • SF(P[a,>] d)) = { (D } u SF(ED) • SF(ch1 U[a,b] (D2) = { (D1, (D2 } u SF((D1) u SF(cD2) • SF(ct)1 S[a,b] 42) = { CD 1, (D2 } u SF(O1) u SF((D2) ^ SF((D1 S[a,>] (D2) = { 01, (D2 } u SF((D1) u SF((t2) • SF(((D)) = SF(cD)30 Par exemple : SF(ùip)={p}uSF(p)={p}u0={p} SF ( F[2.43, 7.85] (P1 n-i P2)) = { (P1 n-1 P2), --1 P2, P1 , P2 } Les sous-formules directes d'une formule sont celles placées directement sous son opérateur. Par exemple, pour -43 il s'agit de (D. Pour (DI U[a,b] CD2 il s'agit de (DI et (D2. Une formule du langage est dite purement booléenne si : • c'est une proposition ou bien • son opérateur n'est pas temporel (par exemple dans {ù,,v,A,ù>}) et toutes ses sous-formules sont aussi purement booléennes. Sémantique du langage de spécification formelle des comportements redoutés Sémantique intuitive : • L'opérateur est la négation. -4) est vraie si et seulement si est fausse. • L'opérateur A est appelé conjonction. La formule (DI A CD2 n'est vraie que si (DI et CD2 sont toutes deux vraies. • L'opérateur F[a,b] porte sur le futur. Cet opérateur signifie intuitivement � dans le futur, entre a et b � ou encore � il y aura entre a et b �. Plus rigoureusement la formule F[a,b] (D est vraie à 25 une date t si et seulement s'il existe une date entre t+a et t+b où est vraie. • L'opérateur P[a,b] porte sur le passé. Cet opérateur signifie intuitivement � dans le passé, entre a et b � ou encore � il y a eu entre a et b �. Plus rigoureusement la formule P[a,b] (D est vraie en t 30 si et seulement s'il existe une date entre t-b et t-a où (I) est vraie. • L'opérateur P[a,>] porte sur le passé. Cet opérateur signifie intuitivement : � au-delà de -a dans le passé �. Plus rigoureusement la formule P[a,>] t)est vraie en t si et seulement s'il existe une date entre 0 et t-a où 43 est vraie. • L'opérateur U[a,b] porte aussi sur le futur (le � U � viens de l'expression anglo-saxonne � Until �). Cet opérateur signifie intuitivement : � (I)2 sera vraie entre a et b et (D, sera partout vraie entre temps �. Plus rigoureusement la formule (DI U[a,b] 41)2 est vraie en t si et seulement s'il existe une date t' entre t+a et t+b où 02 est vraie et que 431 est partout vraie dans l'intervalle [t, t'[. • L'opérateur S[a,b] porte aussi sur le passé (le � S � viens de l'expression anglo-saxonne � Since �). Cet opérateur signifie : � (1)2 sera vraie vers le passé entre -b et -a et (D1 sera partout vraie entre temps �. Plus rigoureusement la formule (PI S[a,b] (D2 est vraie en t si et seulement s'il existe une date t' entre t-b et t-a où (D2 est vraie et que (1 est partout vraie dans l'intervalle ]t', t]. • L'opérateur S[a,>] porte aussi sur le passé. Cet opérateur signifie : � 02 sera vraie vers le passé au-delà de -a et tI sera partout vraie entre temps �. Plus rigoureusement la formule (DI S[a,>i 432 est vraie 20 en t si et seulement s'il existe une date t' entre 0 et t-a où (D2 est vraie et que (DI reste vraie dans l'intervalle ]i:', t]. Sémantique formelle : L'objet de cette définition est de donner un sens mathématique à la notion de 25 validation d'une formule par un processus it (processus au sens défini ci-avant) à une date t quelconque. La notation 7t,t 1= se lit : � le processus 1t valide cl) à la date t � , et est définie ainsi : • it,t 1= p ssi p est dans l'ensemble de propositions de l'instantané 7t(i) où i est le plus grand rang des rangs d'instantanés dont les 30 dates sont inférieures à t (t est supérieure ou égale à la date portée par l'instantané n(i) et strictement inférieure à la date de l'instantané n(i+1) ). • n,t 1= ù, (D ssi n,t 1# (D (lire : n,t ne valide pas (D) • n,t1=ct1A t2ssin,t1=(D1et n,t1=(D2 • n,t 1= F[a,b] (D ssi il existe une date t' de [t+a, t+b] telle que n,t' 1= • n,t 1= P[a,b] C1 ssi il existe une date t' de [t-b, t-a] telle que n,t' 1= • n,t 1= P[a,>] (1 ssi il existe une date t' de [0, t-a] telle que n,t' 1= e. • n,t 1= 4)1 U[a,b] (D2 ssi il existe une date t' de [t+a,t+b] telle que n,t' 1= (D2 et pour toute date t" de [t,t'[ n,t" 1= 431 • n,t 1= ctii S[a,b] (D2 ssi il existe une date t' de [t-b, t-a] telle que n,t' 1= (D2 et pour toute date t" de ]t',t] n,t" 1= (DI • n,t 1= 4 i S[a,>] (D2 ssi il existe une date t' de [0, t-a] telle que n,t' 1= I2 et pour toute date t" de ]t',t] n,t" 1= (DI La notion de liste de validité précédemment exposée était limitée aux propositions. Sans sortir du cadre de l'invention, cette approche peut être étendue à toute expression de notre langage (les propositions ne formant qu'une partie de ce langage). Pour cela nous avons besoin d'établir la façon dont les opérateurs du langage se traduisent en termes d'opérations sur les listes de validités. Correspondance entre opérateurs du langage et opérations sur les listes de validité II a été précédemment exposé comment se constituait une liste de validité pour des propositions. Comme les formules complexes sont construites à partir des propositions et des opérateurs du langage, pour calculer les intervalles de validités des formules complexes, il est nécessaire d'établir une correspondance entre les opérateurs du langage et opérations sur les listes de validité. Une description informelle est donnée pour chaque opérateur de la logique. Pour calculer la liste de validité des formules purement booléennes l'algorithme de calcul utilisé pour les propositions est employé, moyennant une adaptation mineure. Comme pour une proposition, pour une formule purement booléenne, une variable booléenne c.val lui est associée. La valeur de 1.0 (valeur donnée par un instantané I à (D) est définie de manière inductive : • Si (D est une proposition p alors 1.0 est I.p • Si (D est la formule (D1 alors I.(D vaut la négation de valeur de vérité de I.c1 (I.(D vaut vrai si 1.431 vaut faux et réciproquement) • Si (D est (D1 A (D2 alors I.c vaut vrai si 1.01 et 1.432 valent tous deux vrai, faux sinon. Moyennant ces définitions le calcul des listes de validité d'une formule purement booléenne est identique à celui d'une proposition. Il suffit simplement d'appeler au préalable le calcul sur les sous-formules afin que toutes les variables en jeu soient définies (par exemple pour (D1 A 02 , on lance d'abord le calcul pour (D1 et pour (D2 de telle sorte que 1.01 et I.(D2 soient définies). Le calcul des listes de validité des formules non purement booléennes est maintenant abordé. L'idée générale est que la liste de validité d'une formule (D dépend de la liste de validité de ses sous-formules immédiates. Dans les cas énumérés ci-dessous les principes du calcul � hors ligne � sont exposés. Les principes du calcul � en ligne � seront présentés plus loin, lorsque nous aborderons les principes de certitude, de continuation et de zone d'influence. Nous faisons l'hypothèse implicite que le calcul est fait sur une certaine plage temporelle (qui n'a pas besoin d'être précisée pour exposer les principes). Cas de La figure 4 illustre le calcul de la liste de validité de -,q) connaissant celle de t). Le principe est le suivant : deux intervalles successifs i et i+1 de 43 donnent lieu à un intervalle pour -43 qui s'insère entre i et i+1. Des intervalles virtuels (détruits après le calcul) permettent de gérer les cas où les bornes de la plage de calcul ne sont pas comprises dans des intervalles de la liste de validité de (D. Cas de A. La liste de validité de (D, A CI32 est fonction de celles de (DI et de 432. Le principe est le suivant : si i, est un intervalle de ED1 et i2 un intervalle de (D2 et que i, n i2 ≠ 0, alors i, n i2 est un intervalle de (DI A ED2. Pour calculer la liste complète de (DI A CD2 en fonction de celles de (DI et de 02 nous utilisons deux boucles imbriquées. La première itère sur les intervalles de la liste de validité de 0112 de façon chronologique (du premier au dernier). Posons que son itérateur est il. La deuxième boucle itère de façon chronologique sur la liste de validité de (D2. Son itérateur est i2. Chaque fois que il n i2 ≠ 0 alors l'intervalle il n i2 est ajouté à la liste de validité de ()I n ED2. Par construction nous obtenons une liste de validité pour ED1 A t)2, rangée dans l'ordre chronologique. A des fins d'optimisation, la boucle sur la liste de validité de (DI termine lorsque la borne inférieure de son itérateur il est supérieure à la borne supérieure de i2 et que il n i2 ≠ 0. Pour la boucle en (D2 suivante i, est conservé comme point de départ (on ne re-parcoure pas la liste de (D, depuis le début à chaque fois). Cas de Fia,b]. La figure 5 illustre la manière dont un intervalle de F[a,b] (D est produit en fonction d'un intervalle existant dans la liste de validité de (D. Si i = [u,v] est un intervalle de (D alors l'intervalle [u-b, v-a] (noté aussi i û [a,b]) dans la liste de validité de F[a,b] (. Ceci illustre un traitement pour un intervalle isolé. Pour calculer la liste de validité complète de F[a,b] 013 en fonction de celle de le traitement est le suivant. On parcoure toute la liste de validité de 0, dans l'ordre chronologique. Pour chaque intervalle i de cette liste on calcule i û [a,b]. Cet intervalle i-[a,b] est adjoint à la liste de validité de F[a.b] cl) où adjoindre un intervalle m à une liste de validité signifie que : • Si m est disjoint du dernier intervalle de la liste de validité alors m est ajouté en fin de cette liste, • Si m n'est pas disjoint du dernier intervalle u de la liste de validité alors ce dernier intervalle u est remplacé dans la liste par l'intervalle u u m. ~o Dans la suite l'adjonction d'un intervalle dans une liste aura toujours ce sens. Cas de P[a.b]. Si i = [u,v] est un intervalle de d) alors [u+a,v+b] est un intervalle de P. Pour calculer la liste de validité complète de P[a,b] (D en fonction de celle de (D le traitement est similaire au cas de F[a,b] . 15 Cas de U[a,b]. La figure 6 illustre la manière dont deux intervalles respectivement de 431 et 02 donnent lieu à un intervalle de (DI U[a,b] . Cette figure 6 s'explique ainsi : (DI U[a,b] 02 est valide en une date t si 02 est vraie à une date t' de t + [a,b], et 0i est vraie auparavant c'est-à-dire partout sur [t,t'[. Sauf le cas 20 où a vaut 0, il résulte de ceci que deux intervalles il de 431 et i2 de 432 tels que il n i2 = 0 ne peuvent donner lieu à un intervalle pour (DI U[a,b] (D2 . En effet si il n i2 = 0 quelle que soit la date t de il, 01 ne peut être partout vraie jusqu'à une date de i2. Donc il n i2 ≠ 0 est une condition nécessaire pour que il et i2 génèrent un intervalle pour et U[a,b] ED2 . En considérant donc il et 25 i2 tels que K = il n i2 ≠ 0 comme sur la figure 6 (i'I ferme il sur sa borne supérieure), pour toute date t de k il existe une date postérieure t' de i2 telle que est partout vraie sur [t,t'[. Il en va de même de toute date de K' qui étend K vers le passé jusqu'à la borne inférieure de il. Pour qu'une date de cet intervalle K' valide 431 U[a,b] 4)2 il faut qu'elle soit aussi dans K", puisque 30 K" dénote toute date t telle que 02 est vraie dans le futur entre t+a et t+b. Ainsi, l'intervalle généré par il et i2 pour (DI U[a,b] CD2 est K' n K". Dans le cas particulier où a vaut 0, l'ensemble i2 est lui-même un ensemble de dates qui valident 01 U[a,b] . Pour calculer la liste de validité complète de (DI U[a,b] c2 en fonction de celles de (DI et (D2 nous opérons par deux boucles imbriquées. La boucle principale est sur la liste de validité de (D2. Soit i2 l'itérateur de cette boucle. L'autre boucle parcoure la liste de validité de (D,. Soit il son itérateur. A chaque fois que il n i2 ≠ 0 nous calculons un intervalle pour (DI U[a,b] (D2 comme expliqué, lequel est adjoint à la liste de validité de c1 U[a,b] CD2. A titre d'optimisation la boucle sur (DI est terminée dès que il est supérieur à i2 et d'intersection vide avec i2. L'itérateur il n'est pas réinitialisé pour l'itération suivante sur la boucle en (D2 (la liste de (DI n'est pas re-parcourue depuis le début à chaque fois). Si a vaut 0, i2 est adjoint en dernier. Cas S[a,b]. Similaire à U[a,b] mais retourné vers le passé. Cas P[a,>]. La liste de validité de P[a,>i 1 ne dépend que du premier intervalle de la liste de validité de 4. Si celui-ci existe et est de la forme [u,v] alors la liste de 20 validité de P[a,>]c est composé de l'unique intervalle [u+a,00[. Cas S[a,>]. Considérons la formule 4 S[a,>] c2 . Là encore pour que i, de (DI et i2 de 02 produisent un intervalle pour E D1 (D2 il faut que il n i2 ≠ 0. Supposons que ce soit le cas. Supposons que i2 soit [u,v]. Posons k = [u+a, oo[. Alors k n 25 il est un intervalle de validité pour (Del Sta,>] (D2. Pour calculer la liste complète de (DI S[a,>] (D2 en fonction de celles de (Di et cD2, on utilise deux boucles comme décrit pour C1 U[a,b] (D2 et chaque production est adjointe à la liste en cours. Une description de la correspondance entre opérateurs et composition des listes de validité a été donnée ci-avant. Cette description a été décomposée en deux parties pour la plupart des opérateurs. Une description locale qui montre comment un intervalle d'une formule est produit à partir d'un ou deux (un si l'opérateur est unaire, deux s'il est binaire) intervalle(s) de sa ou ses sous-formule(s). La seconde partie décrit la manière dont la liste complète est construite. Nous pouvons apporter la preuve que la seconde description est correcte et complète vis-à-vis de la première à savoir que (complétude) toute production locale est bien prise en compte dans le calcul effectif complet et que réciproquement (correction) toute date de la liste complète est une date résultant d'une production locale. Principe du calcul de la liste de validité de la formule principale Une partie notable du procédé selon l'invention repose sur le calcul de la liste de validité d'une formule dite principale qui est donnée en entrée du procédé par l'utilisateur. Le principe de ce calcul est fondé sur un algorithme récursif. En effet, dans la section précédente il a été vu que la liste de validité d'une formule complexe dépend de celles des ses sous-formules. Le calcul est donc par nature récursif puisque le calcul pour une formule complexe doit être appliqué au préalable sur les sous-formules. En dernière instance le calcul atteint des propositions ou bien des formules purement booléennes pour lesquels l'algorithme dédié est appliqué. Voici schématiquement l'algorithme général de calcul de la liste de validité d'une formule. Cet algorithme est appelé CALCUL_I_V(ED) (pour CALCUL de 25 la Liste de Validité) : CALCUL LV(113) : { 1. Si 1 est une proposition ou une formule purement booléenne, calcul de la liste de validité selon l'algorithme propre à ce type de formule. 30 2. Sinon identification de l'opérateur de la formule cl), a. Appel de CALCUL_LV(41) où 431 est la première sous-formule directe de 0, b. Si t possède une deuxième sous-formule directe (1)2 (l'opérateur est binaire) appel de CALCUL_LV(cD2) , c. Composition des listes de validité des sous-formules selon l'opérateur comme expliqué dans la section Correspondance entre opérateurs logiques et opérations sur les listes de validité. } A ce stade seul un calcul non optimisé dont la mise en oeuvre en ligne nécessiterait de recalculer entièrement les listes de validité des formules complexes à chaque nouvel instantané a été explicité. Ceci présente comme inconvénient d'être coûteux, à la fois en temps et en taille mémoire. Les principes du calcul optimisé et en ligne vont être exposés ci-après. Comme il va être vu, il s'agit de conserver les résultats déjà obtenus lorsque le procédé est assuré qu'ils ne seront plus modifiés et de ne faire que les calculs nécessaires au prolongement de ces résultats. De sorte que le calcul peut être vu comme une suite de calculs locaux qui prolongent des résultats acquis antérieurement. Principes du calcul en liqne (certitude, continuation et zone d'influence) Le procédé de calcul selon l'invention efficace, en ligne, et à mémoire bornée, des intervalles de validité repose sur des principes originaux qui vont être exposés. Ce sont les principes de certitude, de continuation et de zone d'influence. Corollaire de la notion de zone d'influence, la notion de date d'inutilité permet de doter le procédé d'un mécanisme essentiel à son fonctionnement sans limite de durée, à savoir l'élimination des intervalles devenus non pertinents du point de vue de la problématique de détection du comportement redouté. Principe de certitude : Ce principe consiste à déterminer, à tout moment et pour toute formule du langage, la portion de sa liste de validité qui restera 30 inchangée, quoique qu'il advienne par la suite. Pour rendre opérationnel ce principe, le procédé définit une fonction, appelée Cert, qui prend en argument une formule et renvoie un nombre réel et ce de telle sorte que [0, t û Cert(()] soit cet intervalle de certitude de d), lorsque t est la date portée par le dernier instantané. Pour une proposition p, si t est la date portée par le dernier instantané, il est clair que la liste de validité de p sur [0, t] est figée, quoiqu'il advienne après t. Il faut donc poser Cert(p) = 0 pour que [0, t û Cert(p)] soit l'intervalle de certitude de p. En effet, en posant Cert(p) = 0, nous avons bien [0, t û Cert(p)] = [0, t û 0] = [0, t]. Avant de généraliser à tous les opérateurs, ce principe est présenté dans un premier temps pour l'opérateur F[a,b] qui est temporel. En se référant à la sémantique de cet opérateur, la validité d'une formule de type F[a,bj ( n'est pas complètement déterminée à une date u tant que la valeur de ( n'est pas connu sur tout l'intervalle [u+a, u+b]. Autrement dit, si le dernier instantané I n'a pas encore atteint ou dépassé la date u+b, la valeur de F[a,b] cl) en u reste incertaine. La Figure 7 illustre ce principe, la validité de F[a.b] est certaine en tl et incertaine en t2. En prenant le point de vue dual, il est possible d'affirmer que si cl) est certaine jusqu'à une date v, alors il ne peut y avoir de certitude sur la valeur de F[a,bi( que jusqu'à la date v - b. Puisque par définition v est alors t-Cert(ED), alors F[a,b] (I) n'est certaine que jusqu'à : (t-CertO - b = t û (CertO+b). D'où il découle que Cert(F[a,b] cl)) = CertO+b. Ce résultat se retrouve dans la définition générale de la fonction Cert donnée ci-après. La certitude d'une formule se définit de façon inductive en partant des propositions pour lesquelles la fonction Cert est connue (comme nous venons de le voir elle vaut 0), pour aller ensuite vers les formules plus complexes. Au final cette fonction prend en argument une formule et renvoi un nombre réel (ce nombre ne dépend que de la formule et peut donc être calculé statiquement). Comme il a été dit cette fonction est définie de telle sorte que [0, t ù Cert(cl))] soit l'intervalle de certitude de (D, lorsque t est la date portée par le dernier instantané observé. Définition inductive de la fonction Cert: • Cert(cl)) = 0 si 1 est une proposition • Cert(-4)) = Cert(cD) • Cert(ED1 A CI32) = sup (Cert((D1), Cert(c1)2)) • Cert(FIa,b] = Cert(cD) + b • Cert(c1?1 U[a,b] (2) = sup (Cert(cD1), Cert(c1?2)) + b • Cert(P[a,b]c1?) = Cert(ch) ù a • Cert (P[a,>] cl)) = Cert(cD) ù a • Cert(di1 S[a,b] (2 ) = sup (Cert((1), Cert(c1?2)) • Cert(c1?1 S[a,>] ED2 ) = sup (Cert(cD1), Cert((2)) Par exemple, la Certitude de (c01 U[a,b]42) s'explique en se référant à la figure 6. Cette figure illustre la façon dont un intervalle de c>;2 et un intervalle de (D1 donnent lieu à un intervalle pour c1)1 U[a,b] CD2 . Sur cette figure 6, cet intervalle est K' n K". Or la certitude d'une intersection est donnée par la plus petite date des certitudes attachées aux intervalles qui interviennent. K' n'est certain que jusqu'à la date de certitude de K, à savoir jusqu'à t - sup (Cert(c1?1), Cert((12)), puisque K lui-même résulte de l'intersection d'un intervalle de (D1 avec un intervalle de 432 . La certitude de K" est liée à celle de K, par retrait de b. Finalement K' n K" n'est certain que jusqu'à : t - sup (Cert(ch1), Cert(ch2)) ù b = t ù (sup (Cert(cD1), Cert(cD2 )) + b). D'où Cert(cl?1 U[a,b] cI32) = sup (Cert(ED1), Cert(ch2)) + b. Pour les autres formules, la fonction Cert s'explique par des raisonnements analogues. Principe de continuation Du principe de certitude précédemment développé, découle le principe de continuation qui gouverne les algorithmes détaillés ci-avant de calcul des listes de validité. Supposons que la liste de validité d'une formule (13 ait été établie jusqu'à t ù Cert(cD) (sa zone de certitude est [0, t-Cert(cI))] ). Par définition ceci assure que la liste de validité de cl) sur [0, t-Cert(cD)] ne peut être modifiée par la suite. Cette portion est donc un résultat acquis qui ne doit plus être recalculé par la suite. Si donc arrive un nouvel instantané portant la date t', le calcul des intervalles pour c rie doit porter que sur la fenêtre dite de continuation : ] t ù Cert(cD), t' ù Cert(cD) ] Il s'agit donc de prolonger les résultats acquis sur [0, t-Cert(ED)] par un calcul sur ] t - Cert(cD), t' - Cert(cD) ] de sorte que in fine le résultat est obtenu sur [ 0, t'-Cert(cD) ] qui est bien l'intervalle de certitude de 1 sachant que le dernier instantané porte la date t'. C'est ce qui est désigné dans ce contexte, par principe de continuation. Sur le plan algorithmique, à chaque formule cl) sont associées deux variables : • une variable de type réel positif, initialisée à zéro. Appelons cette variable cD.crt pour une formule O. • une variable de type intervalle, initialisée à vide. Appelons cette variable (D.w pour une formule (D. C'est cette seconde variable qui représente la fenêtre de continuation de (D. Lorsque l'instantané I est rafraichi, de date I.t, la fenêtre de continuation c.w de cl) se calcul ainsi : • Si 1.w est vide o Si I.t ù Cert(c) >_ 0 alors cD.w devient : [0, I.t ù Cert(0) ] o Sinon c.w reste l'intervalle vide • Si i.w n'est pas vide alors c.w devient :] t.crt, I.t ù Cert(cD) ] • Affecter à 1.crt la valeur (I.t ù Cert(cl))) Afin de rendre optimal le calcul de la liste de validité d'une formule (D sur sa fenêtre de continuation, il s'agit de déterminer, dans les sous-formules de cl), quels intervalles sont susceptibles de générer de nouveaux intervalles dans cette fenêtre de continuation de (D. C'est l'objet de la notion de zone d'influence que de cibler seulement ces intervalles. Notion de zone d'influence Cette notion intervient dans l'objet de l'invention, à deux titres : • Elle définit, pour une formule 0, quels intervalles des sous-formules de ont une influence sur la fenêtre de continuation (D.w de (D définie précédemment, • Réciproquement, elle définit, pour une formule 0, quels intervalles des sous-formules de (D n'ont plus d'influence que sur la zone déjà certaine de • Ceci permet donc : o D'optimiser le calcul en ligne des intervalles de validité, en ne ciblant que les intervalles qui influent sur la fenêtre de continuation. o De manière duale, ceci permet de définir les intervalles qui ne peuvent plus avoir d'influence sur les fenêtres de continuation, et donc d'éliminer ces intervalles comme il a été illustré à la figure 8A. Là encore l'opérateur F[a,b] est particulièrement intuitif pour présenter ce principe avant sa généralisation à tout opérateur. La figure 8A illustre la zone d'influence pour F[a,b] (D. Dans cette figure 8A, le dernier instantané porte la date t' tandis que le précédent portait la date t. La fenêtre de continuation de F[a,b] est donc ] t û Cert(F[a,b] (D), t' û Cert(F[a,b] (t') ]. Les premières dates sur la valeur de (D qui influent sur la fenêtre de continuation de F[a,b]ED sont donc les dates supérieures à t - Cert(F[a,b] (D) + a tandis que la dernière qui influe sur cette fenêtre de continuation est t' - Cert(F[a,b] D) + a. Autrement dit il s'agit de la fenêtre de continuation de F[a,b] 43 décalée de a dans la futur soit ] t û Cert(F[a,b] cl)) + a, t' û Cert(F[a,b] 0) +a ] que l'on notera ] t û Cert(F[a,b] (D), t' û Cert(F[a,b] (D) ] O+ a. En posant w = ] t û Cert(F[a,b] (D), t' û Cert(F[a,b] (D) ], la zone d'influence de (D sur F[a,b] (D, obtenue, eu égard à la fenêtre de continuation w est donc w C+ a. Ceci peut s'exprimer sous forme d'une fonction à trois arguments, la fonction ZI (pour Zone d'Influence) : ZI((D, F[a,b] (D, w) = w O+ a. La généralisation à toutes les formules est donnée par la définition inductive ci-dessous de la fonction ZI((D,`P, w) (ZI pour � Zone d'Influence �, w pour désigner la fenêtre ou en anglais � window �) qui définit la zone d'influence de toute formule (D sur une sur-formule `P (donc supposée construite sur (D) et un intervalle de continuation w (de `P). Pour 'P une formule, (D une sous-formule directe de If, ZI((D,IF,w) est un intervalle tel que : un intervalle de la liste de validité de (D a une influence sur la fenêtre de continuation w de `P si et seulement si il a une intersection non vide avec ZI((D,`P,w). Pour définir ZI la notation [u,v] E) r qui dénote l'intervalle [u+r,v+r] est utilisée. • ZI(c,ùi(D, w) = w 15 • Zl((D1 , ((D1 n 1132 ), w) = Zl((D2 , ((D1 n (D2 ),W) = w • ZI(4, (F[a,b] (D), w) = w O+ a • ZI(4, (P[a,b] (D), w) = w (-b) • ZI(b, (P[a,>] (D), w) = w O (-a) • Zl((D1, ((DI U[a,b] (D2), W) = ZI(c2, ((D1 U[a,b] (D2), W) = W 0 a 20 • ZI(ED1, ((D1 S[a,b] (D2 ), W) = ZI(c2, ((D1 S[a,b] c2 ), W) = W (-b) • ZI(41, ((D1 S[a,>] ), w) = Zl((D2, ((D1 S[a,>] (D2 ), w) = w o (-a) Calcul en ligne, par continuation, des listes de validité Le principe de la continuation en ligne est le suivant. Pour chaque formule le 25 procédé ne produit de nouveaux intervalles que sur sa fenêtre propre de continuation. Ces nouveaux intervalles sont calculés à partir des listes de validité des sous-formules, mais en ne considérant que les intervalles dont l'intersection est non vide avec la zone d'influence calculée au moyen de la fonction ZI. Ces restrictions étant faites, le calcul proprement dit est alors 30 réalisé selon les principes du calcul hors ligne (ainsi que décrit dans la section Correspondance entre opérateurs logiques et opérations sur les listes de validité). Pour synthétiser : le calcul en ligne est une succession de calculs hors ligne locaux restreints pour chaque formule à sa fenêtre de continuation propre. Remarque : pour que ce calcul soit correct il est nécessaire que, pour toute formule, quelle que soit la zone d'influence qui lui est attribuée, celle-ci soit incluse dans sa zone de certitude propre. Or cela est toujours le cas. Ceci se démontre à partir des définitions des fonctions Cert et ZI. Le calcul par continuation peut là encore être facilement illustré pour F[a,b] (D. II s'agit de ne considérer que les intervalles de la liste de validité de (D situés dans la zone d'influence calculée pour F[a,b] (1). Etant donné que ces intervalles ont plus de chance d'être à la fin de la liste de validité de 1 l'algorithme procède par marche arrière. II remonte la liste de validité de 4 à partir de la fin jusqu'à déterminer le dernier et le premier intervalle ayant une intersection non vide avec la zone d'influence. Ceci définit une sous liste de la liste de validité de 1 qui est exploitée selon l'algorithme hors ligne décrit plus haut pour le calcul de nouveaux intervalles de la liste de validité de F[a,b] (D. Pour chaque production nous calculons son intersection avec la fenêtre de continuation de F[a,b]c. Si elle n'est pas vide elle est ajoutée à la liste de validité de F[a,b] 43• Le principe de continuation présente néanmoins des particularités pour les opérateurs Pua,>i et Sla,>i. Pour une formule de type F'[a,>]c il suffit que (D soit vraie une fois à une date t pour que P[a,>] (D soit vraie sur [t+a, +oo[. Le procédé peut donc être simplifié. Dès que la liste de validité de Pia,>j (D est non vide, l'unique intervalle de cette liste est ensuite systématiquement étendue sur sa borne supérieure (qui devient donc t-Cert(P[a,>] 0) à chaque calcul local), sans se préoccuper de la valeur de O. Pour S[a,>], d'après la sémantique de cet opérateur, le procédé doit examiner la valeur de vérité de (D2 arbitrairement loin dans le passé et donc aussi celle de (DI. Mais cette approche obligerait à conserver en mémoire tous les intervalles de (D2 et de (DI. De sorte que la mémoire requise par le moniteur pourrait croitre indéfiniment. Or un des objectifs de la présente invention est que la mémoire requise par le moniteur soit bornée. En réalité la définition posée précédemment ZI((EDi S[a,>i (D2 ),w) = w O+ (-a) convient car l'information que (D2 a été vraie est conservée dans la liste de validité de (D, Spa,>i ct)2. En effet en considérant le calcul de (DI S[a,>] 02 sur sa fenêtre de continuation w = ]u,v] ; si le dernier intervalle de la liste de validité de Cel SEa,>i (D2 est tel que sa borne supérieure est u alors cela signifie qu'il a existé dans la ou les fenêtre(s) précédente(s) de continuation, un intervalle i de (D, ayant intersecté un intervalle de (D2 dans le passé et qui se prolongeait au moins jusqu'à u. Si lors du calcul de (D1 Sia,>j (D2 sur w le procédé trouve dans la liste de validité de (DI un intervalle qui contient u, cela signifie qu'il prolonge i sans interruption, et que donc il prolonge la validité de t1 S[a,>] 02. La mémoire que 02 a été vraie est donc contenue dans le dernier intervalle de la liste de validité de (DI Spa,>i 02. Il n'est donc pas nécessaire de faire remonter la zone d'influence au temps O. Le faire remonter de a permet en revanche de capturer tout intervalle de (D2 pouvant initier un début de validité de (DI Sia,>] 02 sur w. Pour synthétiser, le calcul par continuation de la liste de validité d'une formule peut être décrit par l'algorithme CALCUL_LV __W suivant (qui est une modification de CALCUL_LV vu précédemment). Là encore il s'agit d'un algorithme récursif (qui s'appelle lui-même). CALCUL LV W((D) : { 1. Si (D est une proposition ou une formule purement booléenne, calcul de la liste de validité selon l'algorithme propre à ce type de formule. 2. Sinon identifier l'opérateur de la formule (, • Appel de CALCUL_LV W(c,) où est la première sous- formule directe de (D, • Si J possède une deuxième sous-formule directe (l'opérateur est binaire) appel de CALCIJL_LV W(cD2), • Calcul des zones d'influences afférentes aux sous-formules directes de (D (calcul de ZI((1, cl), c.w) ; calcul de ZI((D2, c.w) si l'opérateur est binaire), où ^t).w est la fenêtre de continuation de c (calculée comme expliqué dans la section Principe de continuation), • Composition, conformément à l'opérateur de ( (comme expliqué dans la section Correspondance entre opérateurs logiques et opérations sur les listes de validité), des intervalles des sous-formules directes de 1 situés dans les zones d'influences calculées précédemment et troncature de chaque intervalle produit à c.w la fenêtre de continuation de O. } 15 Zone d'influence et élimination des intervalles inutiles illustrés à la fiqure 8A, 8B Il a été exposé ci-dessus comment calculer la liste de validité de la formule principale. Ce calcul repose sur le calcul préalable des listes de validité de toutes ses sous-formules. Ce calcul sur les sous-formules apparaît donc 20 comme un moyen et non comme une fin en soi puisque seule la liste de validité de la formule principale est déterminante pour le procédé (car c'est la non vacuité de cette liste qui témoigne de l'occurrence du comportement redouté). Si cl> est la formule principale, que t est la date portée par le dernier instantané, nous savons que sur [0, t û Cert(41))] le calcul de la liste de 25 validité de est certain c'est-à-dire ne peut plus être modifié quoiqu'il advienne. Ainsi les intervalles des sous-formules qui ne peuvent impacter, au niveau de la formule principale, que la zone [0, t û Cert((D)] ne peuvent plus apporter d'information nouvelle déterminante. Ainsi ils sont inutiles. Il s'agit donc de les éliminer de la mémoire. Pour cela il faut être capable de 10 déterminer, pour chaque sous-formule, en deçà de quelle date les intervalles peuvent être éliminés. Pour la formule principale (D, cette date d'inutilité est donc, en valeur absolue : t û Cert(0). En effet, si des intervalles dans [0, t û Cert((D)] ont été obtenus par le procédé, l'hypothèse suivante peut être émise : ces intervalles ont été exploités (pour émettre un signal d'alarme ou un signal de régulation du système...). Ayant été exploités, ils ne sont plus utiles. Etant donnée la date d'inutilité fixée pour la formule principale, la date d'inutilité des sous-formules se détermine récursivement. Le cas de la conjonction est particulièrement intuitif (Figure 8B). Si la date d'inutilité de ((D1 A I2) est t, il est clair que les intervalles i, de (DI et i2 de 12, qui sont tous deux antérieurs à t, ne peuvent que contribuer à former un intervalle dans la zone d'inutilité de ((DI A CM. Ils sont donc eux-mêmes inutiles. Il en serait de même de tout autre intervalle antérieur à t. En somme, si t est la date d'inutilité de ((DI A 42) alors la date d'inutilité de (DI et de cD2 est aussi t. Cependant, si ((DI A C2) n'est pas la formule principale, il se peut que tI et (D2 soient sous-formules d'autres formules. Il se peut donc que d'autres formules leurs imposent une date d'inutilité antérieure à t. Ainsi, ce qui peut être affirmé est qu'à partir de ((DI A 02) et de sa date d'inutilité t, les dates d'inutilité de (D, et de (D2 doivent être inférieures à t. Une généralisation de ceci à toutes les formules du langage est explicitée ci-après. Pour généraliser, le procédé va prendre en compte les contraintes que doit satisfaire une fonction pour être une fonction d'inutilité avec dans l'idée qu'une fonction d'inutilité prend en argument une formule en supposée être une sous-formule d'une formule principale (D, et renvoi un nombre réel r, de telle sorte que la date absolue d'inutilité de (Dn soit : Date d'inutilité de la formule principale + r En relatif, par rapport à la date d'inutilité 4d; de la formule principale, la date so d'inutilité de en est donc r. Etant donnée une formule c et l'ensemble {(D,, ..., cä} de ses sous-formules une fonction Dl de {(DI, ..., cn, (13} R est une fonction d'inutilité si elle est telle que toutes ces contraintes sont vérifiées : • Dl(*) = 0 (0 pour la formule principale) Et pour i,j e [1,n] 15 En pratique, la fonction retenue sera celle qui attribue la valeur la plus grande possible pour chaque sous-formule, de sorte à pouvoir éliminer le 20 plus grand nombre d'intervalles possibles. Il s'agit en fait de choisir la plus grande valeur donnée par la contrainte la plus forte. Par exemple, si, pour une formule (D;, la plus forte contrainte est DI((D;) DI(P[a,b] (D;) ù b, alors le choix pour la fonction est DI(cD;) = DI(P[a,b] (D;) ù b. Etant donné ce choix de la fonction Dl, il est possible d'écrire que la date 25 absolue d'inutilité propre d'une sous-formule (D; de la formule principale est : Borne inférieure de c.w + DI(ci) L'élimination des intervalles inutiles consiste à supprimer, pour chaque sous-30 formule (D; de la formule principale (D, les intervalles de sa liste de validité • DI(ci) 5 DI(ù,(D;) • Dl((D;) Dl((Di n (Di) • DI(EDi) Dl((Di A (Di) • DI(cD;) 5 DI(F[a,b] (Di) + a Dl((D;) DI(P[a,b] (Di) ù b • DI((D;) DI(P[a,>] (D;) ù a DI(cD;) DI(ED; U[a,b] (Di) + a Dl((Di) DI((D;U[a,b] (Di) + a • DI(cDi) DI(cDi S[a,b] (Di) ù b • Dl((D,) Dl((Di S[a,b] (Di) ù b • DI(cD;) 5 Dl((Di Sia,>] (Di) ù a • Dl(cDi) Dl((Di S[a,>] (Di) ù a strictement antérieurs à sa date absolue d'inutilité propre (un intervalle est strictement antérieur à une date si tous ses points sont inférieurs, au sens des nombres réels, à cette date). Le mécanisme d'élimination des intervalles devenus inutiles permet notamment de garantir que la ressource mémoire requise par le moniteur soit bornée assurant de ce fait le fonctionnement sans limite de durée du moniteur généré par le procédé. Exemple d'application du procédé pour la surveillance d'un système masse-ressort ~o La figure 9 illustre un exemple d'application pratique au contrôle du comportement d'un système masse-ressort. Une masse M se déplaçant sans frottement sur un plan horizontal est reliée à un support vertical S par un ressort R et un système d'amortissement A. Plusieurs propriétés peuvent être analysées par le procédé selon l'invention, lors d'une simulation de ce 15 modèle. Par exemple, une propriété attendue pourrait être que la force f et le déplacement x varient toujours dans le même sens. Autrement dit, ce qui est redouté est la proposition (df.dx 0) est rétablie entre 0.2 et 0.5 secondes plus tard. Autrement dit la propriété attendue est (df.dx _ 0) globalement mais on tolère que (df.dx 0.5)). Pour résumer, les propriétés envisagées pour générer des moniteurs pour ce modèle pourraient être : • df.dx 0.5) Pour illustrer de façon plus complète le procédé, nous allons étudier son déroulement en considérant la propriété (df.dx représenté sous la forme d'un tableau. Ce tableau possède notamment une colonne � Liste de validité � qui permet de visualiser les listes de validité pour chaque sous-formule. 1er instantané : ({ (df.dx Pour les formules purement booléennes le calcul se base sur l'algorithme direct. C'est pourquoi la fenêtre de continuation n'est pas mentionnée. Pour chaque formule sa date d'inutilité est donnée par Cert(ED) (où b est la formule principale, à savoir (df.dx Fenêtre Date d'Inutilité : Liste de validité de continuation Borne inférieure 4.w + DI(~,) (df.dx Le procédé et le système selon l'invention présentent notamment les avantages suivants : Un procédé automatique : le moniteur est calculé automatiquement à partir de l'expression du comportement redouté et le fonctionnement du moniteur est automatique en fonctionnement normal. Il est de fait rapide et peu coûteux en mémoire. Le procédé peut s'appliquer à tout modèle, contrairement aux approches types preuve ou model-checking qui analysent le modèle tel qu'il est défini dans sa structure interne. Le moniteur ne s'intéresse qu'aux exécutions d'un système, à ses productions observables. Que le modèle soit, dans sa structure interne, très simple ou très complexe, de petite ou de grande taille, cela est sans incidence pour le moniteur généré, puisqu'il ne dépend pas de la structure du modèle mais uniquement de la formule donnée en entrée. L'analyse est effectuée en ligne, ce qui signifie que : • La surveillance du processus est réalisée pendant que le processus d'exécution/simulation se produit, • La surveillance est opérée sans limite de durée, • La surveillance se fait sans stockage de l'exécution, • La mémoire consommée par le moniteur est bornée (ce qui permet une surveillance sans limite de durée) Le procédé selon l'invention ne suppose par de régularité particulière sur l'exécution, le délai entre deux observations pouvant être quelconque.15 REVENDICATIONS1. ù Procédé permettant de générer un détecteur de comportements redoutés spécifiés en logique temporelle linéaire métrique d'un système dont le comportement est à surveiller caractérisé en ce qu'il comporte au moins les étapes suivantes mises en oeuvre par un processeur : • définir des variables caractéristiques du système à surveiller, • définir un certain nombre de propositions p sur ces variables, • allouer en mémoire du détecteur un espace suffisant pour mémoriser 1 o un instantané I relatif à ces propositions, • définir une formule principale (p, construite sur lesdites propositions p, traduisant un comportement redouté en utilisant un langage composé d'opérateurs logiques et d'opérateurs temporels portant sur le futur et le passé, 15 • de façon régulière ou périodique faire l'acquisition de la valeur des variables caractéristiques du système observé et mémoriser la date de cette acquisition, • en fonction des valeurs des variables caractéristiques issues de l'acquisition réalisée à l'étape précédente, évaluer les propositions p 20 rafraîchir l'instantané i en conséquence et attribuer à I la date d'acquisition mémorisée, • pour chaque rafraîchissement de l'instantané I: o calculer la fenêtre de continuation Ow de la formule principale et les fenêtres de continuation respectives de toutes ses 25 sous-formules au moyen d'une fonction Cert définie comme une fonction qui pour toute formule (D' passée en argument renvoie un nombre réel tel que [0, t-Cert( ] O I (13) Où ( (Dl U[a,b] CD2 101 S[a.b] S[a,>] CD2 I P[a,b] 1 I • p dénote tout symbole de proposition • a et b sont des réels positifs tels que b ? a + L'opérateur -, est la négation 15 • L'opérateur A est appelé conjonction • L'opérateur F[a,b] porte sur le futur entre a et b • L'opérateur Pta,bl porte sur le passé entre ùb et -a • L'opérateur P[a,>] porte sur le passé entre 0 et -a • L'opérateur U[a,b] porte aussi sur le futur entre a et b et la 20 permanence d'une propriété entre temps + L'opérateur S[a,b] porte sur le passé entre ùb et -a et la permanence d'une propriété entre temps • L'opérateur S[a,>] porte aussi sur le passé entre 0 et -a et la permanence d'une propriété entre temps. 25 3 ù Procédé selon la revendication 1 caractérisé en ce que l'étape d'appel de l'algorithme récursif CALCUL_LV_W sur une proposition ou une formule purement booléenne p, comporte au moins les étapes suivantes : à toute proposition ou formule purement booléenne p est associée une 30 variable booléenne p.val,si 1 est l'instantané, I.t correspond à la date portée par I et I.p à la valeur de vérité que I attribue à p, initialiser (20) les valeurs de p.val et de p.Lv, respectivement à faux et à liste vide, attendre le rafraichissement de l'instantané I (21), tester ensuite (22) la valeur de vérité [p: Si l.p est à vrai le procédé teste, étape (23), la valeur de p.val : Si p.val est à vrai alors, étape (24), le procédé prolonge le dernier intervalle de p.Lv jusqu'à l.t compris (intervalle fermé sur la ~o valeur I.t). Si p.val est à faux alors, étape (25), le procédé ajoute à la fin de p.Lv le nouvel intervalle [l.t, I.t]. Si I.p est à faux, alors le procédé teste la valeur de p.val ; Si p.val est à vrai , étape (26), alors le procédé prolonge le 15 dernier intervalle de p.Lv jusqu'à l.t non compris (ouvert sur l.t ) (étape 28). Si p.val est à faux, alors le procédé laisse p.Lv inchangé (étape 27). à la suite des étapes (24, 25, 27 et 28), affecter à p.val la valeur actuelle 20 de 1.p (29), puis puis retourner à l'étape (21) d'attente de rafraichissement de I, le calcul se prolongeant tant que le procédé est maintenu en fonctionnement. 4 ù Procédé selon la revendication 1 caractérisé en ce que l'appel de 25 l'algorithme récursif CALCUL_LV_W sur une formule qui n'est ni une proposition ni purement booléenne est fondée sur une opération propre à chaque opérateur, permettant de composer les listes de validité. 30 5 ù Procédé selon la revendication 1 caractérisé en ce que la fonction de certitude s'exprime selon la formule cl) de la manière suivante :• Cert(P) = 0 si (D est une proposition • Cert(û,O) = Cert((D) • Cert(CI)1 A 4)2) = sup (Cert(cD1), Cert(cD2)) • Cert(F[a,b] (D) = Cert((D) + b 5 • Cert(c1 U[a,b] (D2) = sup (Cert((D1), Cert�2) ) + b • Cert(P[a,b) d)) = Cert((D) û a • Cert (P[a,>] (D) = Cert() û a • Cert((D1 S[a,b] 4)2) = sup (Cert(((D1), Cert(( 2)) • Cert�1 S[a,>]) = sup (Certtci), Cert�2)) 10 6 û Procédé selon la revendication 1 caractérisé en ce que le calcul de la fenêtre de continuation (D.w de la formule principale (D et de toutes ses sous-formules comporte au moins les étapes suivantes : associer à chaque formule principale ou sous-formule deux variables, 15 initialiser à zéro la 1 ère variable, de type réel positif, appelée c.crt pour une formule (D, initialiser à vide la seconde variable, de type intervalle, appelée qui est la fenêtre de continuation de GD, rafraichir l'instantané I, de date I.t, 20 calculer la fenêtre de continuation ID.w de (D: Si GD.w est vide si I.t û Cert((D) 0 alors (D.w devient : [0, I.t Cert(*) ] si I.t û Cert((D) ] ci)), w) = wO (-a) • Zl((D1, (~1 U[a,bi 02), w) = ZI((2, (!(D1 U[a,b] ~2), w) = w G a • Zl(~1, (~1 S[a,b] ), w) = 3(02, ((Di S[a,b] (1)2 ), w) = w CD, (-b) • ZI(EI)1, ((D1 S[a,>] q)2 ), w) = Zl(cJ)2, (~1 S[a,>] (2 ), w) = w O (-a). 8 ù Procédé selon l'une des revendications 1 à 7 caractérisé en ce qu'il comporte en plus les étapes suivantes : • fixer la date d'inutilité cDd; de la formule principale à la borne inférieure de sa fenêtre de continuation l.w, • attribuer à chaque sous-formule Ql)n de la formule principale sa date d'inutilité propre qui est égale à (1)di + DI(cl)n) soit la somme de la date fixée pour la formule principale et de la valeur renvoyée par une fonction d'inutilité Dl appliquée à con, • éliminer, pour toute formule (formule principale et toutes ses sous-formules), les intervalles de sa liste de validité propre qui sont antérieurs à sa date d'inutilité propre. 9 ù Procédé selon la revendication 1 caractérisé en ce qu'il attribue comme date d'inutilité à la formule principale la borne inférieure de sa fenêtre de continuation et en ce que la date d'inutilité de toute sous-formule {01, ..., c~~} d'une formule principale (1) vaut la somme de la date attribuée à la formule principale cl) et de la valeur calculée à l'aide de la fonction d'inutilité Dl laquelle doit satisfaire toutes les contraintes suivantes : • Dl((J) = 0 (0 pour la formule principale)• DI(O;) DI(-e;) • Dl(cD;) 5 DI((D; n 0]) • Dl�]) DI(cD; A (D]) • DI(t;) ] ù a • De;) 5 Dl((; U[a,b] (D]) + a • Dl(cD]) ] 4]) ù a • DI((D]) ] (D]) ù a 10 ù Procédé selon la revendication 1 caractérisé en ce que le signal émis est un signal déclenchant une alarme et/ou un signal de déclenchement 20 d'une commande pour contrôler un processus, ou encore l'émission d'un rapport signalant l'anomalie détectée. 11 ù Système permettant de générer un détecteur de comportements redoutés spécifiés en logique temporelle linéaire métrique, à mémoire 25 bornée, caractérisé en ce qu'il comporte au moins les éléments suivants : Une entrée recevant un ou plusieurs paramètre(s) caractéristique(s) de l'état du système à surveiller, et une horloge H indiquant la date d'acquisition de ce(s) paramètre(s), Et pour i,j e [1,n] 5 10 la fonction d'inutilité Dl retenue est celle qui choisit pour chaque sous-formule i5 la plus grande la valeur permise par la contrainte la plus forte, afin de pouvoir éliminer le plus grand nombre d'intervalles possible.• Un processeur adapté à exécuter les étapes du procédé selon l'une des revendications 1 à 10 en utilisant le(s) paramètre(s) mesuré(s) et la date associée, • Une mémoire (14) adaptée à o mémoriser l'instantané courant o mémoriser les listes de validité LV déterminées par la mise en oeuvre du procédé pour la formule principale et ses sous-formules, • Une sortie (16) émettant un signal S correspondant aux informations io contenues dans la liste de validité pour la formule principale et émettre ledit signal. 12 û Système selon la revendication 11 caractérisé en ce qu'il comporte un dispositif d'affichage piloté par le signal correspondant aux informations 15 contenues dans la liste de validité pour la formule principale. 13 û Système selon la revendication 11 caractérisé en ce que le signal obtenu est transmis à un dispositif de génération d'une alarme et/ou à un système de contrôle ou de régulation du système placé sous la surveillance 20 d'un moniteur généré selon le procédé selon l'une des revendications 1 à10. 25