Les travaux de recherche développés dans cette thèse, définissent une approche d'évolution d'ontologie Onto-Evoal (Ontology Evolution-Evaluation) qui s'appuie sur une modélisation de patrons de gestion de changement CMP (Change Management Patterns). Ces patrons spécifient des classes de changements, des classes d'incohérences et des classes d'alternatives de résolution. Sur la base de ces patrons et des relations sémantiques entre eux, un processus automatisé permettant de conduire l'application des changements tout en maintenant la cohérence de l'ontologie évoluée a été développé. L'approche intègre également une activité d'évaluation basée sur un modèle de qualité d'ontologie qui a été défini. Ce modèle est employé pour guider la gestion des incohérences en évaluant l'impact des résolutions proposées sur le contenu et l'usage de l'ontologie à travers un ensemble de métriques quantitatives et ce, afin de choisir une résolution qui préserve la qualité de l'ontologie évoluée. La gestion des changements étant fortement liée au modèle dans lequel est représentée l'ontologie, nous nous sommes focalisés sur le langage OWL en tenant compte de l'impact des changements sur la cohérence logique de l'ontologie telle que spécifiée dans la couche OWL DL. Les principales contributions de l'approche résident dans la modélisation des patrons de gestion de changement guidant le processus d'évolution, l'intégration de l'évaluation de la qualité pour optimiser la résolution des changements et la modélisation formelle et explicite du journal d'évolution.

En Génie Automatique, le GRAFCET [IEC 848] est couramment employé pour la modélisation de la dynamique des systèmes à événements discrets, en raison de ses capacités de modélisation et de son ergonomie. Cependant, il lui est reproché de ne pas être défini de manière suffisamment formelle pour que tous les grafcets établis soient sans ambigüité et puissent être validés. L'objectif des travaux est double : contribuer à la formalisation du GRAFCET de manière à renforcer ses fondements théoriques et offrir à tout analyste les moyens nécessaires pour valider une modélisation exprimée en GRAFCET en vérifiant les propriétés des modèles et leur comportement par rapport à leurs entrées/sorties. Le GRAFCET étant une machine d'état complexe - essentiellement à cause des parallélismes importants qu'il permet de décrire - nous proposons à l'analyste d'utiliser le graphe des situations accessibles, ou grafcet d'état équivalent pour valider sa spécification. Nous avons conçu une technique de génération automatique du graphe des situations accessibles d'un grafcet global (qui est un automate fini «équivalent»), de manière à pouvoir établir un ensemble de preuves et propriétés sur la cohérence intrinsèque du grafcet et sur sa pertinence par rapport au cahier des charges. Une algèbre de Boole, dans laquelle la notion de fronts a été formalisée par deux opérateurs unaires a été construite. Les 14 propriétés qui ont été démontrées ont permis d'établir un module de calcul symbolique utilisé pour tenir compte de l'historique des évolutions des entrées. Nos travaux intègrent les extensions du modèles GRAFCET. Pour valider notre approche, une maquette informatique en C a été développée et permet de calculer l'automate équivalent au grafcet à valider. Nous utilisons pour vérifier certaines propriétés l'outil MEC développé pour l'étude des systèmes de transitions. Deux exemples de validation de grafcets par analyse de leur automate sont donnés dans le mémoire.

Dans une première partie, nous montrons qu'il est possible d'établir une correspondance naturelle entre les preuves en déduction naturelle de la validité d'une formule et les réfutations par resolution d'un ensemble de clauses obtenues en appliquant a la négation de cette formule une mise sous forme clausale non standard utilisant une technique de renommage. En particulier, nous montrons qu'il est possible de simuler le fonctionnement d'un calcul des sequents proche de celui de Gentzen par la resolution et nous montrons comment traduire des réfutations par resolution en preuve en déduction naturelle. De plus, nous proposons plusieurs ameliorations de cette mise sous forme clausale avec renommage permettant de faciliter la recherche d'une réfutation par resolution. Dans une deuxième partie, nous décrivons en détail des techniques permettant une mise en œuvre efficace de la resolution avec sortes ordonnées ainsi qu'un principe d'indexation des clauses permettant de résoudre efficacement de nombreux problèmes-clés (tels ceux poses par la subsomption, l'utilisation de systèmes de réécriture...). Ces algorithmes ont ete utilises dans l'implémentation d'un démonstrateur par resolution que nous avons réalisé dans le cadre d'atinf

Parmi les nouveaux nano-dispositifs, les CNTFETs sont des candidats prometteurs. Mais les circuits à base de nanotubes auront une probabilité élevée de défectuosité lors de la fabrication et une assez grande dispersion des caractéristiques. Dans ce contexte, cette thèse étudie l'implantation de portes logiques élémentaires à base de CNTFETs. Une comparaison précise de plusieurs structures logiques montre les avantages de la structure complémentaire pour les applications futures. L'influence des variations paramétriques sur les caractéristiques des CNTFETs et des portes logiques complémentaires est ensuite analysée. Une étude synthétique des défauts et fautes transitoires spécifiques aux circuits à base de CNTFETs est présentée. Enfin, une structure logique redondante est proposée pour réduire l'effet des dispersions paramétriques et pour améliorer le rendement de fabrication en tolérant certains défauts.

Méthodologie générale pour réaliser des circuits logiques décrits par leur comportement. On traite 1) la machine séquentielle qui est assimilée à la réalisation d'un algorithme ; 2) la modélisation de la partie operative où l'on présente un modèle pour en déduire un ensemble de primitives. réalisation des éléments de base, des charges externes des portes, de la partie operative. Etude du dessin.

.

.

De nombreux travaux ont montré l'importance de l'interpolation de Craig pour la structuration et la modularité des spécifications de type axiomatique. En vue d'en donner des conditions suffisantes dans un cadre théorique adapté à l'informatique, nous nous sommes intéressé à une propriété équivalente à l'interpolation de Craig dans le cadre de la théorie standard des modèles : la consistance de Robinson. L'étude de cette dernière propriété nous a amené à généraliser dans une spécialisation des institutions les notions classiques de diagrammes complets et de morphismes élémentaires. Ceci nous a alors permis de généraliser quelques résultats classiques de théorie des modèles tels que les théorèmes de Löwenheim-Skolem ou l'union de chaînes de Tarski. En fin, les constructeurs de formules étant explicites dans notre cadre théorique, nous nous sommes naturellemant intéressés à la combinaison de logiques et à la préservation de l'interpolation de Craig et de la consistance de Robinson.

Les technologies électroniques actuelles offrent la possibilité de réaliser des systèmes sur puce (SoC). Les méthodologies doivent s'adapter à ce nouveau cadre de conception afin de tirer profit des capacités que présentent les SoC.<br />Dans ce contexte, le thème émergent de radio logicielle a pour rôle de répondre à une diversité de fonctionnalités et de standards de télécommunication sans fil à l'aide d'une interface matérielle unique.<br /><br />L'objet de cette thèse est d'élaborer des méthodologies et des outils contribuant au dimensionnement et à la synthèse systématique d'un module analogique/numérique dédié à des applications radio logicielle.<br />Les aspects modélisation et prototypage d'une tête de réception mixte constituent les principales contributions de ce travail. Un exemple de dimensionnement d'une tête de réception mixte répondant aux standards GSM et UMTS est développé. La simulation globale de ce système ainsi que son implémentation matérielle sont proposées.

Dans cette thèse, on présente un cadre théorique général d'analyse statique pour l'inférence de propriétés `structurelles' ou d'`usage' des programmes. Le terme `structurel', emprunté à la théorie de la démonstration, suggère un rapport étroit avec la logique linéaire, où les règles structurelles de contraction et affaiblissement jouent un rôle important. Le problème de l'analyse statique consiste à trouver une traduction d'un langage source dans le style de PCF vers un langage comportant des annotations structurelles. On montre que l'on peut characteriser l'ensemble de traductions possibles comme des solutions d'un ensemble d'inequations appropriées. Plus particulièrement, on s'intéresse à la plus petite solution, qui correspond à la traduction la plus précise ou optimale. La plus grande partie de ce manuscrit de thèse est dédié à un seul cas d'étude, l'analyse linéaire, dont l'objectif est de déterminer les valeurs qui sont utilisées une seule fois. On decrit d'abord une version de l'analyse linéaire très simplifiée, en suite on introduise des extensions qui comportent des notions de sous-typage et du polymorphisme d'annotations, ce étant clé dans la pratique, car il permet à l'analyse de garder son pouvoir expressif en présence de modules compilés séparément.