No description available.

Les Infrastructures Virtuelles (VIs) ont émergé de la combinaison de l’approvisionnement des ressources informatiques et des réseaux virtuels dynamiques. Grâce à la virtualisation combinée des ressource de calcul et de réseau, le concept de VI transforme l’Internet en un réservoir mondial de ressources interconnectées. Avec l’innovation des VIs viennent aussi des nouveaux défis nécessitant le développement de modèles et technologies, pour assister la migration d’applications existantes d’infrastructures traditionnelles vers des VIs. L’abstraction complète des ressources physiques et l’indéterminisme dans les besoins des applications, en termes de ressources de calcul et de communication ont fait de la composition de VI un problème difficile. En outre, l’allocation d’un ensemble des VIs sur un substrat distribué est un problème NP-difficile. En plus des objectifs traditionnels (par exemple un coût minimal, un revenu croissant), un algorithme d’allocation doit également satisfaire les attentes des utilisateurs (par exemple la qualité de l’allocation). Ce manuscrit contribue aux initiatives de recherche en cours avec les propositions suivantes : i) le Virtual Infrastructure Description Language (VXDL), qui permet aux utilisateurs et aux systèmes de décrire les composants pertinents d’une VI ; ii) un mécanisme qui traduit un flux de travail en une spécification de VI pour faciliter l’exécution d’applications distribuées; iii) une solution pour réduire l’espace de recherche d’une façon automatique qui accélère le processus d’allocation ; et iv) un service offert par des fournisseurs d'infrastructure avec lequel un utilisateur peut déléguer les besoins en fiabilité. / Virtual Infrastructures (VIs) have emerged as result of the combined on-demand provisioning of IT resources and dynamic virtual networks. By combining IT and network virtualization, the VI concept is turning the Internet into a worldwide reservoir of interconnected resources, where computational, storage, and communication services are available on-demand for different users and applications. The innovation introduced by VIs posed a set of challenges requiring the development of new models, technologies, and procedures to assist the migration of existing applications from traditional infrastructures to VIs. The complete abstraction of physical resources, coupled with the indeterminism of required computing and communication resources to execute applications, turned the specification and composition of a VI into a challenging task. In addition, mapping a set of VIs onto a distributed substrate is an NP-hard problem. Besides considering common objectives of infrastructure providers (e.g., efficient usage of the physical substrate, cost minimization, increasing revenue), an allocation algorithm should consider the users' expectations (e.g., allocation quality, data location and mobility). This thesis contributes to related research initiatives by proposing the following: i) Virtual Infrastructure Description Language (VXDL), a descriptive and declarative language that allows users and systems to model the components of a VI; ii) a mechanism for composing VI specifications to execute distributed applications; iii) an approach to reduce the search space in an automatic way, accelerating the process of VI allocation; and iv) mechanism for provisioning reliable VIs.

La vérification de la résistance aux attaques des implémentations embarquées des vérifieurs de code intermédiaire Java Card est une tâche complexe. Les méthodes actuelles n'étant pas suffisamment efficaces, seule la génération de tests manuelle est possible. Pour automatiser ce processus, nous proposons une méthode appelée VTG (Vulnerability Test Generation, génération de tests de vulnérabilité). En se basant sur une représentation formelle des comportements fonctionnels du système sous test, un ensemble de tests d'intrusions est généré. Cette méthode s'inspire des techniques de mutation et de test à base de modèle. Dans un premier temps, le modèle est muté selon des règles que nous avons définies afin de représenter les potentielles attaques. Les tests sont ensuite extraits à partir des modèles mutants. Deux modèles Event-B ont été proposés. Le premier représente les contraintes structurelles des fichiers d'application Java Card. Le VTG permet en quelques secondes de générer des centaines de tests abstraits. Le second modèle est composé de 66 événements permettant de représenter 61 instructions Java Card. La mutation est effectuée en quelques secondes. L'extraction des tests permet de générer 223 tests en 45 min. Chaque test permet de vérifier une précondition ou une combinaison de préconditions d'une instruction. Cette méthode nous a permis de tester différents mécanismes d'implémentations de vérifieur de code intermédiaire Java Card. Bien que développée pour notre cas d'étude, la méthode proposée est générique et a été appliquée à d'autres cas d'études.

Thèse numérisée par la Direction des bibliothèques de l'Université de Montréal.

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

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

Dans cette thèse nous proposons un modèle temporel dans le cadre des machines à états abstraits (ASM). Une extension du langage de spécification ASM est développé qui correspond à ce modéle temporel pour le temps continu. L'extension du langage avec des constructions de temps permet de diminuer la taille de la spécification et donc de réduire la probabilité d'erreurs. La sémantique de l'extension du langage ASM est fournie et prend en compte les définitions des fonctions externes, les valeurs des délais et les choix de résolution des non-déterminismes. Un sous-système de vérification des propriétés exprimées en logique FOTL (FirstOrder Timed Logic) est développé. Un simulateur d'ASMs temporisées est développé et implémenté, il comprend un analyseur syntaxique, un interprète du langage, un sous-système de vérification des propriétés ainsi qu'une interface graphique / In this thesis a temporal model for abstract state machines (ASM) method is pro- posed. An extension of ASM specification language on the base of the proposed temporal model with continuous time is developed. The language extension helps to reduce the size of the specification hence to diminish the probability of an error. The semantics of the extended ASM language is developed which takes into account the definitions of external functions, the values of time delays and the method of non-determinism resolving. A subsystem for verification of user properties in the FOTL language is developed. A simulator prototype for ASMs with time is developed and implemented. It includes the parser of the timed ASM language, the interpreter, the verification subsystem and the graphical user interface

Cette thèse porte sur la spécification, la vérification et la validation de systèmes critiques à l'aide de méthodes formelles, en particulier, B événementiel. Nous avons travaillé sur l'utilisation de B événementiel pour étudier des algorithmes de contrôle du platooning, à partir d'une version 1D simplifiée vers une version 2D plus réaliste. L'analyse critique du modèle du platooning en 1D a découvert certaines anomalies. La difficulté d'exprimer les théorèmes de deadlock-freeness dans B événementiel nous a motivé pour développer un outil, le générateur de théorèmes de deadlock-freeness, pour construire automatiquement ces théorèmes. Notre évaluation a confirmé que les preuves mathématiques ne sont pas suffisantes pour vérifier la correction d'une spécification formelle : une spécification formelle doit aussi être validée. Nous pensons que les activités de validation, comme les activités de vérification, doivent être associées à chaque raffinement. Pour ce faire, nous avons besoin de meilleurs outils de validation. Certains outils d'exécution existants échouent pour certains modèles non-déterministes exprimés en B événementiel. Nous avons donc conçu et implanté un nouvel outil d'exécution, JeB, un environnement de simulation en JavaScript pour B événementiel. JeB permet aux utilisateurs d'insérer du code sûr à la main pour fournir des calculs déterministes lorsque la traduction automatique échoue. Pour atteindre cet objectif, nous avons défini des obligations de preuve qui garantissent la correction de simulations par rapport au modèle formel / This thesis aims at the specification, verification and validation of safety-critical systems with formal methods, in particular, with Event-B. We assessed the usability of Event-B by the development of platooning control algorithms, specially how it scaled up from a simplified 1D version to a more realistic 2D version. The critical analysis of the 1D platooning model uncovered some anomalous behaviors. The difficulty of expressing the deadlock-freeness theorems in Event-B motivated us to develop a tool, the generator of deadlock-freeness theorems, to automatically construct these theorems. Our assessment confirmed that the mathematical proofs are not sufficient to assure the correctness of a formal specification: a formal specification should also be validated. We believe that the validation activities, like the verification activities, should be associated with each refinement during the development. To do that, we need better validation tools. The state-of-the-art tools which can execute Event-B models failed in highly non-deterministic models. Therefore we designed and implemented a new execution tool, JeB, which is a JavaScript simulation framework for Event-B. JeB allows users to safely insert hand-coded pieces of code to supply deterministic computations where the automatic translation fails. To achieve this goal, we have defined a set of proof-obligations which, when discharged, guarantee the correctness of the simulations with respect to the model.

L’ectoderme embryonnaire devient spécifié en ectoderme non-neural, plaque neurale et bordure neurale à la fin de la gastrulation. Les cellules de bordure neurale sont les progéniteurs de la crête neurale et des placodes. La crête neurale est une population transitoire de cellules multipotentes, qui se forme au cours de la neurulation. Quand les bourrelets neuraux s’élèvent pour former le tube neural, les cellules de la crête neurale subissent une transition épithélio-mésenchymateuse, migrent dans l'ensemble du corps pour atteindre leur destination finale et se différencier. La crête neurale donne naissance à de multiples dérivés tels que les neurones et les cellules gliales du système nerveux périphérique, le cartilage et les os du visage, ou encore les mélanocytes. Des régulations complexes, impliquant de nombreuses signalisations et la transcription de gènes-clé, orchestrent ces événements. Cependant, les premières étapes menant à la formation de la crête neurale et à la spécification précoce de la bordure neurale sont encore peu comprises. Nous avons analysé le transcriptome de la crête neurale d'embryon de l'amphibien Xenopus laevis, à la recherche de nouveaux régulateurs des premières étapes de la formation de la crête neurale. Nous avons constaté que le régulateur de la glycolyse PFKFB4, est exprimé dans l’ectoderme dorsal de la jeune gastrula et dans les cellules de la crête neurale. Ici, nous démontrons que PFKFB4 régule la spécification de l’ectoderme via la voie de signalisation Akt, indépendamment de la glycolyse, démontrant ainsi la première fonction non-glycolytique des enzymes PFKFB. En outre, cette régulation est essentielle pour permettre aux progéniteurs de l'ectoderme d’être spécifiés en plaque neurale, crête neurale, placodes ou ectoderme non neural, mettant en évidence un nouveau point de contrôle de développement. De plus, nous démontrons que PFKFB4 régule des étapes ultérieures de la formation de la crête neurale. Notre travail met en évidence que les régulateurs du métabolisme cellulaire possèdent des fonctions non-métaboliques pour contrôler des étapes de développement au cours du développement embryonnaire. / Embryonic ectoderm becomes specified into non-neural ectoderm, neural plate and neural border at the end of gastrulation. Neural border cells are the progenitors of the neural crest and placodes. The neural crest is a transient population of multipotent cells, which forms during neurulation. As the neural border elevates to form the neural tube, neural crest cells undergo an epithelial to mesenchymal transition, migrate extensively into the whole body to reach their final destinations and differentiate. Neural crest gives rise to multiple derivatives such as neurons and glia, facial cartilage, bones, melanocytes and sympatho-adrenal cells. A complex interplay of signaling and transcriptional regulations orchestrates these early patterning events. However, the first steps leading to NC formation and early specification at the NB are less understood. We analysed the NC transcriptome of frog embryos, to look for novel regulators of the early steps of NC formation. We found that the well-known glycolysis regulator PFKFB4, is expressed in early gastrula dorsal ectoderm, and in neurula neural crest cells. Here, we demonstrate that PFKFB4 regulates ectoderm specification via Akt signaling independently of glycolysis, thus demonstrating the first non-glycolytic function of PFKFB enzymes. Moreover, this regulation is essential to allow ectoderm embryonic progenitors to be patterned into neural plate, neural crest, placodes and definitive ectoderm, highlighting a novel developmental checkpoint. Moreover, we also demonstrate that PFKFB4 regulates later steps of neural crest formation. Our work highlights that regulators of cell metabolism accumulate non-metabolic related functions to control developmental steps during embryonic development.

Cette thèse propose une extension de la logique de séparation pour les programmes parallèles et orientés-objets. La logique de séparation est un formalisme récent et prometteur pour vérifier les programmes impératifs. Cependant, jusqu'à présent, la logique de séparation a été appliquée à des programmes utilisant un opérateur parallèle irréaliste (||) et des verrous non-ré-entrants (contrairement au langage Java). Dans cette thèse, nous adaptons la logique de séparation aux opérateurs "fork" et "join" (utilisés par de nombreux langages: C, Java, etc...) et aux verrous ré-entrants (utilisés par le langage Java).<br /><br />Cette adaptation inclut un système de vérification pour des programmes similaires aux programmes Java. Ce système est constitué d'un ensemble de triplets de Hoare qui forment un algorithme de vérification. La preuve de correction de ce système a été effectuée et ce système a été évalué sur plusieurs exemples ambitieux (dont la classe Itérateur de la librairie Java et un algorithme de couplage de verrous).<br /><br />En plus de l'extension décrite ci-dessus, plusieurs analyses utilisant la logique de séparation ont été inventées.<br /><br />La première analyse consiste à spécifier les séquences d'appels de méthodes autorisées (appelés "protocoles") dans les classes. Cette analyse décrit finement des protocoles complexes (telle que celui de la classe Itérateur). En outre, nous avons proposé une nouvelle technique permettant de vérifier que les spécifications d'un programme sont correctes en utilisant les protocoles.<br /><br />La seconde analyse permet de montrer qu'une formule en logique de séparation n'implique pas une autre formule. Cela est utile dans les vérificateurs de programmes car ceux-ci doivent fréquemment démontrer des implications entre formules. L'intérêt de cette analyse est que sa complexité est basse : cela permet de l'utiliser souvent sans consommer beaucoup de ressources.<br /><br />La troisième analyse permet de paralléliser automatiquement des programmes. Cette analyse prend en entrée des programmes prouvés en logique de séparation et rend en sortie des programmes parallélisés, optimisés, et prouvés. Notre analyse utilise la sémantique de séparation de l'opérateur "*" pour détecter quand deux sous programmes accèdent à des parties disjointes du tas. Dans ce cas, la parallélisation est possible. L'algorithme de détection est implémenté par un système de réécriture.