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

Les applications de traitement intensif de signal apparaissent dans de nombreux domaines d'applications tels que multimédia ou systèmes de détection. Ces applications gèrent les structures de données multidimensionnelles (principalement des tableaux) pour traiter les différentes dimensions des données (espace, temps, fréquence). Un langage de spécification permettant l'utilisation directe de ces différentes dimensions avec un haut niveau d'abstraction est une des clés de la manipulation de la complexité de ces applications et permet de bénéficier de leur parallélisme potentiel. Le langage de spécification Array-OL est conçu pour faire exactement cela. Dans cette thèse, nous introduisons une extension d'Array-OL pour exprimer des dépendances cycliques par des dépendances interrépétitions uniformes. Nous montrons que ce langage de spécification est capable d'exprimer les principaux motifs de calcul du domaine de traitement de signal intensif. Nous discutons aussi de la modélisation répétitive des applications parallèles, des architectures répétitives et les placements uniformes des premières sur les secondes, en utilisant les concepts Array-OL intégrés dans le profil UML MARTE (Modeling and Analysis of Real-time and Embedded systems). Des transformations de haut niveau data-parallèles sont disponibles pour adapter l'application à l'exécution, ce qui permet de choisir la granularité des flots et une simple expression du placement en étiquetant chaque répétition par son mode d'exécution: data parallèle ou séquentiel. L'ensemble des transformations a été revu, étendu et implémenté dans le cadre de l'environnement de comodélisation pour les systèmes embarqués, Gaspard2. Avec l'introduction des dépendances uniformes, notre intérêt s'est tourné aussi sur l'interaction entre ces dépendances et les transformations de haut niveau. C'est essentiel, afin de permettre l'utilisation des outils de refactoring sur les modèles avec dépendances uniformes. En utilisant les outils de refactoring de haut niveau, des stratégies et des heuristiques peuvent être conçues pour aider à l'exploration de l'espace de conception. Nous proposons une stratégie qui permet de trouver de bons compromis entre l'usage de stockage et de ressources de calcul, et dans l'exploitation de parallélisme (à la fois de tâches et de données), stratégie illustrée sur une application industrielle radar. / Intensive signal processing applications appear in many application domains such as video processing or detection systems. These applications handle multidimensional data structures (mainly arrays) to deal with the various dimensions of the data (space, time, frequency). A specification language allowing the direct manipulation of these different dimensions with a high level of abstraction is a key to handling the complexity of these applications and to benefit from their massive potential parallelism. The Array-OL specification language is designed to do just that. In this thesis, we introduce an extension of Array-OL to express cycle dependences by the way of uniform inter-repetition dependences. We show that this specification language is able to express the main patterns of computation of the intensive signal processing domain. We discuss also the repetitive modeling of parallel applications, repetitive architectures and uniform mappings of the former to the latter, using the Array-OL concepts integrated into the Modeling and Analysis of Real-time and Embedded systems (MARTE) UML profile. High-level data-parallel transformations are available to adapt the application to the execution, allowing to choose the granularity of the flows and a simple expression of the mapping by tagging each repetition by its execution mode: data-parallel or sequential. The whole set of transformations was reviewed, extended and implemented as a part of the Gaspard2 co-design environment for embedded systems. With the introduction of the uniform dependences into the specification, our interest turns also on the interaction between these dependences and the high-level transformations. This is essential in order to enable the usage of the refactoring tools on the models with uniform dependences. Based on the high-level refactoring tools, strategies and heuristics can be designed to help explore the design space. We propose a strategy that allows to find good trade-offs in the usage of storage and computation resources, and in the parallelism (both task and data parallelism) exploitation, strategy illustrated on an industrial radar application.

Les phénomènes physiques complexes peuvent être simulés numériquement par des techniques mathématiques. Ces simulations peuvent mener ainsi à la résolution de très grands systèmes. La parallélisation des codes de simulation numérique est alors une nécessité pour parvenir à faire ces simulations en des temps non-exorbitants. Le parallélisme s’est imposé au niveau des architectures de processeurs et les cartes graphiques sont maintenant utilisées pour des fins de calcul généraliste, aussi appelé "General-Purpose GPU", avec comme avantage évident l’excellent rapport performance/prix. Cette thèse se place dans le domaine de la conception de ces applications hautes-performances pour la simulation des machines électriques. Nous fournissons une méthodologie basée sur l’Ingénierie Dirigées par les Modèles (IDM) qui permet de modéliser une application et l’architecture sur laquelle l’exécuter, afin de générer un code OpenCL. Notre objectif est d’aider les spécialistes en algorithmes de simulations numériques à créer un code efficace qui tourne sur les architectures GPGPU. Pour cela, une chaine de compilation de modèles qui prend en compte plusieurs aspects du modèle de programmation OpenCL est fournie. De plus, nous fournissons des transformations de modèles qui regardent des niveaux d’optimisations basées sur les caractéristiques de l’architecture.Comme validation expérimentale, la méthodologie est appliquée à la création d’une application qui résout un système linéaire issu de la Méthode des Éléments Finis. Dans ce cas nous montrons, entre autres, la capacité de la méthodologie de passer à l’échelle par une simple modification de la multiplicité des unités GPU disponibles. / Complex physical phenomena can be numerically simulated by mathematical techniques. Usually, these techniques are based on discretization of partial differential equations that govern these phenomena. Hence, these simulations enable the solution of large-scale systems. The parallelization of algorithms of numerical simulation, i.e., their adaptation to parallel processing architectures, is an aim to reach in order to hinder exorbitant execution times. The parallelism has been imposed at the level of processor architectures and graphics cards are now used for purposes of general calculation, also known as "General- Purpose GPU". The clear benefit is the excellent performance/price ratio. This thesis addresses the design of high-performance applications for simulation of electrical machines. We provide a methodology based on Model Driven Engineering (MDE) to model an application and its execution architecture in order to generate OpenCL code. Our goal is to assist specialists in algorithms of numerical simulations to create a code that runs efficiently on GPGPU architectures. To ensure this, we offer a compilation model chain that takes into account several aspects of the OpenCL programming model. In addition, we provide model transformations that analyze some levels of optimizations based on the characteristics of the architecture. As an experimental validation, the methodology is applied to the creation of an application that solves a linear system resulting from the Finite Element Method (FEM). In this case, we show, among other things, the ability of the methodology of scaling by a simple modification of the number of available GPU devices.

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

Une définition des systèmes temps réel est que leur correction dépend de la correction fonctionnelle mais aussi du temps d'exécution des différentes opérations. Les propriétés temps réels sont alors exprimées comme des contraintes temporelles sur les opérations du système. Nous proposons dans cette thèse un autre point de vue où la correction est définie relativement à la validité temporelle des valeurs prises par les variables du système et aux flots de données qui parcourent le système. Pour définir ces conditions de validité, nous nous intéressons au rythme de mise à jour des variables mais aussi aux liens entre les valeurs des différentes variables du système. Une relation dite d'observation est utilisée pour modéliser les communications et les calculs du système qui définissent les liens entre les variables. Un ensemble de relations d'observation modélise l'architecture et les flots de données du système en décrivant les chemins de propagation des valeurs dans le système. Les propriétés temps réels sont alors exprimées comme des contraintes sur ces chemins de propagation permettant d'assurer la validité temporelle des valeurs prises par les variables. La validité temporelle d'une valeur est définie selon la validité temporelle des valeurs des autres variables dont elle dépend et selon le décalage temporel logique ou événementiel introduit par les communications ou les calculs le long des chemins de propagation. Afin de prouver la satisfiabilité d'une spécification définie par une telle architecture et de telles propriétés, nous construisons un système de transitions à état fini bisimilaire à la spécification. L'existence de ce système fini est justifiée par des bornes sur le décalage temporel entre les variables du système. Il est alors possible d'explorer les exécutions définies par ce système de transitions afin de prouver l'existence d'exécutions infinies satisfaisant la spécification. / Real time systems are usually defined as systems where the total correctness of an operation depends not only on its logical correctness, but also on the execution time. Under this definition, time constraints are defined according to system operations. Another definition of real time systems is centered on data where the correctness of a system depends on the timed correctness of its data and of the data flows across the system. i.e. we expect the values taken by the variable to be regularly renewed and to be consistent with the environment and the other variables. I propose a modeling framework based on this later definition. This approach allows users to focus on specifying time constraints attached to data and to postpone task and communication scheduling matters. The timed requirements are not expressed as constraints on the implantation mechanism, but on the relations binding the system’s variables. These relations between data are expressed in terms of a so called observation relation which abstracts the relation between the values that are taken by some variables, the set of sources and the image. This relation abstracts the communication as well as the computational operations and a set of observation relations models the system architecture and the data flows by defining the paths along which values of sources are propagated to build the values of an image. The real time properties are expressed as constraints on the propagation paths and state the temporal validity of the values. This temporal validity is defined by the time shift between the source and the image, and specifies the propagation of timely sound values along the path to build temporally correct values of the system outputs. At this level of abstraction, the designer gives a specification of the system based on timed properties about the timeline of data such as their freshness, stability, latency etc. In order to prove the feasibility of an observation-based model, a finite state transition system bi-similar with the specification is built. The existence of a finite bi-similar system is deduced from the bounded time shift between the variables. The existence of an infinite execution in this system proves the feasibility of the specification.

La couleur de la peau résulte de la synthèse et de la distribution de la mélanine dans l’épiderme et les poils. La mélanine est un pigment produit par les mélanocytes, des cellules dérivées de la crête neurale. Les mélanocytes transfèrent la mélanine aux kératinocytes environnants et forment l'unité épidermique de mélanisation constituée d’un mélanocyte pour 40 kératinocytes. Les interactions entre les mélanocytes et les kératinocytes sont assurées principalement par la E-CADHÉRINE, une protéine responsable de la formation de jonctions adhérentes entre deux cellules adjacentes. L’ancrage de ses jonctions au cytosquelette est assuré par l’intermédiaire de la β-CATÉNINE. Le rôle de ces protéines n’est pas simplement adhésif, elles interviennent aussi dans de nombreux processus développementaux et assurent le maintien de l’architecture de l’épiderme. De plus, β-CATÉNINE est une protéine centrale de la voie de signalisation WNT/β-CATÉNINE essentielle dans la formation du lignage mélanocytaire. Lors de cette thèse, nous nous sommes intéressés au rôle des protéines E-CADHÉRINE et β-CATÉNINE, d’une part dans l’homéostase des mélanocytes et d’autre part dans le développement embryonnaire d’un type particulier de mélanocytes, ceux peuplant l’extrémité des membres. Dans la première partie, nous avons étudié l’implication de ces protéines dans une leucodermie circonscrite acquise, le Vitiligo. Dans cette pathologie, les mélanocytes disparaissent, générant des zones de peau dépigmentées. L’une des hypothèses invoquées est un défaut adhésion des mélanocytes et leur élimination de la lame basale vers les couches supérieures de l’épiderme. Nous avons montré que la présence de E-CADHÉRINE et β-CATÉNINE à la membrane est altérée dans les mélanocytes Vitiligo avant leur disparition de l’épiderme, au niveau de la peau pigmentée des patients. L’altération de E-CADHÉRINE et β-CATÉNINE à la membrane des mélanocytes est corrélée à une localisation suprabasale de ces cellules et une perturbation de l’unité épidermique de mélanisation. A l’aide de systèmes de peaux reconstruites in vitro et de souris déficientes en E-CADHÉRINE dans les mélanocytes, nous avons démontré un rôle essentiel de E-CADHÉRINE pour l’adhésion des mélanocytes à la lame basale de l’épiderme en présence de stress mécanique et oxydatif, deux facteurs aggravants de la dépigmentation dans le Vitiligo. Nous proposons que l’altération de E-CADHÉRINE est un événement précoce dans la pathologie du Vitiligo qui reste silencieux jusqu’à ce que des stress mécaniques ou oxydatifs accélèrent la perte des mélanocytes (Wagner et al., 2015).Dans la deuxième partie, nous nous sommes intéressés aux rôles des protéines E-CADHÉRINE et β-CATÉNINE dans le développement embryonnaire des mélanocytes. Nous avons examiné la possibilité de générer des mélanoblastes à partir des dérivés des cellules de crêtes neurales qui emprunteraient la voie ventrale de migration et non la voie dorso-latérale classiquement décrite. Nous avons montré que les mélanoblastes produits à partir de la voie ventrale dérivent de cellules précurseurs se spécifiant à E14 en mélanoblastes ou en cellules de Schwann. A l’aide d’un mutant gain de fonction de β-CATÉNINE, nous avons mis en évidence que l’activation de la signalisation de β-CATÉNINE induit la spécification des mélanocytes au détriment des cellules de Schwann. La E-CADHÉRINE n’intervient pas dans la spécification des mélanoblastes issus de la voie ventrale mais est impliquée dans l’expansion des mélanoblastes issus de la voie dorso-latérale au niveau des membres.Ces résultats démontrent un rôle critique de E-CADHÉRINE et β-CATÉNINE dans l’homéostase des mélanocytes dans des conditions de stress et dans la régulation du développement des mélanocytes. / Skin pigmentation results from the synthesis and the distribution of melanin by melanocytes. Melanocytes are neural crest derived cells that produce and transfer melanin to their surrounding keratinocytes. One melanocyte makes contacts with approximately 40 keratinocytes, forming the so-called epidermal melanin unit. Adhesion between melanocytes and keratinocytes is mediated by the adhesive protein E-CADHERIN, which is responsible for the formation of adherens junctions. These junctions are anchored to the cytoskeleton via β-CATENIN. The main function of adhesive proteins is to form cell-cell junctions and to maintain epidermal architecture. β-CATENIN is a central component of the WNT signalling pathway, which is implied in the development of the melanocyte lineage. During this PhD we were interested in the potential roles of E-CADHERIN and β-CATENIN proteins first in melanocyte homeostasis and second in melanocyte development in the mouse limb.In the first part of this PhD project, we studied the role of these proteins in an acquired leuco-derma: the Vitiligo disease. In this disease, depigmented areas appears in the skin due to melano¬cyte loss. One hypothesis for this loss is a defect in adhesive proteins of melanocytes, leading to melanocyte detachment and loss. We examined pigmented skin biopsies of patients with or without Vitiligo and observed that membranous staining of E-CADHERIN and β-CATENIN is absent from, or discontinuously distributed across melanocyte membranes of Vitiligo patients long before clinical lesions appeared. The abnormal distribution of E-CADHERIN correlated with lower melanocyte numbers in the basal epidermal layer and higher melanocyte numbers in the suprabasal layer. Using reconstructed human epidermis and mouse models with defective E-CADHERIN expression in melanocytes, we showed that E-CADHERIN is required for melanocyte adhesiveness to the basal layer under oxidative and mechanical stress. These observations establish a link between pre-clinical, cell-autonomous defects in Vitiligo melanocytes and known environmental stressors accelerating disease onset. Our results implicate a primary predisposing skin defect affecting melanocyte adhesiveness, which under stress conditions, leads to the disappearance of melanocytes and clinical Vitiligo (Wagner et al., 2015).In the second part of this PhD project, we examined the role of these two proteins E-CADHERIN and β-CATENIN in the development of melanoblasts from the ventrally migrating pathway in contrast to the laterally migrating pathway previously described. We observed that ventrally migrating melanoblasts arose from precursors specified at E14 in melanoblasts or Schwann cells. Using a β-CATENIN gain of function mouse model, Tyr::Cre ; bcatΔex3 we observed that β-CATENIN signalling activation induced melanoblast specification at the expense of Schwann cells. We also demonstrated that E-CADHERIN loss in melanocytes (Tyr::Cre ; EcadF/F) decreased dorso-laterally migrating melanoblast expansion in the limb. Taken together, these results point to a critical role for E-CADHERIN and β-CATENIN in maintaining melanocyte homeostasis under stress conditions and regulating melanocyte development.

Durant ma thèse, j’ai participé à une étude fonctionnelle qui a démontré que p120-RasGAP, une protéine appartenant à la famille GAP (GTPase-activating protein), est le médiateur cytoplasmique de l’éphrine lors de l’atténuation d’ERK1/2. Pour confirmer cela, j’ai réalisé une expérience de co-immunoprécipitation et j’ai démontré que p120-RasGAP s’associe au récepteur de l’éphrine, Eph3, quand celui-ci est activé par un ligand éphrine. Ce résultat indique fortement que les signaux FGF et éphrine convergent au niveau de Ras et qu’ils contrôlent de manière antagoniste son activité. Dès lors, j’ai analysé les autres événements de spécification cellulaire impliquant l’antagonisme FGF/éphrine. Chez l’embryon d’ascidie, le signal FGF est décrit comme inducteur du destin neural dans les cellules ectodermiques qui, en absence du signal FGF, adoptent le destin épidermique. L’induction neurale des ascidies a lieu au stade 32 cellules et se traduit par la spécification de quatre précurseurs neuraux (ERK+) parmi les 16 cellules ectodermiques. J’ai démontré que le signal éphrine/Eph/RasGAP antagonise le signal FGF pour générer une activation d’ERK1/2 de type tout ou rien parmi les cellules ectodermiques. Enfin, en collaboration avec Philip Abitua, doctorant dans le laboratoire du Dr. Mike Levine (UC Berkeley), nous démontrons que l’antagonisme entre les signaux éphrine et FGF est impliqué dans la régionalisation antéro-postérieure de la plaque neurale / During my thesis study, I was involved in functional studies to demonstrate that p120-RasGAP, a GTPase-activating-protein (GAP), is a cytoplasmic mediator of the ephrin-mediated ERK attenuation. To confirm this notion, I conducted a co-immunoprecipitation experiment and demonstrated that p120-RasGAP associates with an ephrin receptor, Eph3, when the latter is activated by an ephrin ligand in ascidian embryos. These results strongly indicate that FGF and ephrin signals converge at the level of Ras and control its activity antagonistically. Following this finding, I looked for other cell fate specification events controlled by the antagonism between ephrin and FGF signals. In ascidian embryos, FGF signals are known to induce neural fates in ectodermal cells which otherwise adopt epidermal fates. Ascidian neural induction takes place at the 32-cell stage, resulting in specification of specific four cells as ERK1/2-active neural precursors among 16 ectodermal cells. I was able to demonstrate that ephrin/Eph/RasGAP signals counterbalance FGF neural inducing signals to generate the ON-OFF response of ERK activation among the ectodermal cells. Finally, in collaboration with a PhD student in Dr. Mike Levine’s lab (UC Berkeley), the antagonism between ephrin and FGF signals plays a role in regionalisation of the neural plate along the anterior-posterior axis.

Chez les rongeurs, les interneurones (INs) corticaux sont issus de l’éminence ganglionnaire (EG) médiale (MGE) et caudale (CGE), expriment une combinaison de facteurs définis et migrent tangentiellement puis radialement pour atteindre leur position laminaire définitive. La diversité et la spécification des sous-types d’INs provenant de la MGE ont suscité de nombreuses études, en revanche les mécanismes moléculaires contrôlant la migration et la spécification des INs issus de la CGE demeurent toujours obscurs. Dans cette étude, les voies de migration de ces INs ont été examinées grâce à une lignée de souris rapportrices des interneurones issus de la CGE avant d’analyser le rôle de deux facteurs de transcription, COUP-TFI et COUP-TFII, hautement exprimés dans la CGE. Deux voies de migration non précédemment caractérisées ont alors été identifiées : une voie dorsale (CLMS) où les INs migrent vers l’EG latérale (LGE) et une voie ventrale (CMMS) où les INs migrent vers la MGE. Le CLMS et le CMMS ont donc été analysés, ainsi que la voie de migration caudale (CMS), à différents stades de développement et l’expression spécifique de certains gènes a pu être identifiée. En inactivant conditionnellement COUP-TFI et/ou COUP-TFII dans les INs, les voies de migration sont altérées ainsi que l’expression des marqueurs moléculaires. Comme probable conséquence, les souris mutantes adultes montrent une distribution altérée des sous-populations d’INs en particulier de celles issues de la CGE. Mon étude a donc permis d’identifier et de caractériser deux nouvelles voies de migration pour les INs provenant de la CGE et a montré que COUP-TFs contribuent à leur modulation. / In rodents, cortical interneurons (INs) originate from the medial (MGE) and caudal ganglionic eminence (CGE) according to precise temporal schedules, express a defined combination of factors, and reach their final laminar position through tangential and radial cell migration. The diversity and fate-specification of MGE-derived interneuron subtypes are well characterized however the molecular mechanisms controlling the migration and specification of CGE-derived INs are still vague. In this study, I have first investigated the migratory paths of cortical INs using a reporter line specific to the CGE, and then I have assessed the involvement of COUP-TFI and COUP-TFII, which are highly expressed in the embryonic CGE during development, in these paths. My data unravelled two major previously non-characterized migratory streams from the subpallium to the pallium: a dorsal stream (CLMS) in which CGE-derived cells migrate to the lateral GE (LGE), and a ventral one (CMMS) in which CGE-derived cells migrate to the MGE. I have characterized both streams and the already well-described caudal stream (CMS) during different stages of development and identified a series of genes expressed in the migrating cells. By inactivating COUP-TFI and/or COUP-TFII in the developing INs, these streams together with their molecular marker expression are perturbed. As a consequence, adult mutant mice have an altered distribution of interneuron subpopulations, particularly the ones derived from the CGE. Taken together, my study identified and characterized two novel CGE-derived interneuron migratory routes to the cortex and showed that COUP-TFs contribute in modulating these paths.

Pour la conception d’un système contrôle-commande, les spécifications fonctionnelles sont à la charge des concepteurs car ce sont eux qui en maîtrisent le fonctionnement. Ces experts n’ont pourtant généralement pas les connaissances en programmation de ceux qui conçoivent le système de pilotage. Ils écrivent alors ces spécifications fonctionnelles en langage naturel, les communiquent ensuite aux concepteurs de l’interface de supervision et du programme de commande qui sont en charge de les implémenter et de les intégrer au système. Les erreurs qui découlent de l’interprétation des spécifications émanent de la différence de culture technique entre les différents intervenants du projet. De plus, suivant la complexité du système, la définition des spécifications fonctionnelles peut être fastidieuse. Nous proposons une approche de conception basée d’une part sur l’analyse de la tâche et sur les techniques du End User Development pour l’obtention de spécifications fonctionnelles validées par les experts métiers. Les techniques de l’ingénierie dirigée par les modèles sont mises en oeuvre pour générer automatiquement l’interface de spécification (qui intègre un Enregistreur, un Généralisateur, un Rejoueur, et un Correcteur), l’interface de supervision du système à piloter et son programme de commande. La démarche proposée a fait l’objet d’une preuve de concept démontrant sa faisabilité technique. Cette preuve de concept a fait l’objet d’évaluations qui ont démontré son intérêt dans le cadre de la conception de système de supervision. / For designing complex and sociotechnical systems, business experts are responsible for writing the functional specifications because of their operational expert knowledge. However, these experts do not usually own the programming knowledge of those who design supervision systems. The task of the system design expert is then to define the functional specifications. S/he writes them in natural language, and then provides them to the designers of the supervision interface and the control-command code. The designers’ job is then to implement and integrate the specifications into the system. Errors from the specification interpretation come from the difference of technical knowledge between the various partners involved in the project. Moreover, depending on the complexity of the system, the definition of functional specifications can be tedious.We propose a design approach based on task modelling and End User Development in order to obtain functional specifications validated by the business experts (mechanical engineer for example).Model-driven engineering techniques are implemented to automatically generate the specification interface (that integrates Recorder, Generalizer, Replayer, and Corrector), the system supervision interface to be piloted and its control program.The technical feasibility of the proposed approach was demonstrated through a proof of concept. This proof of concept was evaluated to demonstrate the interest of the approach in the design of supervision systems.

Le présent mémoire propose une investigation approfondie de l’analyseur Alloy afin de juger son adaptabilité en tant que vérificateur de modèles. Dans un premier temps, l’étude dresse un tableau comparatif de six vérificateurs de modèles, incluant Alloy, afin de déterminer lequel d’entre eux est le plus apte à résoudre les problématiques de sécurité fonctionnelle posées par les systèmes d’information. En conclusion de cette première phase, Alloy émerge comme l’un des analyseurs les plus performants pour vérifier les modèles sur lesquels se fondent les systèmes d’information. Dans un second temps, et sur la base des problématiques rencontrées au cours de cette première phase, l’étude rapporte une série d’idiomes pour, d’une part, présenter une manière optimisée de spécifier des traces et, d’autre part, trouver des recours afin de contourner les limitations imposées par Alloy. À ces fins, le mémoire propose deux nouveaux cas d’espèce, ceux d’une cuisinière intelligente et d’une boîte noire, afin de déterminer si oui ou non l’analyseur est capable de gérer les systèmes dynamiques possédant de nombreuses entités avec autant d’efficacité que les systèmes qui en possèdent moins. En conclusion, le mémoire rapporte que Alloy est un bon outil pour vérifier des systèmes dynamiques mais que sa version récente, DynAlloy, peut être encore mieux adapté pour le faire puisque précisément conçu pour faire face aux spécificités de ce type de système. Le mémoire s’achève sur une présentation sommaire de ce dernier outil.