Ces travaux de recherche présentent un nouveau cadre formel pour intégrer le diagnostic de fautes multiples et la reconfiguration. L'idée principale est d'utiliser STRIPS (Stanford Research Institute Problem Solver), un langage formel pour la planification automatisée qui peut intégrer les relations cause_effect et le mécanisme de raisonnement automatique dans un modèle. Le processus de diagnostic de fautes multiples et son module de vérification de cohérence sont basés sur le langage STRIPS. En outre, le modèle de faute est introduit dans le module de vérification de cohérence pour empêcher les diagnostics impossibles. Le langage STRIPS peut définir qualitativement le modèle de faute, sans nécessiter une connaissance précise et détaillée des composants défaillants. A partir des résultats du diagnostic, la reconfiguration met à jour le modèle du système. Elle vérifie que le modèle permet de réaliser les objectifs à partir d’une approche basée sur la vérification de modèle. Les objectifs sont pour ceci, exprimés à l’aide une logique temporelle. / This research presents a new formal framework for integrating multi-fault diagnosis and reconfiguration. The main idea is to use the STRIPS (STanford Research Institute Problem Solver), a formal language for automated planning which can integrate the cause_effect knowledge and the automated reasoning mechanism into one model. The multi-fault diagnostic process and its consistency-checking module are all based on the models defined by STRIPS actions. Moreover, the fault models are introduced into the consistency-checking module for preventing the impossible diagnoses. The STRIPS can qualitatively define the fault models without requiring detail and precise knowledge of faulty components. According to the results of diagnosis, the reconfiguration updates the system’s model. It uses the model checking to verify whether the updated model satisfies the desired objectives. These objectives are described by a temporal language.

Mémoire numérisé par la Direction des bibliothèques de l'Université de Montréal.

Il devient important d'assurer que tout système critique est fiable. Pour cela différentes techniques existent, telles que le test ou l'utilisation de méthodes formelles. S'assurer que le comportement d'un vérifieur de byte code Java Card n'entraînera pas de faille de sécurité est une tâche complexe. L'automatisation totale de cette vérification n'à popr le moment pas été realisee. Des jeux de tests coûteux ont été produits manuellement, mais ils doivent être refaits à chaque nouvelle spécification. Les travaux présentés dans ce mémoire proposent une nouvelle méthode pour la génération automatique de tests de vulnérabilité. Ceux-ci reposent sur l'utilisation et la transformation automatique de modèles formels. Pour valider cette méthode, un outil à été développé puis utilisé sur différentes implémentations du vérifieur de byte code Java Card. Le langage de modelisation que nous avons utilisé est Event-B. Nos modèles représentent le comportement normal du système que l'on souhaite tester. Chaque instruction est modélisée comme un événement. Leur garde représente l'ensemble des conditions que doit satisfaire une instruction pour être acceptable. À partir de ce modèle initial, une succession de dérivations automatiques génère un ensemble de modèles dérivés. Chacun de ces modèles dérivés représente une faute particulière. On extrait de ces nouveaux modèles les tests de vulnérabilité abstraits. Ceux-ci sont ensuite concrétisés puis envoyés à un système à tester. Ce processus est assuré par notre logiciel qui repose sur les API Rodin, ProB, CapMap et OPAL.

Mémoire numérisé par la Direction des bibliothèques de l'Université de Montréal.

Dans cette thèse, nous établissons un modèle à deux échelles à la fois pour des matrices de cantilevers unidimensionnels et bidimensionnels en régime de fonctionnement élastodynamique avec des applications possibles aux réseaux de microscopes à force atomique (AFM). Son élaboration est basée sur une analyse asymptotique pour les structures minces élastiques, une approximation à deux échelles et une mise à l'échelle utilisée pour l'homogénéisation des milieux fortement hétérogènes. Nous complétons la théorie de l'approximation à deux échelles pour les problèmes aux limites du quatrième ordre posés dans des domaines minces périodiques connexes seulement dans certaines directions. Notre modèle reproduit la dynamique globale du support ainsi que les mouvements locaux des cantilevers. Pour simplifier la suite du travail, nous concentrons nos travaux à l'étude de matrices de leviers constituées de lignes découplées en régime dynamique. Comme le support des leviers est élastique, l'effet du couplage entre levier est pris en compte. La vérification du modèle est soigneusement réalisée. Nous montrons que chaque mode propre peut être décomposé en produits d'un mode de base avec un mode de levier. Nous présentons une méthode de discrétisation du modèle et effectuons sa vérification numérique en la comparant avec des résultats de simulation par éléments finis du problème d'élasticité tridimensionnel. Par ailleurs, nous avons élaboré de nouveaux outils d'aide à la conception de réseaux d'AFM. Une boîte à outils d'optimisation robuste est interfacée avec le modèle permettant d'optimiser un design avant micro-fabrication. Un algorithme d'estimation de l'état statique combinant la mesure de déplacements mécaniques par interférométrie et le modèle a été introduit. Nous avons également synthétisé un régulateur quadratique linéaire (LQR) pour un réseau de cantilevers en mode dynamique comprenant actionneurs et capteurs régulièrement espacées. Dans le but de mettre en oeuvre le contrôle en temps réel, nous proposons une approximation semi-décentralisée qui peut être réalisé par un circuit électronique distribué analogique. Plus précisément, notre processeur analogique peut être réalisé par un réseau périodique de résistances (PNR). La méthode d'approximation de commande est basée sur deux concepts généraux, à savoir sur un calcul fonctionnel (c'est-à-dire des fonctions d'opérateurs) et sur la formule de représentation d'une fonction d'opérateur de Dunford-Schwartz. Cette méthode d'approximation est étendue pour la résolution d'un problème de filtrage optimal robuste de type H∞ de la dynamique d'un réseau de leviers couplés avec sources aléatoires de bruit.

Les langages dédiés de modélisation (DSMLs) sont de plus en plus utilisés dans les phases amont du développement des systèmes complexes, en particulier pour les systèmes critiques embarqués. L’objectif est de pouvoir raisonner très tôt dans le développement sur ces modèles et, notamment, de conduire des activités de vérification et validation (V and V). Une technique très utilisée est la vérification des modèles comportementaux par exploration exhaustive (model-checking) en utilisant une sémantique de traduction pour construire un modèle formel à partir des modèles métiers pour réutiliser les outils performants disponibles pour les modèles formels. Définir cette sémantique de traduction, exprimer les propriétés formelles à vérifier et analyser les résultats nécessite une expertise dans les méthodes formelles qui freine leur adoption et peut rebuter les concepteurs. Il est donc nécessaire de construire pour chaque DSML, une chaîne d’outils qui masque les aspects formels aux utilisateurs. L’objectif de cette thèse est de faciliter le développement de telles chaînes de vérification. Notre contribution inclut 1) l’expression des propriétés comportementales au niveau métier en s’appuyant sur TOCL (Temporal Object Constraint Language), une extension temporelle du langage OCL; 2) la transformation automatique de ces propriétés en propriétés formelles en réutilisant les éléments clés de la sémantique de traduction; 3) la remontée des résultats de vérification grâce à une transformation d’ordre supérieur et un langage de description de correspondance entre le domaine métier et le domaine formel et 4) le processus associé de mise en oeuvre. Notre approche a été validée par l’expérimentation sur un sous-ensemble du langage de modélisation de processus de développement SPEM, et sur le langage de commande d’automates programmables Ladder Diagram, ainsi que par l’intégration d’un langage formel intermédiaire (FIACRE) dans la chaîne outillée de vérification. Ce dernier point permet de réduire l’écart sémantique entre les DSMLs et les domaines formels. / Domain specific Modeling Languages (DSMLs) are increasingly used at the early phases in the development of complex systems, in particular, for safety critical systems. The goal is to be able to reason early in the development on these models and, in particular, to fulfill verification and validation activities (V and V). A widely used technique is the exhaustive behavioral model verification using model-checking by providing a translational semantics to build a formal model from DSML conforming models in order to reuse powerful tools available for this formal domain. Defining a translational semantics, expressing formal properties to be assessed and analysing such verification results require such an expertise in formal methods that it restricts their adoption and may discourage the designers. It is thus necessary to build for each DSML, a toolchain which hides formal aspects for DSML end-users. The goal of this thesis consists in easing the development of such verification toolchains. Our contribution includes 1) expressing behavioral properties in the DSML level by relying on TOCL (Temporal Object Constraint Language), a temporal extension of OCL; 2) An automated transformation of these properties on formal properties while reusing the key elements of the translational semantics; 3) the feedback of verification results thanks to a higher-order transformation and a language which defines mappings between DSML and formal levels; 4) the associated process implementation. Our approach was validated by the experimentation on a subset of the development process modeling language SPEM, and on Ladder Diagram language used to specify programmable logic controllers (PLCs), and by the integration of a formal intermediate language (FIACRE) in the verification toolchain. This last point allows to reduce the semantic gap between DSMLs and formal domains.

Dans cette thèse, nous établissons un modèle à deux échelles à la fois pour desmatrices de cantilevers unidimensionnels et bidimensionnels en régime de fonctionnementélastodynamique avec des applications possibles aux réseaux de microscopesà force atomique (AFM). Son élaboration est basée sur une analyseasymptotique pour les structures minces élastiques, une approximation à deuxéchelles et une mise à l’échelle utilisée pour l’homogénéisation des milieux fortementhétérogènes. Nous complétons la théorie de l’approximation à deux échellespour les problèmes aux limites du quatrième ordre posés dans des domaines mincespériodiques connexes seulement dans certaines directions. Notre modèle reproduitla dynamique globale du support ainsi que les mouvements locaux des cantilevers.Pour simplifier la suite du travail, nous concentrons nos travaux à l’étude de matricesde leviers constituées de lignes découplées en régime dynamique. Comme lesupport des leviers est élastique, l’effet du couplage entre levier est pris en compte.La vérification du modèle est soigneusement réalisée. Nous montrons que chaquemode propre peut être décomposé en produits d’un mode de base avec un modede levier. Nous présentons une méthode de discrétisation du modèle et effectuonssa vérification numérique en la comparant avec des résultats de simulation paréléments finis du problème d’élasticité tridimensionnel. Par ailleurs, nous avonsélaboré de nouveaux outils d’aide à la conception de réseaux d’AFM. Une boîte àoutils d’optimisation robuste est interfacée avec le modèle permettant d’optimiserun design avant micro-Fabrication. Un algorithme d’estimation de l’état statiquecombinant la mesure de déplacements mécaniques par interférométrie et le modèlea été introduit. Nous avons également synthétisé un régulateur quadratiquelinéaire (LQR) pour un réseau de cantilevers en mode dynamique comprenant actionneurset capteurs régulièrement espacées. Dans le but de mettre en oeuvre lecontrôle en temps réel, nous proposons une approximation semi-Décentralisée quipeut être réalisé par un circuit électronique distribué analogique. Plus précisément,notre processeur analogique peut être réalisé par un réseau périodique derésistances (PNR). La méthode d’approximation de commande est basée sur deuxconcepts généraux, à savoir sur un calcul fonctionnel (c’est-À-Dire des fonctionsd’opérateurs) et sur la formule de représentation d’une fonction d’opérateur deDunford-Schwartz. Cette méthode d’approximation est étendue pour la résolutiond’un problème de filtrage optimal robuste de type H∞ de la dynamique d’un réseaude leviers couplés avec sources aléatoires de bruit. / In this dissertation, we establish a two-Scale model both for one-Dimensionaland two-Dimensional Cantilever Arrays in elastodynamic operating regime withpossible applications to Atomic Force Microscope (AFM) Arrays. Its derivationis based on an asymptotic analysis for thin elastic structures, a two-Scale approximationand a scaling used for strongly heterogeneous media homogenization. Wecomplete the theory of two-Scale approximation for fourth order boundary valueproblems posed in thin periodic domains connected in some directions only. Ourmodel reproduces the global dynamics as well as each of the cantilever motion. Forthe sake of simplicity, we present a simplified model of mechanical behavior of largecantilever arrays with decoupled rows in the dynamic operating regime. Since thesupporting bases are assumed to be elastic, cross-Talk effect between cantileversis taken into account. The verification of the model is carefully conducted. Weexplain not only how each eigenmode is decomposed into products of a base modewith a cantilever mode but also the method used for its discretization, and reportresults of its numerical validation with full three-Dimensional Finite Element simulations.We show new tools developed for Arrays of Microsystems and especiallyfor AFM array design. A robust optimization toolbox is interfaced to aid for designbefore the microfabrication process. A model based algorithm of static stateestimation using measurement of mechanical displacements by interferometry ispresented. We also synthesize a controller based on Linear Quadratic Regulator(LQR) methodology for a one-Dimensional cantilever array with regularly spacedactuators and sensors. With the purpose of implementing the control in real time,we propose a semi-Decentralized approximation that may be realized by an analogdistributed electronic circuit. More precisely, our analog processor is made by PeriodicNetwork of Resistances (PNR). The control approximation method is basedon two general concepts, namely on functions of operators and on the Dunford-Schwartz representation formula. This approximation method is extended to solvea robust H∞ filtering problem of the coupled cantilevers for time-Invariant systemwith random noise effects.