Reproduction de : Thèse de doctorat : Acoustique : Le Mans : 2008. / Titre provenant de l'écran-titre. Bibliogr. p. 167-176.

Thèse doctorat : Optoélectronique : Ecully, Ecole centrale de Lyon : 2006. / 368 réf.

Thèse doctorat : Optoélectronique : Ecully, Ecole centrale de Lyon : 2006. / Titre provenant de l'écran-titre. 368 réf.

Thèse de doctorat : Génie Electrique : Villeurbanne, INSA : 2000. / Titre provenant de l'écran-titre. Bibliogr. p. 187-197.

Reproduction de : Thèse de doctorat : Microondes et Microtechnologies : Lille 1 : 2004. / N° d'ordre (Lille 1) : 3594. Résumé en français et en anglais. Titre provenant de la page de titre du document numérisé. Bibliogr. à la suite de chaque chapitre.

Résumé non communiqué / Résumé non communiqué

Dans cette thèse, on étudie des problèmes liés à la vérification de systèmes (logiciels). On s’intéresseplus particulièrement à la conception sûre de procédures de décision utilisées en vérification. De plus, onconsidère également un problème de modularité pour un langage de modélisation utilisé dans la plateformede vérification Why.De nombreux problèmes de vérification peuvent se réduire à un problème de satisfaisabilité modulodes théories (SMT). Pour construire des procédures de satisfaisabilité, Armando et al. ont proposé en2001 une approche basée sur la réécriture. Cette approche utilise un calcul général pour le raisonnementéquationnel appelé paramodulation. En général, une application équitable et exhaustive des règles ducalcul de paramodulation (PC) conduit à une procédure de semi-décision qui termine sur les entréesinsatisfaisables (la clause vide est alors engendrée), mais qui peut diverger sur les entrées satisfaisables.Mais ce calcul peut aussi terminer pour des théories intéressantes en vérification, et devient ainsi uneprocédure de décision. Pour raisonner sur ce calcul, un calcul de paramodulation schématique (SPC)a été étudié, en particulier pour prouver automatiquement la décidabilité de théories particulières etde leurs combinaisons. L’avantage de ce calcul SPC est que s’il termine sur une seule entrée abstraite,alors PC termine pour toutes les entrées concrètes correspondantes. Plus généralement, SPC est unoutil automatique pour vérifier des propriétés de PC telles que la terminaison, la stable infinité et lacomplétude de déduction.Une contribution majeure de cette thèse est un environnement de prototypage pour la conception etla vérification de procédures de décision. Cet environnement, basé sur des fondements théoriques, estla première implantation du calcul de paramodulation schématique. Il a été complètement implanté surla base solide fournie par le système Maude mettant en oeuvre la logique de réécriture. Nous montronsque ce prototype est très utile pour dériver la décidabilité et la combinabilité de théories intéressantes enpratique pour la vérification.Cet environnement est appliqué à la conception d’un calcul de paramodulation schématique dédié àune arithmétique de comptage. Cette contribution est la première extension de la notion de paramodulationschématique à une théorie prédéfinie. Cette étude a conduit à de nouvelles techniques de preuveautomatique qui sont différentes de celles utilisées manuellement dans la littérature. Les hypothèses permettantd’appliquer nos techniques de preuves sont faciles à satisfaire pour les théories équationnellesavec opérateurs de comptage. Nous illustrons notre contribution théorique sur des théories représentantdes extensions de structures de données classiques comme les listes ou les enregistrements.Nous avons également contribué au problème de la spécification modulaire pour les classes et méthodesJava génériques. Nous proposons des extensions du language de modélisation Krakatoa, faisant partiede la plateforme Why qui permet de prouver qu’un programme C ou Java est correct par rapport à saspécification. Les caractéristiques essentielles de notre apport sont l’introduction de la paramétricité à lafois pour les types et les théories, ainsi qu’une relation d’instantiation entre les théories. Les extensionsproposées sont illustrées sur deux exemples significatifs: tri de tableaux et fonctions de hachage.Les deux problèmes traités dans cette thèse ont pour point commun les solveurs SMT. Les procéduresde décision sont les moteurs des solveurs SMT, et la plateforme Why engendre des conditions devérification dérivées d’un programme source annoté, qu’elle transmet aux solveurs SMT (ou assistants depreuve) pour vérifier la correction du programme.Mots-clés: / In this thesis we address problems related to the verification of software-based systems. We aremostly interested in the (safe) design of decision procedures used in verification. In addition, we alsoconsider a modularity problem for a modeling language used in the Why verification platform.Many verification problems can be reduced to a satisfiability problem modulo theories (SMT). In orderto build satisfiability procedures Armando et al. have proposed in 2001 an approach based on rewriting.This approach uses a general calculus for equational reasoning named paramodulation. In general, afair and exhaustive application of the rules of paramodulation calculus (PC) leads to a semi-decisionprocedure that halts on unsatisfiable inputs (the empty clause is then generated) but may diverge onsatisfiable ones. Fortunately, it may also terminate for some theories of interest in verification, and thusit becomes a decision procedure. To reason on the paramodulation calculus, a schematic paramodulationcalculus (SPC) has been studied, notably to automatically prove decidability of single theories and oftheir combinations. The advantage of SPC is that if it halts for one given abstract input, then PC haltsfor all the corresponding concrete inputs. More generally, SPC is an automated tool to check propertiesof PC like termination, stable infiniteness and deduction completeness.A major contribution of this thesis is a prototyping environment for designing and verifying decisionprocedures. This environment, based on the theoretical studies, is the first implementation of theschematic paramodulation calculus. It has been implemented from scratch on the firm basis provided bythe Maude system based on rewriting logic. We show that this prototype is very useful to derive decidabilityand combinability of theories of practical interest in verification. It helps testing new saturationstrategies and experimenting new extensions of the original (schematic) paramodulation calculus.This environment has been applied for the design of a schematic paramodulation calculus dedicated tothe theory of Integer Offsets. This contribution is the first extension of the notion of schematic paramodulationto a built-in theory. This study has led to new automatic proof techniques that are different fromthose performed manually in the literature. The assumptions to apply our proof techniques are easyto satisfy for equational theories with counting operators. We illustrate our theoretical contribution ontheories representing extensions of classical data structures such as lists and records.We have also addressed the problem of modular specification of generic Java classes and methods.We propose extensions to the Krakatoa Modeling Language, a part of the Why platform for provingthat a Java or C program is a correct implementation of some specification. The key features arethe introduction of parametricity both for types and for theories and an instantiation relation betweentheories. The proposed extensions are illustrated on two significant examples: the specification of thegeneric method for sorting arrays and for generic hash map.Both problems considered in this thesis are related to SMT solvers. Firstly, decision procedures areat the core of SMT solvers. Secondly, the Why platform extracts verification conditions from a sourceprogram annotated by specifications, and then transmits them to SMT solvers or proof assistants to checkthe program correctness.

De l'automobile à l'aéronautique en passant par le biomédical, tout domaine d'applications utilise des capteurs dont certains sont à sortie fréquentielle. L'arrivée de nouveaux matériaux piézoélectriques a ouvert une porte vers des applications inaccessibles jusqu'à lors et essentiellement à hautes températures. L'orthophosphate de gallium est l'un de ces nouveaux matériaux piézoélectriques ayant de plus un fort facteur de couplage. Ce mémoire porte sur l'étude et la réalisation de capteurs en orthophosphate de gallium fonctionnant en ondes de volumes. La première partie consiste à étudier la sensibilité et stabilité thermique en élaborant un modèle analytique de poutre vibrant en élongation, flexion et torsion. Au cours de cette partie est démontrée l'existence de coupes compensées en température pour ces différents modes. Cette étude théorique est ensuite complétée par une analyse utilisant la méthode des éléments finis (MEF). La réalisation de résonateurs dans diverses orientations cristallographique est effectuée, dont celles compensées en températures. Les mesures associées à ces structures sont confrontées aux résultats théoriques. Vient ensuite l'application d'un biocapteur fonctionnant en cisaillement d'épaisseur. Un modèle éléments finis est élaboré pour étudier l'influence de certains paramètres sur le comportement du capteur. Une comparaison entre le modèle établi et les mesures expérimentales est également présentée. Ces résultats positifs ouvrent des perspectives d'évolution décrites en conclusion.

L’Histoire des écoles d’horlogerie de Besançon est inhérente à la naissance et à la continuité d’une industrie spécifique très localisée sur un territoire. Avec elles nous partons de l’ère « proto-industrielle » qui plonge ses racines dans les idéaux révolutionnaires de 1793 pour aboutir aux bouleversements technologiques de l’électronique et du « quartz » des années 1970… S’inscrivant sur la longue durée, trois « écoles » vont se succéder. Pour répondre aux attentes d’une industrie horlogère qui doit constamment faire face aux évolutions techniques, chacune à sa manière, va innover pour constituer un « corpus » original de formation qui n’est pas sans bousculer les rites et usages du temps. Si les deux premières « écoles » eurent une durée de vie limitée, la dernière entité, née en 1861 de la volonté municipale, va pendant plus d’un siècle, accompagner toute une ville (et sa région) dans sa réussite industrielle. Dès sa création, et au fur et à mesure des adaptations qu’elle a su mettre en place, par la qualité et la spécificité des formations dispensées, elle va irriguer de ses élèves toute une industrie toujours à l’affût de personnels qualifiés. Au plan national elle va diffuser le nom de Besançon comme « capitale française de l’horlogerie » en formant nombre d’horlogers-rhabilleurs tenant boutiques et autres ateliers de réparation par tout le territoire… Elle va servir de référence pour implanter dans la Cité des laboratoires de recherche et d’enseignement supérieur : un Observatoire chronométrique, une École d’ingénieurs, un Centre d’études horlogères et de développement industriel (Cétéhor)… Elle va contribuer à la diversification industrielle de la ville dans des domaines connexes à l’horlogerie, notamment dans le découpage, la micromécanique, l’appareillage et les microtechniques… Nationalisée en 1891, elle fait dès lors partie de la petite élite des Écoles Nationales Professionnelles (par assimilation), qui vont marquer le développement industriel du Pays. En 1933, quand elle intègre ses nouveaux locaux, par le nombre et l’originalité de ses filières (de l’ouvrier qualifié à l’ingénieur), par sa dotation en matériels modernes, elle est signalée comme étant le « premier établissement de l’enseignement technique » en France. Le cheminement de cette dernière école fait aussi ressortir une histoire « humaine », « prosopographique », qui met en exergue les nombreux anciens élèves qui se sont lancés avec grande réussite dans la création d’entreprises. Restés fidèles à leur école, ils ont contribué au renom et au développement de la richesse économique de la cité et de sa région… Avec ces écoles d’horlogerie, on aborde enfin l’histoire de l’Enseignement Technique en France. Pour répondre à la demande d’une industrie horlogère en pleine croissance qui déplorait les carences de l’apprentissage en atelier, elles ont été pionnières en ouvrant la voie de « la scolarisation » de la formation professionnelle. Par leurs innovations pédagogiques, et soutenues par les Anciens Élèves, elles ont su établir un lien « École-Entreprise » des plus fructueux qui marque encore la mémoire collective des Bisontins…En 1974 elle perd toute référence à l’horlogerie pour devenir le Lycée Jules Haag. Le temps de l’histoire est désormais advenu pour tenter de comprendre ce qui a fait la force et la réussite de ces « Écoles d’horlogerie » dans leur participation active, sur la durée, à la prospérité économique et industrielle d’une ville et de sa région… / The history of the watchmaking schools in Besançon is part of the birth and continuous development of a specific industry in a very limited sector of the French territory. When studying those schools we start at the « protoindustrial » time with its roots in the revolutionary ideals of 1793 and end up with the technological upheavals of electronics and the « quartz » technology in the 1970s. Three « schools » followed one another over the long term. Each school aimed at satisfying the demands of a watchmakng industry confronted to rapidly changing technical evolutions ; so it innovated in its own way by creating an original « corpus » in the students training and most of the time upset the practices and common ideas of the time. If the first two « schools » had a limited lifespan, the last one created in 1861 by the town council itself has been supporting the industrial growth of the city and the surrounding region. Since its foundation it has stuck to the industrial reality by placing the emphasis on high standards and opening new specific branches whenever necessary, thus answering the needs of firms always looking for highly qualified staff. For a large number of French people Besançon became the « capital town of the watchmaking industry » thanks to the shops or repair workshops kept by Besançon-trained former students all over France… It served as a background to set up research and university laboratories in the city : Observatoire Chronométrique, Ecole d’Ingénieurs, Centre d’Etudes Horlogères et de Développement Industriel (Cétéhor)… It contributed to the industrial diversification of the town in fields related to watchmaking such as mechanical cutting, micromechanics, equipment and microtechniques. It was nationalized in 1891 and then belonged to the very small elite goup of the Professional National Schools that influenced the future industrial development of the country. In 1933 it moved into sparkling-new premises and was acknowledged as the flagship of technical education in France : it offered a large number of innovating courses ranging from the skilled worker to the engineer and was granted the latest equipments in every field. The path of this new school also enhanced a « humane » and « prosopographical » history ; it highlighted the part played by the numerous former students who created their own successful businesses. Being faithful to their old school they contributed to the renown and economic growth and prosperity of the city and its region… Beyond the local impact we must regard the history of the watchmaking schools as an important part of the history of Technical Education in France. To meet the needs of a soaring watchmaking industry they opened the way to the transfer of professional training from apprenticeship in workshops with its observed shortcomings to education in technical high schools. Their pedagogical innovations, the strong support of their former students created a vital school-business link that still lives on in the collective memory of the town inhabitants.In 1974 its name changed to Lycée Jules Haag thus losing any reference to watchmaking. Let us now try and understand the strong influence and success of those watchmaking schools, the active part they played in the economic industrial prosperity of a town and its surrounding region…