• Refine Query
  • Source
  • Publication year
  • to
  • Language
  • 417
  • 175
  • 49
  • 1
  • Tagged with
  • 649
  • 241
  • 138
  • 83
  • 79
  • 79
  • 65
  • 64
  • 61
  • 51
  • 46
  • 45
  • 41
  • 40
  • 38
  • About
  • The Global ETD Search service is a free service for researchers to find electronic theses and dissertations. This service is provided by the Networked Digital Library of Theses and Dissertations.
    Our metadata is collected from universities around the world. If you manage a university/consortium/country archive and want to be added, details can be found on the NDLTD website.
21

Effets des lipoprotéines de faible densité oxydées sur les cellules ostéoblastiques

Hamel, Patrick January 2008 (has links) (PDF)
Plusieurs études rapportent que les personnes ayant un taux élevé de LDL et souffrants d'athérosclérose ont un risque accru de développer l'ostéoporose. Le remodelage osseux est effectué par deux types de cellules. Les ostéoblastes sont responsables de la synthèse de la matrice osseuse et de la régulation de sa dégradation par les ostéoclastes. L'altération de ce processus de renouvellement mène à diverses pathologies osseuses. L'ostéoporose est caractérisée par une faible densité minérale du tissu osseux et une microarchitecture de piètre qualité augmentant les risques de fractures. Les LDL en forte concentration dans le plasma des patients athérosclérotiques subissent une oxydation progressive, ce qui accroit leur réactivité et les rend athérogéniques. Ainsi, le principal objectif de l'étude a été d'évaluer les effets des LDL oxydés (oxLDL), des oxystérols 7β-hydroxycholestérol et 7ketocholestérol et de la Iysophosphatidylcholine (IysoPC) sur les pré-ostéoblastes humains MG-63. Considérant la variété des effets induits par les oxLDL qui étaient rapportés dans la littérature, nous avons émis l'hypothèse que la réponse des ostéoblastes à des concentrations croissantes de oxLDL ne serait pas monophasique. L'exposition des MG-63 à des hox-LDL (LDL fortement oxydées) et au 7β-hydroxycholestérol pendant 48 heures produit une réponse de type hormèse lors des essais de viabilité cellulaire (activité réductrice MTT). Ainsi, il y a augmentation de l'activité réductrice cellulaire à faibles concentrations, effet perdu à fortes concentrations de hox-LDL et de 7β-hydroxycholestérol. Les nLDL (LDL natives) et les mox-LDL (LDL moyennement oxydées) induisent aussi une stimulation de l'activité MTT. Toutefois, celle-ci n'est pas de type hormèse, car il n'y a pas de chute de l'activité MTT à fortes concentrations. Par contre, le 7ketocholestérol réduit l'activité MTT de manière dose-dépendante et la lysoPC n'influence pas l'activité MTT. Contrairement aux nLDL, la stimulation de l'activité MTT par les hox-LDL et les mox-LDL est plus élevée que l'augmentation du nombre de cellules et le taux de division cellulaire (déterminé par la réduction de fluorescence du CFSE mesurée au cytofluoromètre) dans les mêmes conditions. De plus, aucune différence significative de taille cellulaire, de masse mitochondriale ni de l'état lysosomal n'a été observée. Cependant, l'exposition aux hox-LDL provoque une augmentation du potentiel membranaire mitochondrial et la production de ROS. Nous avions comme hypothèse que la stimulation d'activité MTT reflétait les niveaux de ROS cellulaire. Toutefois, une incubation avec l'antioxydant NAC n'a pas d'effet sur l'activité MTT et l'agent pro-oxydant BSO, qui favorise une augmentation de ROS cellulaire, diminue plutôt l'activité MTT. Par contre, nous avons démontré l'expression de l' ARNm d'une f1avoenzyme, la NADPH oxydase NOX-4. Cette enzyme est connue pour produire le radical superoxyde et être stimulée par les hox-LDL. L'inhibition des flavoenzymes avec le DPI a réduit l'activité MTT. De plus, l'analyse de l'autofluorescence des cellules au microscope confocale a permis de constater une augmentation de la fluorescence associée au NAD(P)H. Ces résultats démontrent que les enzymes réductrices dépendantes du NAD(P)H du type flavoenzymes, possiblement NOX-4, jouent un rôle dans l'augmentation du potentiel réducteur cellulaire. Nous voulions aussi vérifier l'hypothèse selon laquelle l'augmentation de la production de ROS induit un stress oxydatif pouvant être dommageable pour les ostéoblastes. Cette hypothèse est appuyée par nos résultats montrant une diminution des groupements thiols réduits (SH-) intracellulaires, de l'activité phosphatase alcaline et l'augmentation de l'expression de l'ARNm de l'enzyme de détoxification métallothionéine en présence de faibles concentrations de oxLDL. Nous proposons le mécanisme suivant: les oxLDL stimulent la production de ROS et des mécanismes intracellulaires associés aux thiols sont enclenchés afin de contrecarrer les effets de ces ROS. Il en découle un stress oxydatif qui oriente l'énergie cellulaire vers la production de NAD(P)H. Le NAD(P)H participe aux activités de flavoenzymes servant à régénérer les groupements thiols, mais il peut aussi être utilisé par la flavoenzyme NOX-4, qui contribue aussi à la production de ROS. Ainsi, les fonctions ostéoblastiques sont perturbées par le stress oxydatif et la réorientation de l'utilisation de l'énergie cellulaire, ce qui contribue à affaiblir la structure osseuse et mène à l'ostéoporose. En effet, les altérations de la prolifération, de la différenciation et de la migration cellulaire témoignent en ce sens. ______________________________________________________________________________ MOTS-CLÉS DE L’AUTEUR : Athérosclérose, Ostéoporose, oxLDL, Essais MTT, ROS, NADPH, Flavoenzyme, NADPH oxydase, NOX-4, Stress oxydatif, Thiols, Métallothionéine.
22

Importance du récepteur Cluster of differentiation-36 dans le métabolisme des LDL natives et oxydées chez la souris

Luangrath, Vilayphone 11 1900 (has links) (PDF)
Les lipoprotéines sont des molécules sanguines composées de lipides et de protéines dont la fonction est de véhiculer les lipides, dont le cholestérol, vers les cellules de l'organisme. Le maintien de l'équilibre plasmatique en cholestérol est réalisé par le taux de synthèse et de captation qui peut s'effectuer principalement par deux voies. D'abord, la captation globale, est un processus d'épuration totale puisqu'elle consiste en la prise et la dégradation complète des lipoprotéines. Dans le cas des lipoprotéines à apoprotéine B, cette voie fait surtout intervenir le récepteur de lipoprotéine de faible densité (rLDL). Cependant, l'homéostasie cellulaire lipidique peut également être régulée par la voie de la captation sélective qui implique seulement la captation d'une fraction des lipides sans amener la dégradation des molécules protéiques. Cette voie fait intervenir l'action de récepteurs scavengers de classe B dont le scavenger de classe B type l (SR-BI). Le SR-BI, reconnu comme étant un récepteur de lipoprotéines de haute densité (HDL) ayant la capacité de prendre sélectivement les esters de cholestérol (EC), a également été reconnu pour sa capacité à lier et à capter sélectivement les EC d'autres classes de lipoprotéines, dont les LDL natives. Un autre récepteur dans la famille des récepteurs scavengers de classe B, le Cluster of differentiation-36 (CD36) manifeste également son implication dans le métabolisme des lipoprotéines. Cependant, son rôle a surtout été démontré au niveau des LDL oxydées (LDLox). Il aurait aussi une faible implication au niveau du métabolisme des HDL. Son rôle dans le métabolisme des LDL reste encore à être défini. Il est maintenant bien reconnu que de hauts niveaux de LDL plasmatiques ont une corrélation positive avec l'incidence de développement de maladies cardiovasculaires telle que l'athérosclérose. Ainsi, l'objectif du présent projet visait à élucider l'implication de CD36 dans le métabolisme des lipoprotéines de faible densité natives et oxydées à différents degrés. Cette étude a été réalisée grâce il des souris transgéniques déficientes pour le gène CD36 (-/-) et de souris sauvages (+/+) servant de contrôles. Le métabolisme des différentes lipoprotéines a été évalué selon des analyses de clairances plasmatiques. Pour ce faire, des lipoprotéines marquées radioactivement au niveau de leur portion protéique ou lipidique ont été injectées et des échantillons sanguins ont été prélevés pour mesurer la quantité de lipoprotéines résiduelles non métabolisées restant en circulation. Des courbes de clairances plasmatiques ont ensuite été tracées et à partir de celles-ci, le taux catabolique fractionnel (TCF) a été calculé pour chacune des parties (protéique et lipidique) des différentes lipoprotéines afin de quantifier la proportion de lipoprotéines métabolisées par les souris. Au terme de ces analyses, le foie des souris a été récolté et analysé pour son contenu en radioactivité dans le but d'évaluer la contribution de cet organe dans le métabolisme des lipoprotéines à l'étude. Les résultats montrent que les LDL et les LDL légèrement oxydées (LOX) sont soumises à la captation sélective, puisque la partie lipidique est éliminée plus rapidement que la partie protéique. Ce processus de prise sélective n'est toutefois pas retrouvé pour les LDL fortement oxydées (FOX) étant donné une clairance moins rapide en lipides qu'en protéines. L'absence de CD36 a pour effet d'accélérer la clairance de la partie protéique des LDL, mais ralentit de manière importante la clairance des LOX et des FOX. De plus, le foie contribue de façon importante au métabolisme des différentes lipoprotéines, mais le CD36 hépatique ne participe pas à cette prise hépatique. En somme, les LDL sont, en partie, éliminées par la voie de la captation sélective, mais leur oxydation progressive entraîne leur clairance via la captation globale. L'importance de CD36 dans l'élimination des LDL oxydées au niveau extra-hépatique suggère une contribution de ce récepteur dans le développement de l'athérosclérose. ______________________________________________________________________________
23

Influence du profil lipidique maternel sur l'expression de récepteurs à lipoprotéine de faible densité

Éthier Chiasson, Maude 03 1900 (has links) (PDF)
L'obésité, avec les conséquences physiologiques qu'elle engendre, est sans doute une des pathologies entraînant le plus grand nombre de décès en Amérique du Nord. On note un accroissement de l'obésité chez les enfants qui semble pouvoir être corrélée au profil lipidique de la mère durant la grossesse. Cependant, les échanges lipidiques placentaires demeurent un volet de la science encore peu étudié. Dans le plasma, le cholestérol est véhiculé via les lipoprotéines, principalement par un certain type, soit les lipoprotéines à faible densité (LDL). Ces LDL natives sont reconnues par le récepteur aux LDL (LDLr) présent à la surface des syncytiotrophoblastes. Chez l'humain, le troisième trimestre de la grossesse associé à une hypercholestérolémie prononcée pouvant avoir comme conséquence d'engendrer des LDL oxydées. Ces particules sont considérées comme étant plus arthérogéniques, puisque leur affinité avec le LDLr est réduite. Ces LDL oxydées sont les ligands d'autres récepteurs soit le « lectinlike oxidized low density lipoprotein receptor-1 » (LOX-1) et le « scavenger receptor type BI» (SR-BI). Par contre, la régulation de l'expression de ces différents récepteurs au niveau du placenta, en cas d'hypercholestérolémie, reste en grande partie inexplorée. Le but de cette étude est de caractériser la régulation de l'expression des différents récepteurs de LDL dans le placenta en fonction du profil lipidique maternel, soit de la concentration de cholestérol plasmatique, de l'indice de masse corporel pré-grossesse (IMC) et du gain de poids (GDP) en cours de grossesse. Les femmes sélectionnées sont dans un premier temps classées selon leur concentration plasmatique (inférieur à 7mM ou supérieur à 8mM), puis rétrospectivement classées selon leur IMC (normal, inférieur ou supérieur à la normale établie), ainsi qu'en fonction de leur GDP durant la grossesse (normal, inférieur ou supérieur à la normale). De plus, l'expression de ces différents récepteurs sera aussi quantifiée chez un groupe de femmes présentant un diabète gestationnel. Enfin, la localisation de ces récepteurs au niveau du syncytiotrophoblaste, soit au niveau de la membrane à bordure en brosse (BBM) ou de la membrane basale plasmique (BPM), sera déterminée. L'expression protéique des différents récepteurs dans le placenta est quantifiée par immunobuvardage de type Western et par immunohistochimie. Les résultats démontrent une diminution de l'expression du LDLr, chez les femmes ayant une concentration de cholestérol >8mM, qui semble être corrélée négativement à l'IMC et au GDP. Inversement, une augmentation de l'expression de LOX-1 est observée chez les femmes ayant une concentration de cholestérol <7mM et semble être corrélée positivement avec l'IMC, mais négativement avec le GDP. L'expression de SR-BI ne semble pas être modifiée. Ainsi, l'environnement placentaire est influencé par les IMC et GDP hors norme, ce qui, à long terme, pourrait être associé à une augmentation des problèmes cardiovasculaires. (Subventionné par IRSC) ______________________________________________________________________________ MOTS-CLÉS DE L’AUTEUR : Placenta, LDL, LDL oxydées, LDLr, LOX-1, SR-BI, diabète gestationnel
24

Utilisation des valeurs propres et vecteurs propres de couplage pour étudier le comportement vibro-acoustique de systèmes couplés

Bessac, François 06 May 1996 (has links) (PDF)
La caractérisation fine des mécanismes mis en jeu lors du couplage de systèmes vibrants est indispensable pour réduire le volume des calculs (ou le nombre de données à manipuler) nécessaires à la description correcte des phénomènes vibratoires résultants. Dans ce cadre, une nouvelle méthodologie a été développée puis appliquée au cas de deux plaques couplées par un ou plusieurs ressorts. <br />Fondée sur une approche modale et un formalisme vectoriel, elle s'appuie sur l'exploitation d'une matrice de couplage adimensionnelle qui décrit les échanges entre les deux plaques. Cette matrice admet autant de valeurs propres de couplage (quantités totalement déterministes) que de ressorts entre les plaques. Ces valeurs propres sont représentatives de la force du couplage tandis que les vecteurs propres indiquent les chemins modaux de transmissions. L'utilisation de ces quantités propres permet de reconstruire l'état vibratoire des plaques après couplage connaissant leur état avant couplage (en configuration découplée bloquée).<br />Une méthode simplifiée est développée dans le cas du couplage multiple. Le chemin de transmission dominant est identifié par l'examen et le tri des valeurs propres de couplage. Le fait de ne garder que la contribution correspondant à ce chemin modal dominant donne d'excellents résultats, l'erreur maximum par rapport à la solution de référence atteignant 3 dB aux plus hautes fréquences.<br />L'application expérimentale de cette méthodologie est possible puisque les valeurs propres de couplage sont mesurables. La méthode s'apparente à une approche de type mobilité, à la différence près que les grandeurs à mesurer sont en configuration découplée bloquée, ce qui permet d'éviter les fréquences singulières inhérentes à l'approche par mobilité classique. Dans des conditions de couplage multiple, l'application de la méthode simplifiée confirme la qualités des résultats obtenus précédemment de façon numérique.
25

Optimisation de l'énergie dans une architecture mémoire multi-bancs pour des applications multi-tâches temps réel

Ben Fradj, Hanene Belleudy, Cécile. Auguin, Michel January 2006 (has links)
Thèse de doctorat : Automatique, traitement du signal et des images : Nice : 2006. / Bibliogr. p.128-134. Résumés en français et en anglais.
26

Détermination des effets biochimiques et physiologiques de la captation sélective des esters de cholestérol des lipoprotéines de faible densité par le récepteur "scavenger" de classe B, type I

Alem, Sonia 04 1900 (has links) (PDF)
Le cholestérol est véhiculé dans le sang par les lipoprotéines de faible densité (LDL), du foie vers les cellules. Ces LDL se divisent en 3 sous-classes (LDL1, LDL2 et LDL3). Elles sont métabolisées soit par captation sélective par le récepteur « scavenger » de classe B, type I (SR-BI) qui permet de capter uniquement leurs esters de cholestérol (EC) ou par captation globale par le récepteur de LDL (rLDL). Des études réalisées par le groupe de Madame Brissette ont démontré que des LDL injectées à des souris et ré-isolées quelques heures plus tard se retrouvent appauvries en EC et sont de plus petites tailles. Ces études ont donc établi le phénomène de la captation sélective des EC des LDL in vivo. Le sujet de ce mémoire est l'étude de l'effet de la captation sélective sur les LDL1, LDL2 et LDL3. Pour cela, des souris CD1 ont été injectées avec 3 mg de LDL1, LDL2 et LDL3 natives et 5 heures plus tard, les LDL modifiées ont été isolées par ultracentrifugation. Le travail expérimental subséquent a permis de déterminer les caractéristiques de chacun des types de LDL à savoir leur composition chimique par dosage enzymatique; taille par électrophorèse sur gradient de gel de polyacrylamide; densité par la procédure de Terpstra; charge selon leurs migrations sur gel d'agarose-barbital; niveau d'oxydation des LDL après une incubation avec du CuSO4; capacité à accepter les EC des HDL3 par la protéine de transfert des esters de cholestérol (CETP); activité de captation sélective des EC de SR-BI des cellules HepG2 envers les différents types de LDL et leurs affinités de liaison pour le rLDL. Les résultats ont démontré qu'il y a une diminution de 15% en EC pour les LDLt modifiées et de 58% et 41% en triglycérides (TG) pour les LDL1 et LDL2 modifiées. Il y a eu également un enrichissement en cholestérol total (CT) et cholestérol libre (CL) pour chacune des 3 sous-classes de LDL modifiées. Les résultats ont également démontré que, par rapport à leurs formes natives respectives, les LDL1 modifiées sont plus denses, plus petites et sont chargées plus négativement, les LDL3 modifiées sont moins denses, plus grosses et plus chargées négativement, alors que les LDL2 modifiées sont moins chargées négativement et ne démontrent pas de différence de taille et de densité. Toutes les sous-classes de LDL modifiées semblent être plus sensibles à l'oxydation, ce qui à première vue semble néfaste. Les résultats de transfert des EC des HDL3 vers les sous-classes de LDL ne démontrent aucune différence significative entre les différentes sous-classes natives et modifiées mais il y a 11% moins de transfert des EC aux LDL3 natives qu'aux LDL1 natives et une tendance à la diminution pour les LDL3 natives par rapport aux LDL2 natives. L'étude in vitro avec des cellules HepG2 a démontré qu'il y a une augmentation de 90% de la captation sélective pour les LDL1 modifiées alors qu'il y a une diminution de 46% pour les LDL2 modifiées, par rapport à leurs formes natives. Aussi, une augmentation de 56% d'affinité de liaison envers le rLDL est observée pour les LDL1 et LDL2 modifiées, par rapport à leurs formes natives. Ainsi, la captation sélective des EC dans la circulation sanguine par le SR-BI favoriserait la dégradation des LDL1 et LDL2, in vivo, ce qui est bénéfique pour l'organisme et permettrait donc la réduction des risques cardiovasculaires. D'autres études sont nécessaires afin de tester les LDL3 sur les cellules HepG2. ______________________________________________________________________________ MOTS-CLÉS DE L’AUTEUR : captation sélective, SR-BI, rLDL, sous-classes de LDL.
27

Propriétés théoriques et applications en statistique et en simulation de processus et de champs aléatoires stationnaires

Lionel, Truquet 10 December 2008 (has links) (PDF)
Ce travail doctoral étudie les propriétés théoriques et asymptotiques des processus et des champs aléatoires stationnaires dont se déduisent des applications en statistique et en simulation. Une premi ère partie (Chapitres 2, 3 et 4) a pour objectif de construire des nouveaux modèles de champs aléatoires de type autorégressifs, sous forme de schémas de Bernoulli, et de donner des résultats au sujet de leur théorie limite. Des notions de dépendance faible sont utilisées, plus générale que les notions bien connues de mélange fort ou d'association. Nous envisagerons un principe d'invariance, faible et fort, pour les champs aléatoires considérés. Dans un deuxième temps, nous nous intéressons à quelques problèmes d'estimation dans deux contextes de dépendance bien précis. Nous étudions au Chapitre 5 un problème de simulation de textures dans un contexte de rééchantillonnage pour des champs de Markov fortement mélangeants dans un cadre non paramétrique. Le Chapitre 6 est consacré à la construction et à l'estimation des paramètres d'une nouvelle série chronologique à valeurs entières de type ARCH. La construction est établie en utilisant des arguments de contraction établis dans le cadre des champs aléatoires et le comportement asymptotique des estimateurs des paramètres, obtenus par quasi-maximum de vraisemblance gaussien est fondée sur des arguments de type diérence de martingales. Enn nous présentons au Chapitre 7 une nouvelle méthode d'estimation des paramètres pour des modèles ARCH de type markoviens, mé- thode obtenue en lissant la quasi vraisemblance gaussienne et nous appliquons cette méthode à une série hétéroscedastique de type LARCH pour laquelle les faibles valeurs de la variance conditionnelle rendent dicile l'utilisation de la méthode classique du quasi maximum de vraisemblance
28

La protection de la partie faible dans l'arbitrage OHADA / The protection of the weak party in OHADA arbitration law

Akakpo, Martial 06 June 2017 (has links)
Soucieux de moderniser le droit de l’arbitrage, le législateur OHADA a adopté des règles particulièrement libérales. Cette approche conforme à la protection des investisseurs, a été généralisée à toute forme d’arbitrage. Il s’ensuit que les règles visant à protéger une partie en position de faiblesse vis-à-vis de son contradicteur ont été peu envisagées. Qu’il s’agisse de la convention d’arbitrage ou du procès arbitral, le sort du faible n’a pas fait l’objet d’une attention particulière. En conséquence, en dépit de nombreuses avancées quant au régime de l’accord arbitral ou du déroulement du procès, le droit OHADA devrait être révisé dans la perspective de pondérer son libéralisme chaque fois la protection du faible est légitime. Cette démarche n’aura de sens que si le législateur OHADA adapte le droit de l’arbitrage à son environnement sociologique et économique. / In order to modernize arbitration law, the OHADA lawmaker adopted particularly liberal rules. This approach complies with the protection of investors, has been generalized to all forms of arbitration proceedings. It follows that the rules designed to protect a party in a weakness position vis-à-vis his opponent has been little considered. Whether the arbitration agreement or of the arbitral proceedings, the fate of the weak is not the subject of special attention. Accordingly, despite many advances as to the regime of the arbitration agreement or conduct of the trial, the OHADA law should be amended in order to mitigate its liberalism whenever the protection of the weak party is legitimate. This approach will only make sense if the OHADA lawmaker adapts the arbitration law to its sociological and economic environment.
29

Vérification par model-checking de programmes concurrents paramétrés sur des modèles mémoires faibles / Verification via Model Checking of Parameterized Concurrent Programs on Weak Memory Models

Declerck, David 24 September 2018 (has links)
Les multiprocesseurs et microprocesseurs multicœurs modernes mettent en oeuvre des modèles mémoires dits faibles ou relâchés, dans dans lesquels l'ordre apparent des opérations mémoire ne suit pas la cohérence séquentielle (SC) proposée par Leslie Lamport. Tout programme concurrent s'exécutant sur une telle architecture et conçu avec un modèle SC en tête risque de montrer à l'exécution de nouveaux comportements, dont certains sont potentiellement des comportements incorrects. Par exemple, un algorithme d'exclusion mutuelle correct avec une sémantique par entrelacement pourrait ne plus garantir l'exclusion mutuelle lorsqu'il est mis en oeuvre sur une architecture plus relâchée. Raisonner sur la sémantique de tels programmes s'avère très difficile. Par ailleurs, bon nombre d'algorithmes concurrents sont conçus pour fonctionner indépendamment du nombre de processus mis en oeuvre. On voudrait donc pouvoir s'assurer de la correction d'algorithmes concurrents, quel que soit le nombre de processus impliqués. Pour ce faire, on s'appuie sur le cadre du Model Checking Modulo Theories (MCMT), développé par Ghilardi et Ranise, qui permet la vérification de propriétés de sûreté de programmes concurrents paramétrés, c'est-à-dire mettant en oeuvre un nombre arbitraire de processus. On étend cette technologie avec une théorie permettant de raisonner sur des modèles mémoires faibles. Le résultat ce ces travaux est une extension du model checker Cubicle, appelée Cubicle-W, permettant de vérifier des propriétés de systèmes de transitions paramétrés s'exécutant sur un modèle mémoire faible similaire à TSO. / Modern multiprocessors and microprocesseurs implement weak or relaxed memory models, in which the apparent order of memory operation does not follow the sequential consistency (SC) proposed by Leslie Lamport. Any concurrent program running on such architecture and designed with an SC model in mind may exhibit new behaviors during its execution, some of which may potentially be incorrect. For instance, a mutual exclusion algorithm, correct under an interleaving semantics, may no longer guarantee mutual exclusion when implemented on a weaker architecture. Reasoning about the semantics of such programs is a difficult task. Moreover, most concurrent algorithms are designed for an arbitrary number of processus. We would like to ensure the correctness of concurrent algorithms, regardless of the number of processes involved. For this purpose, we rely on the Model Checking Modulo Theories (MCMT) framework, developed by Ghilardi and Ranise, which allows for the verification of safety properties of parameterized concurrent programs, that is to say, programs involving an arbitrary number of processes. We extend this technology with a theory for reasoning about weak memory models. The result of this work is an extension of the Cubicle model checker called Cubicle-W, which allows the verification of safety properties of parameterized transition systems running under a weak memory model similar to TSO.
30

Design of ULP circuits for Harvesting applications / Conception des circuits à très faible consommation pour des applications Harvesting

Verrascina, Nicola 05 July 2019 (has links)
La très faible consommation dans les appareilles modernesest le facteur-clé pour les capteurs alimentée par une source d’énergierécupérée. La réduction du budget de puissance peut être atteinte grâceà différents techniques lié à trois niveaux d’abstraction : transistor, circuitet système. L’objet de cette thèse est l’analyse et la conception descircuits à très faible consommation pour des réseaux des capteurs sansfils. A’ régulateur de tension et an émetteur RF ont été examiné. Lepremier est le circuit principal pour la gestion de puissance ; il agitcomme interface entre le transducteur et les autres circuits du capteur.L’metteur est le circuit que exiges le plus de puissance pour fonctionner,donc une réduction de sa puissance il permet une augmentation de lavie opérationnelle du capteur. / In the modern devices Ultra-low power consumption is thesurvival key for the energy-harvested sensor node. The reduction of thepower budget can be achieved by mixing different low–power techniquesat three levels of abstraction: transistor level, circuit level and systemlevel. This thesis deals with the analysis and the design of Ultra-LowPower (ULP) circuits suitable for Energy-Harvesting Wireless SensorNetworks (EHWSN). In particular, voltage regulator and RF transmissioncircuits are examined. The former is the main block in powermanagement unit; it interfaces the transducer circuit with the rest of thesensor node. The latter is the most energy hungry block and thusdecreasing its power consumption can drastically increases the sensoron-time.

Page generated in 0.07 seconds