La caractérisation sismique des réservoirs pétroliers nécessite l'intégration de plusieurs techniques telles que la lithosismique, la géomodélisation, la géostatistique, l'utilisation des algorithmes évolutionnaires et la pétrophysique. L'information sismique est d'abord utilisée pour la description de l'architecture externe des réservoirs car son utilisation pour la description des faciès ne se fait pas sans difficultés. L'objectif de cette thèse est d'apporter des outils nouveaux pour aider à l'utilisation de l'information sismique pour caractériser les réservoirs.<br />Un premier travail a consisté à évaluer l'impact des incertitudes structurales sur les inversions pétroélastiques et les conséquences en terme de classification de faciès. Ensuite, nous considérons la modélisation sismique comme aide à l'évaluation du modèle réservoir. Cette modélisation permettra de faire le lien entre les simulateurs réservoir ou les géomodeleurs et la réponse sismique du réservoir. <br />Nous développons ensuite deux approches alternatives aux méthodes traditionnelles en inversion pétroélastique et pétrophysique. La première utilise la méthode géostatistique des déformations graduelles pour créer des réalisations de propriétés réservoirs. Elle permet de créer des propriétés à l'échelle réservoir, conditionnées aux puits, tout en respectant une fonction coût basée sur la comparaison des données sismiques réelles et issues de ces réalisations. <br />La seconde méthode repose sur le principe de la classification supervisée et utilise des réseaux de neurones pour analyser la forme des traces sismiques. Une première étape consiste à générer un volume d'apprentissage contenant tous les modèles pétrophysiques envisageables pour un champ donné. Ces modèles sont analysés par les réseaux de neurones. Les neurones ainsi identifiés sont appliqués aux données réelles, pour identifier des relations pétrophysique/sismique identiques aux données d'apprentissage.<br />Toutes les méthodologies sont validées sur plusieurs réservoirs choisis pour leurs particularités géologiques (complexité structurale, lithologie du réservoir).

La conception de systèmes embarqués nécessite de plus en plus l'utilisation d'outils logiciels afin de contenir la complexité croissante de ceux-ci. Les deux principaux outils industriels dans ce domaine sont Simulink et Lustre/Scade. Ces deux outils possèdent de nombreuses fonctionnalités comme un moteur de simulations, des générateurs de tests ou de code. Cependant, Simulink est, dans la majorité des cas, utilisé pour la conception de systèmes embarqués et ceci parce qu'il a une expressivité plus importante. Il est capable de modéliser et de simuler des systèmes à temps continu, à temps discret et un mélange des deux, c'est-à-dire des systèmes hybrides. Pour la conception des systèmes embarqués, Simulink permet de modéliser l'environnement physique et le logiciel embarqué dans un même formalisme. L'application des méthodes formelles sur de telles spécifications est un défi industriel et scientifique important pour la validation des logiciels embarqués. De plus, l'utilisation de méthodes formelles, au plus tôt dans le cycle de développement, est un challenge essentiel dans l'industrie afin de réduire les coûts liés à la correction de bogues.<br /><br />Dans cette thèse, nous définissons une analyse statique par interprétation abstraite de modèles Simulink. Nous appelons cette analyse Simulation Abstraite. L'objectif de la Simulation Abstraite est de fournir un critère de correction des comportements numériques des exécutions des modèles Simulink. Ces simulations sont souvent utilisées pour valider les systèmes modélisés, mais elles sont plus proches de l'activité de tests que celle de la preuve. En conséquence, elles ne permettent pas de valider vis-à-vis des spécifications un système modélisé avec Simulink. La Simulation Abstraite fournit un critère de correction dans le sens que les comportements des modèles Simulink représentent au mieux les comportements du monde réel.<br /><br />Nous supposons que le modèle mathématique, représenté par un modèle Simulink, est correcte vis-à-vis du monde réel. Notre objectif est de calculer automatiquement et conjointement une sur-approximation des comportements mathématiques et des comportements issus de la simulation numérique pour une plage d'entrées possibles. Nous sommes ainsi capable d'estimer l'ensemble des imprécisions introduit par la simulation numérique, c'est-à-dire les erreurs d'arrondi ou les erreurs de troncature liées, par exemple, aux capteurs. Le critère de correction des modèles à temps continu est obtenu en évaluant la distance séparant les résultats des méthodes d'intégration numérique, utilisées par le moteur de simulations, des résultats obtenus par une méthode d'intégration numérique garantie. Le critère de correction des modèles à temps discret est donné par l'utilisation du domaine numérique abstrait des nombres flottants avec erreurs différentiées. Ce nouveau domaine numérique est issu de la combinaison du domaine des flottants avec erreurs et la méthode de différentiation automatique permettant d'avoir une meilleure abstraction des erreurs. Nous définissons également une abstraction d'un domaine des séquences utilisant les partitions d'un ensemble. Nous sommes ainsi en mesure de représenter des simulations infinies d'une manière finie. L'ensemble de ces domaines permet alors d'estimer les erreurs introduites par les traitements numériques présents lors des simulations. Nous obtenons alors une méthode de validation des comportements numériques des systèmes embarqués modélisés en Simulink.

Cette thèse propose une méthodologie pour l'analyse des éléments grammaticaux polysémiques, notamment le pronom ON, à partir d'une réflexion sur le cadre théorique de la Sémantique de Textes. À travers des analyses de deux genres déterminés - l'article scientifique et la poésie - la thèse montre l'interaction et l'influence réciproque de ON et le contexte, aussi bien au niveau de la phrase qu'au celui du texte. <br> La première partie de la thèse traite de la sémantique de ON et de sa classification grammaticale. Elle montre les limitations des descriptions grammaticales basées sur des critères peu précis, et la confusion entre emplois indéfinis et emplois pour des personnes déterminées qui s'exprime par l'oxymoron « pronom personnel indéfini ». Par conséquent, la thèse se propose d'affiner la description sémantique de ON, notamment par une élaboration de la notion de contexte et son influence sur l'interprétation de ce pronom. La variation dans les emplois de ON ne peut pas se réduire à un seul noyau de sens (core meaning) et l'on propose un modèle sémique approprié à l'analyse de ON selon l'hypothèse que les différents emplois correspondent à la réalisation ou l'annulation des différents sèmes en contexte. <br> La seconde partie de la thèse présente deux études de l'emploi de ON dans des genres déterminés ; l'article scientifique et la poésie. La première étude examine l'emploi de ON dans un corpus d'articles scientifiques (le corpus KIAP, voir www.kiap.uib.no) et montre l'influence de paramètres contextuels aussi bien au niveau micro (verbes, temps verbaux, adverbes) qu'au niveau macro (disposition linéaire du texte). La seconde étude analyse l'emploi de ON dans L'excès - l'usine de Leslie Kaplan (1994) à partir de la notion de zones anthropiques (Rastier 1996) qui décrit les relations entre dimensions sémantiques et expériences humaines. Dans cette perspective, ON fonctionne comme un médiateur entre les différentes zones, notamment entre le sujet et le monde qui l'entoure. La flexibilité discursive de ON, allant de l'indéfini jusqu'au déterminé, constitue un facteur remarquable dans la représentation textuelle de l'aliénation du sujet dans ce texte.

Mes travaux de thèse s'articulaient autour de la validation de modèles et de programmes. En ce sens, les modèles sont validés par animation, de manière à s'assurer qu'ils décrivent le bon comportement du système qu'ils représentent. Il s'agit d'un processus semi-automatique, car l'utilisateur sélectionne les actions du système à exécuter et effectue la comparaison entre les descriptions informelles données dans le cahier des charges et les résultats produits par le modèle. Un modèle validé est ensuite utilisé dans l'objectif de produire des cas de tests fonctionnels destinés à être joués sur une implantation ou un système sous test. Le modèle formel est ainsi utilisé à deux niveaux : d'une part, il permet de calculer de manière automatique les suites de tests, et, d'autre part, il sert d'oracle pour établir le verdict du test.<br />Au cours de ces travaux, nous nous sommes intéressés à la validation de programmes Java par l'intermédiaire de son langage de modélisation associé, nommé JML. Suite aux expériences et aux savoirs-faire accumulés au sein de l'équipe Techniques Formelles et à Contraintes du Laboratoire d'Informatique de Franche-Comté, nous avons choisi d'appliquer une représentation logico-ensembliste des modèles JML, reposant sur des solveurs de contraintes pour gérer les valeurs des variables des modèles objets que nous traitons. A partir de cette représentation symbolique, nous avons exprimé l'animation symbolique d'un modèle objet basé sur la sémantique de Java, utilisant les descriptions formelles contenues dans les pré- et postconditions des spécifications des méthodes.<br />Nous nous sommes ensuite appuyés sur la définition symbolique des états du système objet pour extraire des cibles de tests, liées aux comportements issus des méthodes, définies par un prédicat obtenu par conjonction de la condition d'activation du comportement et de la mise aux limites des attributs des objets du système et des paramètres de la méthode sous test. L'animation symbolique du modèle entre en jeu pour la construction des cas de tests. Un algorithme de parcours de l'espace d'états effectue la recherche d'un chemin d'exécution menant à la cible. Les cas de tests sont ensuite concrétisés pour produire un pilote de test Java. Une étude de cas a été menée sur une modélisation fonctionnelle d'un porte-monnaie électronique.<br />Ces travaux ont été implantés dans un prototype, nommé JML-Testing-Tools, qui permet l'animation symbolique d'un modèle JML et la génération de cas de tests pour l'implantation Java qui lui est associée. Ce prototype est composé d'un compilateur traduisant une spécification JML et des signatures de classes Java dans un format logico-ensembliste. Le modèle décrit dans ce format est ensuite animé par un interpréteur rétablissant la sémantique opérationnelle du Java/JML.

Preuves de programmes et intelligence artificielle. Types. Syntaxe: état du langage, analyse syntaxique, extensions, inférence, apprentissage, performance de l'analyse syntaxique. Sémantique déductive. Utilisation-prolongements

L'étude de programmes probabilistes intéresse plusieurs domaines de l'informatique : les réseaux, l'embarqué, ou encore la compilation optimisée. C'est tâche malaisée, en raison de l'indécidabilité des propriétés sur les programmes déterministes à états infinis, en plus des difficultés provenant des aspects probabilistes.<br /><br />Dans cette thèse, nous proposons un langage de formules permettant de spécifier des propriétés de traces de systèmes de transition probabilistes et non-déterministes, englobant celles spécifiables par des automates de Büchi déterministes. Ces propriétés sont en général indécidables sur des processus infinis.<br /><br />Ce langage a à la fois une sémantique concrète en termes d'ensembles de traces et une sémantique abstraite en termes de fonctions mesurables. Nous appliquons ensuite des techniques d'interprétation abstraite pour calculer un majorant de la probabilité dans le pire cas de la propriété étudiée et donnons une amélioration de cette technique lorsque l'espace d'états est partitionné, par exemple selon les points de programme. Nous proposons deux domaines abstraits convenant pour cette analyse, l'un paramétré par un domaine abstrait non probabiliste, l'autre modélisant les gaussiennes étendues.<br /><br />Il est également possible d'obtenir de tels majorants par des calculs propageant les mesures de probabilité en avant. Nous donnons une méthode d'interprétation abstraite pour analyser une classe de formules de cette façon et proposons deux domaines abstraits adaptés à ce type d'analyse, l'un paramétré par un domaine abstrait non probabiliste, l'autre modélisant les queues sous-exponentielles. Ce dernier permet de prouver la terminaison probabiliste de programmes.<br /><br />Les méthodes décrites ci-dessus sont symboliques et ne tirent pas parti des propriétés statistiques des probabilités. Nous proposons d'autre part une méthode de Monte-Carlo abstrait, utilisant des interpréteurs abstraits randomisés.

Cette thèse s'inscrit dans la vérification automatique de propriétés <br />numériques de programmes, principalement des logiciels embarqués. Lors de la <br />vérification on doit représenter de façon finie des ensembles éventuellement <br />infinis de valeurs, pour cela une solution possible est l'utilisation de <br />polyèdres convexes. Cette <br />représentation est précise mais coûteuse ce qui limite le nombre de variables <br />qu'il est possible de manipuler. Le but de cette thèse est d'augmenter le <br />nombre maximal de variables qu'il est possible de représenter. Deux approches <br />ont été envisagées puis testées. Dans un premier temps on a voulu tirer <br />profit de la présence d'équations affines pour éliminer une variable par <br />équation. Cette approche s'est révélée, expérimentalement, assez décevante. <br />Une autre approche, bien plus prometteuse, est l'utilisation du produit <br />cartésien. L'idée est alors de représenter indépendamment les variables dont <br />l'évolution n'est pas liée. Cette décomposition peut être améliorée grâce à <br />un changement de base. Un analyseur a été réalisé afin de <br />tester ces deux approches.

Les travaux présentés se situent dans le domaine de l'aide à la décision pour la surveillance de systèmes complexes tels que les procédés chimiques. Pour de tels procédés il n'est pas toujours possible de disposer d'un modèle mathématique ou structurel du système considéré. De ce fait, d'autres types d'approches telles que les méthodes de classification, doivent être envisagées pour l'identification des états fonctionnels dans lesquels le système peut se trouver. Sur la base de telles méthodes notre travail présente une stratégie permettant de construire, à partir de données historiques et de données récupérées en ligne, un modèle discret (états/transitions) du comportement du processus et d'identifier des situations anormales issues des dysfonctionnements. Cette stratégie consiste à générer un premier modèle de référence, sous la forme d'un automate à états finis, du procédé à partir d'un apprentissage, supervisé ou non. Ce modèle est ensuite validé et complété par l'expert. La reconnaissance en ligne permet de suivre l'évolution temporelle des modes de fonctionnement déjà identifiés. Dans le cas où une transition amène à la non-reconnaissance d'un certain nombre d'éléments, c'est-à-dire à la détection d'une déviation par rapport à un comportement connu, l'objectif est de caractériser cette nouvelle situation. Pour cela, nous proposons de faire un nouvel apprentissage hors ligne prenant en compte ces éléments non reconnus. Les nouvelles classes créées permettent, toujours en interaction avec l'expert, de fixer la nature de la déviation observée. Dans le cas d'une défaillance, une analyse portant sur les descripteurs et le profil des classes permet l'isolation de la défaillance. Ces informations sont transmises à l'opérateur pour l'assister dans son diagnostic. Un outil d'aide à la décision pour la surveillance s'appuyant sur cette stratégie a été mis en place. Cet outil appelé SALSA repose sur la méthode LAMDA. Il s'agit d'une méthode de classification avec apprent issage et reconnaissance de formes qui permet l'analyse de données multi-variables et qui utilise des notions de la logique floue pour introduire le concept d'adéquation d'un élément à une classe. Dans le cadre du projet européen CHEM les principaux aspects de nos travaux et les résultats obtenus ont été illustrés sur des unités industrielles de nature différente.

Les protocoles cryptographiques jouent un rôle majeur dans les applications ou l'intégrité des données, la confidentialité, l'authenticité et autres propriétés sont essentielles. Ils sont utilisés par exemple dans le commerce électronique, la téléphonie mobile, le vote électronique. Dans la première partie de la thèse nous montrons que le problème d'atteignabilité pour des protocoles cryptographiques temporisés bornés est décidable est NP-complet. Notre procédure se base sur une logique de Hoare complète pour des protocoles cryptographiques bornés et un langage de propriétés très expressif. Dans la deuxième partie, en utilisant des techniques d'interprétation abstraite, nous appliquons cette méthode pour vérifier des propriétés de secret pour les protocoles cryptographiques dans un modèle général. Nous traitons un nombre non borné de sessions, de participants et de nonces ainsi que des messages de taille arbitraire. Nous proposons un algorithme qui calcule un invariant inductif en utilisant des patterns comme représentation symbolique. Cette méthode a été implanté dans l'outil Hermes et validée sur plusieurs études de cas.

Si l'analyse automatique des accès aux tableaux a été largement étudiée, on trouve très peu de résultats convaincants sur l'analyse du contenu des tableaux. Pour une telle analyse, les analyses numériques sont centrales. Notamment, si l'on découvre l'invariant i ≠ j, on évite d'affaiblir la connaissance sur a[j] lors d'une affectation à a[i]. Nous proposons une nouvelle analyse numérique faiblement relationnelle, combinant des contraintes de zones (x - y ≤ c ou ±x ≤ c) à des contraintes de non-égalités (x ≠ y ou x ≠ 0). Cette analyse a une complexité en O(n4), si les variables prennent leur valeurs dans un ensemble dense. Dans le cas arithmétique, décider de la satisfaisabilité d'une conjonction de telles contraintes est un problème NP-complet. Nous proposons une analyse en O(n4) également pour ce cas. Au cœur des analyses du contenu des tableaux on trouve aussi des analyses de partitionnement symbolique. Pour une boucle " for i = 1 to n ", où un tableau est accédé à la cellule i, il est nécessaire de considérer le contenu des tableaux sur les tranches [1, i - 1], [i, i] et [i + 1, n] pour être précis. Nous définissons une analyse de partitionnement sémantique, puis une analyse du contenu des tableaux basée sur ses résultats. Cette dernière associe à chaque tranche φ une propriété ψ dont les variables représentent le contenu des tableaux sur cette tranche. La propriété ψ est interprétée cellule-par-cellule, ainsi pour φ = [1, i - 1] et ψ = (a = b + 1) il est exprimé que ∀ k ∈ [1, i - 1], a[k] = b[k] + 1. Les résultats expérimentaux montrent que notre analyse automatique est efficace et précise, sur une classe de programmes simples : tableaux unidimensionnels, indexés par une variable au plus (x + c ou c), traversés par des boucles, imbriquées ou non, avec des compteurs suivant une progression arithmétique. Elle découvre par exemple que le résultat d'un tri par insertion est un tableau trié, ou que durant le parcours d'un tableau gardé par une "sentinelle", tous les accès à ce tableau sont corrects.