A Type-Preserving Compiler from System F to Typed Assembly Language

L'utilisation des méthodes formelles est de plus en plus courante dans le développement logiciel, et les systèmes de types sont la méthode formelle qui a le plus de succès. L'avancement des méthodes formelles présente de nouveaux défis, ainsi que de nouvelles opportunités. L'un des défis est d'assurer qu'un compilateur préserve la sémantique des programmes, de sorte que les propriétés que l'on garantit à propos de son code source s'appliquent également au code exécutable. Cette thèse présente un compilateur qui traduit un langage fonctionnel d'ordre supérieur avec polymorphisme vers un langage assembleur typé, dont la propriété principale est que la préservation des types est vérifiée de manière automatisée, à l'aide d'annotations de types sur le code du compilateur. Notre compilateur implante les transformations de code essentielles pour un langage fonctionnel d'ordre supérieur, nommément une conversion CPS, une conversion des fermetures et une génération de code. Nous présentons les détails des représentation fortement typées des langages intermédiaires, et les contraintes qu'elles imposent sur l'implantation des transformations de code. Notre objectif est de garantir la préservation des types avec un minimum d'annotations, et sans compromettre les qualités générales de modularité et de lisibilité du code du compilateur. Cet objectif est atteint en grande partie dans le traitement des fonctionnalités de base du langage (les «types simples»), contrairement au traitement du polymorphisme qui demande encore un travail substantiel pour satisfaire la vérification de type.

Timing verification in transaction modeling

Les systèmes Matériels/Logiciels deviennent indispensables dans tous les aspects de la vie quotidienne. La présence croissante de ces systèmes dans les différents produits et services incite à trouver des méthodes pour les développer efficacement. Mais une conception efficace de ces systèmes est limitée par plusieurs facteurs, certains d'entre eux sont: la complexité croissante des applications, une augmentation de la densité d'intégration, la nature hétérogène des produits et services, la diminution de temps d’accès au marché. Une modélisation transactionnelle (TLM) est considérée comme un paradigme prometteur permettant de gérer la complexité de conception et fournissant des moyens d’exploration et de validation d'alternatives de conception à des niveaux d’abstraction élevés. Cette recherche propose une méthodologie d’expression de temps dans TLM basée sur une analyse de contraintes temporelles. Nous proposons d'utiliser une combinaison de deux paradigmes de développement pour accélérer la conception: le TLM d'une part et une méthodologie d’expression de temps entre différentes transactions d’autre part. Cette synergie nous permet de combiner dans un seul environnement des méthodes de simulation performantes et des méthodes analytiques formelles. Nous avons proposé un nouvel algorithme de vérification temporelle basé sur la procédure de linéarisation des contraintes de type min/max et une technique d'optimisation afin d'améliorer l'efficacité de l'algorithme. Nous avons complété la description mathématique de tous les types de contraintes présentées dans la littérature. Nous avons développé des méthodes d'exploration et raffinement de système de communication qui nous a permis d'utiliser les algorithmes de vérification temporelle à différents niveaux TLM. Comme il existe plusieurs définitions du TLM, dans le cadre de notre recherche, nous avons défini une méthodologie de spécification et simulation pour des systèmes Matériel/Logiciel basée sur le paradigme de TLM. Dans cette méthodologie plusieurs concepts de modélisation peuvent être considérés séparément. Basée sur l'utilisation des technologies modernes de génie logiciel telles que XML, XSLT, XSD, la programmation orientée objet et plusieurs autres fournies par l’environnement .Net, la méthodologie proposée présente une approche qui rend possible une réutilisation des modèles intermédiaires afin de faire face à la contrainte de temps d’accès au marché. Elle fournit une approche générale dans la modélisation du système qui sépare les différents aspects de conception tels que des modèles de calculs utilisés pour décrire le système à des niveaux d’abstraction multiples. En conséquence, dans le modèle du système nous pouvons clairement identifier la fonctionnalité du système sans les détails reliés aux plateformes de développement et ceci mènera à améliorer la "portabilité" du modèle d'application.

Studies on the exaggerated inflammatory response caused by streptococcus suis at systemic and central nervous system levels

Streptococcus suis de type 2 est un microorganisme pathogène d’importance chez le porc. Il est la cause de différentes pathologies ayant comme caractéristique commune la méningite. C’est également un agent émergeant de zoonose : des cas cliniques humains ont récemment été rapportés en Asie. Cependant, la pathogénèse de S. suis n’est pas encore complètement élucidée. Jusqu’à présent, la réponse pro-inflammatoire initiée par S. suis n’a été étudiée qu’in vitro. L’étude du choc septique et de la méningite requiert toujours des modèles expérimentaux appropriés. Au cours de cette étude, nous avons développé un modèle in vivo d’infection chez la souris qui utilise la voie d’inoculation intra-péritonéale. Ce modèle a servi à l’étude de la réponse pro-inflammatoire associée à ce pathogène, tant au niveau systémique qu’au niveau du système nerveux central (SNC). Il nous a également permis de déterminer si la sensibilité aux infections à S. suis pouvait être influencée par des prédispositions génétiques de l’hôte. Le modèle d’infection par S. suis a été mis au point sur des souris de lignée CD1. Les résultats ont démontré une bactériémie élevée pendant les trois jours suivant l’infection. Celle-ci était accompagnée d’une libération rapide et importante de différentes cytokines pro-inflammatoires (TNF-α, IL-6, IL-12p40/p70, IFN-ɣ) et de chémokines (KC, MCP-1 and RANTES), qui ont entraîné un choc septique et la mort de 20 % des animaux. Ensuite, pour confirmer le rôle de l’inflammation sur la mortalité et pour déterminer si les caractéristiques génétiques de l’hôte pouvaient influencer la réponse inflammatoire et l’issue de la maladie, le modèle d’infection a été étendu à deux lignées murines consanguines différentes considérées comme résistante : la lignée C57BL/6 (B6), et sensible : la lignée A/J. Les résultats ont démontré une importante différence de sensibilité entre les souris A/J et les souris B6, avec un taux de mortalité atteignant 100 % à 20 h post-infection (p.i.) pour la première lignée et de seulement 16 % à 36 h p.i. pour la seconde. La quantité de bactéries dans le sang et dans les organes internes était similaire pour les deux lignées. Donc, tout comme dans la lignée CD1, la bactériémie ne semblait pas être liée à la mort des souris. La différence entre les taux de mortalité a été attribuée à un choc septique non contrôlé chez les souris A/J infectées par S. suis. Les souris A/J présentaient des taux exceptionnellement élevés de TNF-α, IL-12p40/p70, IL-1β and IFN- γ, significativement supérieurs à ceux retrouvés dans la lignée B6. Par contre, les niveaux de chémokines étaient similaires entre les lignées, ce qui suggère que leur influence est limitée dans le développement du choc septique dû à S. suis. Les souris B6 avaient une production plus élevée d’IL-10, une cytokine anti-inflammatoire, ce qui suppose que la cascade cytokinaire pro-inflammatoire était mieux contrôlée, entraînant un meilleur taux de survie. Le rôle bénéfique potentiel de l’IL-10 chez les souris infectées par S. suis a été confirmé par deux approches : d’une part en bloquant chez les souris B6 le récepteur cellulaire à l’IL-10 (IL-10R) par un anticorps monoclonal anti-IL-10R de souris et d’autre part en complémentant les souris A/J avec de l’IL-10 de souris recombinante. Les souris B6 ayant reçu le anticorps monoclonal anti-IL-10R avant d’être infectées par S. suis ont développé des signes cliniques aigus similaires à ceux observés chez les souris A/J, avec une mortalité rapide et élevée et des taux de TNF-α plus élevés que les souris infectées non traitées. Chez les souris A/J infectées par S. suis, le traitement avec l’IL-10 de souris recombinante a significativement retardé l’apparition du choc septique. Ces résultats montrent que la survie au choc septique dû à S. suis implique un contrôle très précis des mécanismes pro- et anti-inflammatoires et que la réponse anti-inflammatoire doit être activée simultanément ou très rapidement après le début de la réponse pro-inflammatoire. Grâce à ces expériences, nous avons donc fait un premier pas dans l’identification de gènes associés à la résistance envers S. suis chez l’hôte. Une des réussites les plus importantes du modèle d’infection de la souris décrit dans ce projet est le fait que les souris CD1 ayant survécu à la septicémie présentaient dès 4 jours p.i. des signes cliniques neurologiques clairs et un syndrome vestibulaire relativement similaires à ceux observés lors de méningite à S. suis chez le porc et chez l’homme. L’analyse par hybridation in situ combinée à de l’immunohistochimie des cerveaux des souris CD1 infectées a montré que la réponse inflammatoire du SNC débutait avec une augmentation significative de la transcription du Toll-like receptor (TLR)2 et du CD14 dans les microvaisseaux cérébraux et dans les plexus choroïdes, ce qui suggère que S. suis pourrait se servir de ces structures comme portes d’entrée vers le cerveau. Aussi, le NF-κB (suivi par le système rapporteur de l’activation transcriptionnelle de IκBα), le TNF-α, l’IL-1β et le MCP-1 ont été activés, principalement dans des cellules identifiées comme de la microglie et dans une moindre mesure comme des astrocytes. Cette activation a également été observée dans différentes structures du cerveau, principalement le cortex cérébral, le corps calleux, l’hippocampe, les plexus choroïdes, le thalamus, l’hypothalamus et les méninges. Partout, cette réaction pro-inflammatoire était accompagnée de zones extensives d’inflammation et de nécrose, de démyélinisation sévère et de la présence d’antigènes de S. suis dans la microglie. Nous avons mené ensuite des études in vitro pour mieux comprendre l’interaction entre S. suis et la microglie. Pour cela, nous avons infecté des cellules microgliales de souris avec la souche sauvage virulente (WT) de S. suis, ainsi qu’avec deux mutants isogéniques, un pour la capsule (CPS) et un autre pour la production d’hémolysine (suilysine). Nos résultats ont montré que la capsule était un important mécanisme de résistance à la phagocytose pour S. suis et qu’elle modulait la réponse inflammatoire, en dissimulant les composants pro-inflammatoires de la paroi bactérienne. Par contre, l’absence d’hémolysine, qui est un facteur cytotoxique potentiel, n’a pas eu d’impact majeur sur l’interaction de S. suis avec la microglie. Ces études sur les cellules microgliales ont permis de confirmer les résultats obtenus précédemment in vivo. La souche WT a induit une régulation à la hausse du TLR2 ainsi que la production de plusieurs médiateurs pro-inflammatoires, dont le TNF-α et le MCP-1. S. suis a induit la translocation du NF-kB. Cet effet était plus rapide dans les cellules stimulées par le mutant déficient en CPS, ce qui suggère que les composants de la paroi cellulaire représentent de puissants inducteurs du NF-kB. De plus, la souche S. suis WT a stimulé l’expression de la phosphotyrosine, de la PKC et de différentes cascades liées à l’enzyme mitogen-activated protein kinase (MAPK). Cependant, les cellules microgliales infectées par le mutant déficient en CPS ont montré des profils de phosphorylation plus forts et plus soutenus que celles infectées par le WT. Finalement, la capsule a aussi modulé l’expression de l’oxyde nitrique synthétase inductible (iNOS) induite par S. suis et par la production subséquente d’oxyde nitrique par la microglie. Ceci pourrait être lié in vivo à la neurotoxicité et à la vasodilatation. Nous pensons que ces résultats contribueront à une meilleure compréhension des mécanismes sous-tendant l’induction de l’inflammation par S. suis, ce qui devrait permettre, d’établir éventuellement des stratégies plus efficaces de lutte contre la septicémie et la méningite. Enfin, nous pensons que ce modèle expérimental d’infection chez la souris pourra être utilisé dans l’étude de la pathogénèse d’autres bactéries ayant le SNC pour cible.

A Categorical Framework for the Specification and the Verification of Aspect Oriented Systems

Un objectif principal du génie logiciel est de pouvoir produire des logiciels complexes, de grande taille et fiables en un temps raisonnable. La technologie orientée objet (OO) a fourni de bons concepts et des techniques de modélisation et de programmation qui ont permis de développer des applications complexes tant dans le monde académique que dans le monde industriel. Cette expérience a cependant permis de découvrir les faiblesses du paradigme objet (par exemples, la dispersion de code et le problème de traçabilité). La programmation orientée aspect (OA) apporte une solution simple aux limitations de la programmation OO, telle que le problème des préoccupations transversales. Ces préoccupations transversales se traduisent par la dispersion du même code dans plusieurs modules du système ou l’emmêlement de plusieurs morceaux de code dans un même module. Cette nouvelle méthode de programmer permet d’implémenter chaque problématique indépendamment des autres, puis de les assembler selon des règles bien définies. La programmation OA promet donc une meilleure productivité, une meilleure réutilisation du code et une meilleure adaptation du code aux changements. Très vite, cette nouvelle façon de faire s’est vue s’étendre sur tout le processus de développement de logiciel en ayant pour but de préserver la modularité et la traçabilité, qui sont deux propriétés importantes des logiciels de bonne qualité. Cependant, la technologie OA présente de nombreux défis. Le raisonnement, la spécification, et la vérification des programmes OA présentent des difficultés d’autant plus que ces programmes évoluent dans le temps. Par conséquent, le raisonnement modulaire de ces programmes est requis sinon ils nécessiteraient d’être réexaminés au complet chaque fois qu’un composant est changé ou ajouté. Il est cependant bien connu dans la littérature que le raisonnement modulaire sur les programmes OA est difficile vu que les aspects appliqués changent souvent le comportement de leurs composantes de base [47]. Ces mêmes difficultés sont présentes au niveau des phases de spécification et de vérification du processus de développement des logiciels. Au meilleur de nos connaissances, la spécification modulaire et la vérification modulaire sont faiblement couvertes et constituent un champ de recherche très intéressant. De même, les interactions entre aspects est un sérieux problème dans la communauté des aspects. Pour faire face à ces problèmes, nous avons choisi d’utiliser la théorie des catégories et les techniques des spécifications algébriques. Pour apporter une solution aux problèmes ci-dessus cités, nous avons utilisé les travaux de Wiels [110] et d’autres contributions telles que celles décrites dans le livre [25]. Nous supposons que le système en développement est déjà décomposé en aspects et classes. La première contribution de notre thèse est l’extension des techniques des spécifications algébriques à la notion d’aspect. Deuxièmement, nous avons défini une logique, LA , qui est utilisée dans le corps des spécifications pour décrire le comportement de ces composantes. La troisième contribution consiste en la définition de l’opérateur de tissage qui correspond à la relation d’interconnexion entre les modules d’aspect et les modules de classe. La quatrième contribution concerne le développement d’un mécanisme de prévention qui permet de prévenir les interactions indésirables dans les systèmes orientés aspect.

In vivo phosphorus spectroscopy in human subjects on a clinical 3T MRI system

Alors que l’Imagerie par résonance magnétique (IRM) permet d’obtenir un large éventail de données anatomiques et fonctionnelles, les scanneurs cliniques sont généralement restreints à l’utilisation du proton pour leurs images et leurs applications spectroscopiques. Le phosphore jouant un rôle prépondérant dans le métabolisme énergétique, l’utilisation de cet atome en spectroscopie RM présente un énorme avantage dans l’observation du corps humain. Cela représente un certain nombre de déEis techniques à relever dus à la faible concentration de phosphore et sa fréquence de résonance différente. L’objectif de ce projet a été de développer la capacité à réaliser des expériences de spectroscopie phosphore sur un scanneur IRM clinique de 3 Tesla. Nous présentons ici les différentes étapes nécessaires à la conception et la validation d’une antenne IRM syntonisée à la fréquence du phosphore. Nous présentons aussi l’information relative à réalisation de fantômes utilisés dans les tests de validation et la calibration. Finalement, nous présentons les résultats préliminaires d’acquisitions spectroscopiques sur un muscle humain permettant d’identiEier les différents métabolites phosphorylés à haute énergie. Ces résultats s’inscrivent dans un projet de plus grande envergure où les impacts des changements du métabolisme énergétique sont étudiés en relation avec l’âge et les pathologies.