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.

Improving photofermentative hydrogen production through metabolic engineering and DOE (Design of Experiments)

A l’heure actuelle, les biocarburants renouvelables et qui ne nuit pas à l'environnement sont à l'étude intensive en raison de l'augmentation des problèmes de santé et de la diminution des combustibles fossiles. H2 est l'un des candidats les plus prometteurs en raison de ses caractéristiques uniques, telles que la densité d'énergie élevée et la génération faible ou inexistante de polluants. Une façon attrayante pour produire la H2 est par les bactéries photosynthétiques qui peuvent capter l'énergie lumineuse pour actionner la production H2 avec leur système de nitrogénase. L'objectif principal de cette étude était d'améliorer le rendement de H2 des bactéries photosynthétiques pourpres non sulfureuses utilisant une combinaison de génie métabolique et le plan des expériences. Une hypothèse est que le rendement en H2 pourrait être améliorée par la redirection de flux de cycle du Calvin-Benson-Bassham envers du système de nitrogénase qui catalyse la réduction des protons en H2. Ainsi, un PRK, phosphoribulose kinase, mutant « knock-out » de Rhodobacter capsulatus JP91 a été créé. L’analyse de la croissance sur des différentes sources de carbone a montré que ce mutant ne peut croître qu’avec l’acétate, sans toutefois produire d' H2. Un mutant spontané, YL1, a été récupéré qui a retenu l'cbbP (codant pour PRK) mutation d'origine, mais qui avait acquis la capacité de se développer sur le glucose et produire H2. Une étude de la production H2 sous différents niveaux d'éclairage a montré que le rendement d’YL1 était de 20-40% supérieure à la souche type sauvage JP91. Cependant, il n'y avait pas d'amélioration notable du taux de production de H2. Une étude cinétique a montré que la croissance et la production d'hydrogène sont fortement liées avec des électrons à partir du glucose principalement dirigés vers la production de H2 et la formation de la biomasse. Sous des intensités lumineuses faibles à intermédiaires, la production d'acides organiques est importante, ce qui suggère une nouvelle amélioration additionnel du rendement H2 pourrait être possible grâce à l'optimisation des processus. Dans une série d'expériences associées, un autre mutant spontané, YL2, qui a un phénotype similaire à YL1, a été testé pour la croissance dans un milieu contenant de l'ammonium. Les résultats ont montré que YL2 ne peut croître que avec de l'acétate comme source de carbone, encore une fois, sans produire de H2. Une incubation prolongée dans les milieux qui ne supportent pas la croissance de YL2 a permis l'isolement de deux mutants spontanés secondaires intéressants, YL3 et YL4. L'analyse par empreint du pied Western a montré que les deux souches ont, dans une gamme de concentrations d'ammonium, l'expression constitutive de la nitrogénase. Les génomes d’YL2, YL3 et YL4 ont été séquencés afin de trouver les mutations responsables de ce phénomène. Fait intéressant, les mutations de nifA1 et nifA2 ont été trouvés dans les deux YL3 et YL4. Il est probable qu'un changement conformationnel de NifA modifie l'interaction protéine-protéine entre NifA et PII protéines (telles que GlnB ou GlnK), lui permettant d'échapper à la régulation par l'ammonium, et donc d'être capable d'activer la transcription de la nitrogénase en présence d'ammonium. On ignore comment le nitrogénase synthétisé est capable de maintenir son activité parce qu’en théorie, il devrait également être soumis à une régulation post-traductionnelle par ammonium. Une autre preuve pourrait être obtenue par l'étude du transcriptome d’YL3 et YL4. Une première étude sur la production d’ H2 par YL3 et YL4 ont montré qu'ils sont capables d’une beaucoup plus grande production d'hydrogène que JP91 en milieu d'ammonium, qui ouvre la porte pour les études futures avec ces souches en utilisant des déchets contenant de l'ammonium en tant que substrats. Enfin, le reformage biologique de l'éthanol à H2 avec la bactérie photosynthétique, Rhodopseudomonas palustris CGA009 a été examiné. La production d'éthanol avec fermentation utilisant des ressources renouvelables microbiennes a été traitée comme une technique mature. Cependant, la plupart des études du reformage de l'éthanol à H2 se sont concentrés sur le reformage chimique à la vapeur, ce qui nécessite généralement une haute charge énergetique et résultats dans les émissions de gaz toxiques. Ainsi le reformage biologique de l'éthanol à H2 avec des bactéries photosynthétiques, qui peuvent capturer la lumière pour répondre aux besoins énergétiques de cette réaction, semble d’être plus prometteuse. Une étude précédente a démontré la production d'hydrogène à partir d'éthanol, toutefois, le rendement ou la durée de cette réaction n'a pas été examiné. Une analyse RSM (méthode de surface de réponse) a été réalisée dans laquelle les concentrations de trois facteurs principaux, l'intensité lumineuse, de l'éthanol et du glutamate ont été variés. Nos résultats ont montré que près de 2 moles de H2 peuvent être obtenus à partir d'une mole d'éthanol, 33% de ce qui est théoriquement possible.