Les activités de validation et vérification de modèles sont devenues essentielles dans le développement de systèmes complexes. Les efforts de formalisation de ces activités se sont multipliés récemment étant donné leur importance pour les systèmes embarqués critiques. Notre travail s’inscrit principalement dans cette voie. Nous abordons deux visions complémentaires pour traiter cette problématique. La première est une description syntaxique implicite macroscopique basée sur une ontologie pour aider les concepteurs dans le choix des outils selon leurs exigences. La seconde est une description sémantique explicite microscopique pour faciliter la construction de techniques de vérification compositionnelles. Nous proposons dans la première partie de cette thèse une ontologie pour expliquer et expliciter les éléments fondateurs du domaine que nous appelons VVO. Cette ontologie pourra avoir plusieurs autres utilisations : une base de connaissance, un outil de formation ou aussi un support pour le choix de la méthode à appliquer et l’inférence de correspondance entre outils. Nous nous intéressons dans la seconde partie de cette thèse à une formalisation dans un assistant à la preuve de l’introduction de composants dans un langage de modélisation et des liens avec les activités de validation et vérification. Le but est d’étudier la préservation des propriétés par composition : les activités de vérification sont généralement coûteuses en terme de temps et d’effort, les faire d’une façon compositionnelle est très avantageux. Nous partons de l’atelier formel pour l’Ingénierie Dirigée par les Modèles Coq4MDE. Nous suivons la même ligne directrice de développement prouvé pour formaliser des opérateurs de composition et étudier la conservation des propriétés par assemblage. Nous nous intéressons au typage puis à la conformité de modèles par rapport au métamodèle et nous vérifions que les opérateurs définis permettent de conserver ces propriétés. Nous nous focalisons sur l’étude d’opérateurs élémentaires que nous exploitons pour spécifier des opérateurs de plus haut niveau. Les préconditions des opérateurs représentent les activités de vérification non compositionnelles qui doivent être effectuées en plus de la vérification des composants pour assurer la postcondition des opérateurs qui est la propriété souhaitée. Nous concluons en présentant des perspectives pour une formalisation algébrique en théorie des catégories. / The validation and verification of models have become essential in the development of complex systems. The formalisation efforts for these activities have increased recently being given their importance for critical embedded systems. We discuss two complementary visions for addressing these issues. The first is a syntactic implicit macroscopic description based on an ontology to help designers in the choice of tools depending on their requirements. The second is a microscopic explicit semantics description aiming to facilitate the construction of compositional verification techniques. We propose in the first part of this thesis an ontology to explain and clarify the basic elements of the domain of Verification and Validation that we call VVO. This ontology may have several other uses: a knowledge base, a training tool or a support for the choice of the method to be applied and to infer correspondence between tools. We are interested in the second part of this thesis in a formalisation using a proof assistant for the introduction of components in a modelling language and their links with verification and validation activities. The aim is to study the preservation of properties by the composition activities. The verification are generally expensive in terms of time and efforts, making theme in a compositional way is very advantageous. Starting from the formal framework for Model Driven Engineering COQ4MDE, we follow the same line of though to formalize the composition operators and to study the conservation of properties by composition. We are interested in typing and conformity of models in relation with metamodels and we verify that the defined operators allow to preserve these properties. We focus on the study of elementary operators that we use to specify hight level operators. The preconditions for the operators represent the non-compositional verification activities that should be performed in addition to verification of components to ensure the desired postcondition of the operator. We conclude by studying algebraic formalisation using concepts from category theory.

Ces dernières années, les engins robotisés n’ont cessé d’améliorer leur autonomie dans le domaine de la décision. Désormais, pour ne citer que l’exemple de véhicules aériens, nombre de drones sont largement capables, sans intervention d’un opérateur humain, de décoller, suivre un itinéraire en activant divers capteurs à des moments précis, atterrir en un lieu spécifié, suivre une cible, patrouiller sur une zone... Une des étapes suivantes consiste à faire collaborer une équipe de véhicules autonomes, de nature hétérogène (aériens, terrestres, marins...) afin de leur permettre d’accomplir des missions plus complexes. L’aspect dynamique de l’environnement réel, la non disponibilité à tout instant des moyens de communication, la coordination nécessaire des véhicules,de conceptions parfois différentes, dans l’exécution de certaines parties d’un plan de mission, sont autant d’obstacles à surmonter. Ce travail tente non seulement d’apporter quelques éléments de réponse face à ces difficultés, mais consiste aussi en la mise en place concrète d’un superviseur haut niveau, capable de gérer l’exécution d’une mission par une équipe de véhicules autonomes hétérogènes, où le rôle de l’opérateur humain est volontairement réduit. Nous décrivons dans ce mémoire l’architecture distribuée que nous avons choisi de mettre en œuvre pour répondre à ce problème. Il s’agit d’un superviseur, réparti à bord des véhicules autonomes, interfacé avec leur architecture locale et en charge de l’exécution de la mission d’équipe. Nous nous intéressons également à la formalisation des connaissances nécessaires au déroulement de cette mission, afin d’améliorer l’interopérabilité des véhicules de l’équipe, mais aussi pour expliciter les relations entre modèles décisionnels abstraits et réalité d’exécution concrète. Le superviseur est capable de réagir face aux aléas qui vont se produire dans un environnement dynamique. Nous présentons ainsi dans un second temps les stratégies mises en place pour parvenir à les détecter au mieux, ainsi que la façon dont nous procédons pour réparer partiellement ou totalement le plan de mission initial, afin de remplir les objectifs initiaux. Nous nous basons notamment sur la nature hiérarchique du plan de mission, mais aussi sur celle de la structure de sous-équipes que nous proposons de construire. Enfin, nous présentons quelques résultats obtenus expérimentalement, sur des missions simulées et des scénarios réels, notamment ceux du Programme d’Etudes Amont Action dans lequel s’inscrivent ces travaux de thèse. / Many autonomous robots with specific control oriented architectures have already been developed worldwide.The advance of the work in this field has led researchers wonder for many years to what extent robots would be able to be integrated into a team consisting of autonomous and heterogeneous vehicles with complementary functionalities. However, robot cooperation in a real dynamic environment under unreliable communication conditions remains challenging, especially if these autonomous vehicles have different individual control architectures.In order to address this problem, we have designed a decision software architecture, distributed on each vehicle.This decision layer aims at managing execution and at increasing the fault tolerance of the global system. The mission plan is assumed to be hierarchically structured. ln case of failure detection, the plan repair is done as locally as possible, based on the hierarchical organization.This allows us to restrict message exchange only between the vehicles concerned by the repair process. Knowledge formalisation is also a part of the study permitting the improvement of interoperability between team members. It also provides relevant information all along mission execution, from initial planning computation to plan repair in this multirobot context. The feasibility of the system has been evaluated by simulations and real experiments thanks to the Action project (http://action.onera.fr/welcome/).

Le vieillissement actuel de la population provoque un accroissement de problèmes dans les systèmes de santé, dont une pénurie de personnel médical pour les soins à domicile. Le vieillissement de la population a également pour effet d'augmenter le nombre de personnes avec troubles cognitifs. Les comportements incohérents induits par les symptômes des troubles cognitifs limitent la capacité de ces personnes à réaliser leurs activités de la vie quotidienne (AVQ). L'un des axes de recherche prometteurs de cette problématique est l'amélioration et le maintien de la qualité de vie des personnes avec troubles cognitifs dans leurs domiciles. Pour répondre à cette problématique, plusieurs laboratoires de recherche, dont le laboratoire de DOmotique et d'informatique Mobile de l'Université de Sherbrooke (DOMUS), explorent les différents moyens de soutenir, à l'intérieur d'un habitat intelligent, un occupant avec troubles cognitifs dans l'accomplissement de ses AVQ. Cette approche s'inscrit dans le récent courant de pensée issu de l'intelligence ambiante, qui fait référence à une tendance où les environnements sont enrichis avec des technologies (capteurs, effecteurs et autres dispositifs interconnectés par un réseau), dans le but de concevoir un système pouvant planifier une assistance ponctuelle aux occupants en fonction des informations recueillies et de l'historique des données accumulées. L'une des difficultés majeures inhérentes à ce contexte est la reconnaissance et la prédiction des comportements anormaux lorsque les occupants effectuent leurs AVQ à l'intérieur d'un habitat intelligent. Cette thèse vise à contribuer à l'amélioration du processus de reconnaissance de comportements d'un occupant avec troubles cognitifs. Notre proposition consiste en une approche de reconnaissance et prédiction de comportements fondée sur une formalisation des actions basée sur la théorie des possibilités, une alternative à la théorie des probabilités. Les actions sont inférées à partir de l'état actuellement observé de l'habitat intelligent obtenu grâce aux évènements envoyés par les capteurs présents dans l'appartement, lesquelles peuvent fournir une information incomplète et imparfaite. À partir de la séquence d'actions observées plausibles, l'approche proposée utilise une formalisation des activités en structure de plans d'actions pour inférer le comportement observé de l'occupant. Cette approche est en mesure de considérer les comportements erronés, où l'occupant effectue de façon erronée certaines activités tandis que d'autres peuvent être effectuées de façon cohérente, et les comportements cohérents, où l'occupant effectue une ou plusieurs activités de façon cohérente. Les hypothèses sur le comportement observé sont ensuite utilisées pour déterminer les opportunités d'assistance que l'habitat intelligent peut offrir. L'approche proposée a été implémentée et validée au sein de l'infrastructure du projet"Ambient Intelligence for Home-based Elderly Care" à l'"Institute for Infocomm Research" de Singapour et présente des résultats prometteurs pour des scénarios de cas réels effectués dans l'infrastructure. Le développement d'un habitat intelligent capable de maintenir et d'améliorer la qualité de vie des personnes avec troubles cognitifs permettrait de diminuer le fardeau des aidants naturels et professionnels, facilitant le choix des ces personnes de rester à domicile. Ce type de technologie pourrait constituer une solution viable aux problèmes des systèmes de santé associés au vieillissement de la population. De plus, ce type d'approche peut également être utilisé dans des contextes où les comportements anormaux et les situations à risque doivent être évités comme, par exemple, dans le domaine de l'aviation.

Dans ce mémoire, des approches contribuant à l'évaluation de la performance d'un barrage sont proposées. Les développements portent sur : -une méthode d'évaluation déterministe de la performance des barrages par recueil, formalisation et agrégation de différentes sources de connaissances ; -une base de connaissances sur les phénomènes de dégradation des barrages permettant la capitalisation des connaissances du domaine ; -une méthode d'analyse des imperfections ; -une méthode non déterministe d'évaluation de la performance qui procède par représentation des imperfections et leur propagation dans le modèle. Ces différentes méthodes ont conduit à trois outils informatiques : une interface d'aide à l'évaluation de la performance, un système de traçabilité des données et une base de connaissances sur les phénomènes de dégradation. Ces approches sont illustrées sur les barrages en remblai et plus spécifiquement le mécanisme d'érosion interne

Les travaux développés dans ce mémoire concernent la formalisation d'un processus sûr d'automatisation en vue de maîtriser la complexité induite par l'intégration de plus en plus importante de technologies de l'information et de la communication au cœur même des processus de production et des produits. Plus précisément, notre travail porte sur l'intégration d'approches méthodologiques, issues du Génie Automatique, et de modèles formels, issus du Génie Informatique et de l'Automatique des Systèmes à Evénements Discrets afin de garantir, a priori, le respect des exigences formulées par les utilisateurs. Notre contribution porte sur deux axes. Le premier concerne l'intégration de techniques de synthèse de la commande dans un processus d'automatisation, incluant les phases de modélisation et de génération d'un code implantable, et leur application à la reconfiguration de systèmes manufacturiers contrôlés par le produit. Le second est basé sur le raffinement formel ou semi-formel de modèles pour identifier et structurer les exigences exprimées à un niveau " système " puis les allouer et les projeter sur une architecture de fonctions, de composants ou d'équipements. Ces travaux ont été initiés dans le cadre de notre thèse en réponse aux besoins de R&D industriels de la Direction des Etudes & Recherche d'EDF, puis ont été poursuivis avec une cible relative aux systèmes manufacturiers et validés dans le cadre de collaborations industrielles variées.

Cette thèse aborde trois thèmes : la formalisation de la virologie informatique, l'élaboration de protections contre l'auto-reproduction et le problème de la détection des programmes malicieux. Nous proposons une formalisation s'appuyant sur les fondements de l'informatique théorique et sur les travaux fondateurs de la discipline. Nous obtenons un formalisme souple où le théorème de récursion prend le rôle d'un compilateur de virus informatiques. Ce théorème trouve alors la place qui lui manquait encore dans la théorie de la programmation. Ce formalisme nous fournit des bases suffisamment solides pour étudier de nouvelles stratégies de protection. Dans un premier temps nous nous intéressons aux relations qu'entretiennent auto-reproduction et capacités de calcul afin d'identifier un modèle raisonnable où l'auto-reproduction est impossible. Ensuite nous exposons deux stratégies construite sur la complexité de Kolmogorov, un outil de l'informatique théorique reliant la sémantique et la syntaxe concrète d'un langage de programmation. Le thème de la détection comporte deux parties. La première traite de la difficulté de la détection des virus informatiques : nous identifions les classes de la hiérarchie arithmétique correspondant à différents scénarios d'infections informatiques. La seconde partie aborde des aspects plus pratiques en décrivant l'architecture d'un détecteur de programmes malicieux conçu durant cette thèse. Ce prototype utilise une détection morphologique, l'idée est de reconnaître la forme des programmes malicieux en utilisant des critères syntaxiques et sémantiques / This dissertation tackles three topics: the formalization of the computer virology, the construction of protections against self-reproduction and the issue of malware detection. We propose a formalization that is based over computer science foundations and over the founder works of the discipline. We obtain a generic framework where the recursion theorem takes a key role. This theorem is seen as computer virus compiler, this approach provides a new programming perspective. The sound basis of this framework allows to study new protection strategies. First, we analyze the relations between the notion of self-reproduction and the computation capabilities. We aims at identifying a reasonable model of computation where self-reproduction is impossible. Then we propose two defense strategies based on the Kolmogorov complexity, a tool which relates the semantics to the concrete syntax of programming languages. We treat the issue of malware detection in two steps. First, we study the difficulty related to the detection of several scenarios of computer infection. Second, we present a malware detector that was designed during the thesis. It is based on a morphological detection which allies syntaxical and semantical criteria to identify the shapes of malware

Cette thèse s'articule autour de la gestion de ressources explicites dans les langages fonctionnels, en mettant l'accent sur des propriétés de calculs avec substitutions explicites raffinant le lambda-calcul. Dans une première partie, on s'intéresse à la propriété de préservation de la beta-normalisation forte (PSN) pour le calcul lambda s. Dans une seconde partie, on étudie la propriété de confluence pour un large ensemble de calculs avec substitutions explicites. Après avoir donné une preuve générique de confluence basée sur une série d'axiomes qu'un calcul doit satisfaire, on se focalise sur la métaconfluence de lambda j, un calcul où le mécanisme de propagation des substitutions utilise la notion de multiplicité, au lieu de celle de structure. Dans la troisième partie de la thèse on définit un prisme des ressources qui généralise de manière paramétrique le lambda-calcul dans le sens où non seulement la substitution peut être explicite, mais également la contraction et l'affaiblissement. Cela donne un ensemble de huit calculs répartis sur les sommets du prisme pour lesquels on prouve de manière uniforme plusieurs propriétés de bon comportement comme par exemple la simulation de la beta-réduction, la PSN, la confluence, et la normalisation forte pour les termes typés. Dans la dernière partie de la thèse on montre différentes ouvertures vers des domaines plus pratiques. On s'intéresse à la complexité d'un calcul avec substitutions en premier lieu. On présente des outils de recherche et on conjecture des bornes maximales. Enfin, on finit en donnant une spécification formelle du calcul lambda j dans l'assistant à la preuve Coq.

Cette thèse s'inscrit dans le cadre de la génération automatique de Langue des Signes Française et plus particulièrement la génération des Gestes Non Manuels (GNM). La génération nécessite une description précise des GNM. Actuellement, nous ne disposons que de notations de nature symbolique. Nous proposons une nouvelle méthodologie d'annotation permettant une description fine et précise des mouvements, tout en tenant compte de la structure temporelle des GNM. Cette méthodologie comporte une annotation qualitative et une annotation quantitative. Nous avons appliqué notre méthodologie aux mouvements des sourcils et aux clignements des yeux et obtenons ainsi des données numériques et symboliques à partir desquelles nous menons l'analyse. Celle-ci permet de dégager une typologie de ces mouvements. Pour chaque catégorie nous précisons son rôle, l'emplacement du mouvement par rapport aux signes avoisinants et sa structure. Nous formalisons chacune des catégories pour une génération ultérieure et proposons des perspectives de poursuites de l'étude.

Plusieurs raisons conduisent aujourd'hui à la nécessité de concevoir une pièce «fabricable» avec le moins de modification et le plus rapidement possible. Nous pouvons citer l'évolution et la mondialisation du marché, la réduction de la taille des séries et des délais de conception comme de réalisation, le fait que le coût d'un produit soit engagé à 80 % au niveau de la conception. C'est dans ce cadre qu'interviennent les outils et les méthodes de l'ingénierie intégrée. Les travaux de cette thèse se positionnent plus précisément au niveau de la formalisation et de l'exploitation des liens qui existent entre le produit et le processus de fabrication. Une démarche a été définie afin d'encadrer la conception progressive de la pièce et de son processus de fabrication. Un outil venant en support à cette démarche a été spécifié. Deux pistes ont été abordées lors du développement de l'outil pour la façon de représenter et d'exploiter les connaissances : un premier formalisme utilisant une ontologie associée à un traitement par classification ou bien un second formalisme basé sur une représentation arborescente des processus de fabrication associée à un traitement par élagage. Cette dernière représentation est nommée « schéma de processus de fabrication ». Un cas d'étude est présenté afin de valider la démarche proposée en utilisant l'outil support. Ces travaux ont été appliqués à la forge en tenant compte des spécificités de ce domaine de fabrication (notamment la nécessité d'une considération plus globale de la pièce par rapport à l'usinage)

Les transformateurs de puissance sont des éléments clés des systèmes électriques. Leurs défaillances sont très coûteuses, principalement à cause de la non-disponibilité du service électrique qu'elles entraînent. L'évaluation rapide et précise de défauts internes des transformateurs est en conséquence un facteur clé d'une exploitation efficace et sûre. Un tel diagnostic est généralement établi par un expert humain qui fait corréler différents types d'informations telles que des résultats d'essais électriques ou chimiques, le déclenchement de protections ou l'historique de l'appareil... Cette thèse présente une méthode d'aide au diagnostic de défauts originale qui reprend, en les formalisant, la démarche et la capitalisation d'expérience de l'expert. Les informations disponibles sur le transformateur à étudier sont mises en correspondance avec le système proposé de manière systématique. Des hypothèses de défaut sont alors formulées et un degré de confiance calculé pour chacune d'elle. Pour améliorer la confiance en certaines de ces hypothèses la méthode recherche, et propose, de renseigner des informations utiles pouvant améliorer le diagnostic. Il progresse ainsi jusqu'à ce que la confiance d'au moins une hypothèse soit suffisante pour l'utilisateur. Le système peut de plus évoluer efficacement dans le temps en prenant facilement en compte de nouveaux types d'essais ou de nouvelles informations pouvant être discriminants dans un diagnostic, et ainsi améliorer les diagnostics futurs automatiquement.