The ROx is a retinal oximeter under development with the purpose of non-invasively and accurately measuring oxygen saturation (SO₂) in vivo. It is novel in that it utilizes the blue-green oximetry technique with on-axis illumination. ROx calibration tests were performed by inducing hypoxia in live anesthetized swine and comparing ROx measurements to SO₂ values measured by a CO-Oximeter. Calibration was not achieved to the precision required for clinical use, but limiting factors were identified and improved. The ROx was used in a set of sepsis experiments on live pigs with the intention of tracking retinal SO₂ during the development of sepsis. Though conclusions are qualitative due to insufficient calibration of the device, retinal venous SO₂ is shown to trend generally with central venous SO₂ as sepsis develops. The novel sepsis model developed in these experiments is also described. The method of cecal ligation and perforation with additional soiling of the abdomen consistently produced controllable severe sepsis/septic shock in a matter of hours. In addition, the ROx was used to collect retinal images from a healthy human volunteer. These experiments served as a bench test for several of the additions/modifications made to the ROx. This set of experiments specifically served to illuminate problems with various light paths and image acquisition. The analysis procedure for the ROx is under development, particularly automating the process for consistency, accuracy, and time efficiency. The current stage of automation is explained, including data acquisition processes and the automated vessel fit routine. Suggestions for the next generation of device minimization are also described.

A series of studies have been carried out to elucidate the sediment effect on the saturation level of methane hydrate in sediments. The specimens tested covered most of the natural sediment types, with various combinations of particle size and mineral composition. The results obtained indicate that particle size and clay contents are the two key factors determining the saturation level of gas hydrate in sediments: the finer the particle size and/or the higher the clay content, the lower the hydrate saturation. The observed particle size effect and clay effect on hydrate saturation can be accredited to the specific surface area of a sediment.

Introduction: Oxygen delivery, or utilization, is a function of retinal blood flow and blood oxygen saturation. The retinal pigment epithelium (RPE), in particular, has been shown to have the highest levels of metabolic activity within the human body. Oxygen delivery is therefore of extreme importance to the maintenance of the health and integrity of the retina. Animal models presuppose that the oxygen tension in the retina is highest in the innermost layers at the level of the choriocapillaris, less in the photoreceptors and further decreases throughout the outer retinal structures. The choroid provides by far the largest component of the oxygen for consumption by the photoreceptors. A lack of oxygen stores in the inner retina therefore makes a constant supply crucial for its normal functioning. Blood flow dysfunction and subsequent hypoxia are both a feature in the pathogenesis of several major ocular diseases such as retinopathy of prematurity (ROP), age-related macular degeneration (ARMD), diabetic retinopathy (DR) and glaucoma. The development of methods to measure retinal blood flow and blood oxygen saturation is crucial to improve understanding of the patho-physiology of major ocular diseases. Purpose: The aims of this work were, firstly, to determine the least variable (range ± standard deviation) wavelength combination (610/548, 600/569 and 605/586) and subsequent ODR with the prototype HRC device. Secondly, using the ODR with the lowest measurement variability, we sought to quantify retinal blood SO2 in arterioles and venules and investigate the relationship between retinal blood SO2 and total retinal blood flow (TRBF) in response to stepwise changes in PETO2 in healthy participants. Retinal blood SO2 and TRBF were assessed using the IRIS HRC (Photon etc. Inc. Montreal, Canada) and the RTvue Doppler Fourier Domain OCT (Optovue Inc, Freemont, CA) instruments, respectively. Methods: Ten healthy participants between the ages of 23 and 37, with an average age of 28.3 years were evaluated in two descriptive cross-sectional studies. Two gas provocation protocols; hyperoxia (end-tidal oxygen; PETO2 of 100, 200, 300, 400mmHg) and hypoxia (PETO2 of 100, 80, 60, 50mmHg) were administered in a fixed sequential order. In each phase of gas provocation (via modulation of PETO2), retinal blood SO2 and TRBF measurements were acquired with the HRC and Doppler FD-OCT. The precise and repeated control of the partial end tidal pressures of oxygen (PETO2) and carbon dioxide (PETCO2) over the pre-determined phase duration, irrespective of the individuals’ respiratory rate, was made possible with the RespirAct (Thornhill Research Inc., Toronto, Canada); a sequential re-breathing gas delivery Results: In arterioles, the group range (±SD) of ODR values for baseline measurements (PETO2 of 100mmHg) was 0.169±0.061 for the 605/586 wavelength combination, 0.371±0.099 for the 600/569 wavelength combination and 0.340±0.104 for the 610/548 wavelength combination. In venules, the group range (±SD) of ODR values was 0.600±0.198 for the 605/586 wavelength combination, 0.569±0.169 for the 600/569 wavelength combination and 0.819±0.274 for the 610/548 wavelength combination. With the 605/586 combination at baseline 1 and 2 in arterioles, the group range (±SD) of ODR values was 0.607 ± 0.224 and 0.619 ± 0.158, respectively (p = 0.370), while in venules the group range (±SD) of ODR at baseline 1 and 2 was 0.289±0.750 and 0.284 ± 0.729, respectively (p = 0.714). For the 600/569 combination at baseline 1 and 2 in arterioles, the group range (±SD) of ODR values was 0.747±0.350 and 0.761±0.391, respectively (p = 0.424) while in venules the group range (±SD) of ODR at baseline 1 and 2 was 0.329±0.675 and 0.366±0.659, respectively (p = 0.372). For the 610/548 combination at baseline 1 and 2 in arterioles, the group range (±SD) of ODR values was 0.604±0.263 and 0.685±0.450, respectively (p = 0.056) while in venules, the group range (±SD) of ODR at baseline 1 and 2 was 0.292±0.746 and 0.285±1.009, respectively (p = 0.131). There was no statistical difference found between baseline ODR values (baseline 1 and 2) across all three wavelength combinations in both arterioles and venules. The mean retinal blood SO2 value at baseline in arterioles for 4 participants was 95.19% ± 31.04% and venules was 53.89% ± 17.24% (p = 0.115). There was a negative linear relationship between group retinal blood SO2 and TRBF values in the 10 participants studied, although the results of any of the 10 individuals did not show evidence of such a relationship using the described methodology. The Pearson’s correlation coefficient (r) between TRBF and SaO2 was r = -0.354 and p = 0.001 and between TRBF and SvO2 was r = - 0.295, p = 0.008 Conclusion: Of the three wavelength combinations investigated (605/586, 600/569 and 610/548), the 605/586 combination was shown to have the overall least variability. It would be unwise at this stage to adopt this wavelength combination for clinical usage, however, since it is presupposed that the 605/586 combination is also the most reliable combination to detect change in retinal blood SO2 i.e. lower variability of the 605/586 combination may be irrelevant if this combination proves to be insensitive to change in retinal blood SO2. The absolute mean ± SD retinal blood SO2 in the arterioles (SaO2) was 95.19% ± 31.04% and in the venules (SvO2) was 53.89% ± 17.24%. These values fell within the range expected and described in the literature. The magnitude of the difference between the SaO2 and SvO2 was also consistent with the literature. These findings were all appropriate for a low flow, high oxygen exchange vascular network typical of the inner retinal vascular system. Using group rather than individual data, TRBF was found in this study to relate inversely with SaO2 (r = -0.354 and p = 0.001) and SvO2 (r = – 0.295 and p=0.008), respectively. This relationship between TRBF and SaO2 and SvO2, was as expected based upon data derived primarily from animal models. This study is ground-breaking and unique, in that, it is the first study to concomitantly measure both retinal blood SO2 and TRBF in human participants. Individual data showed extensive variability and noise, thus limiting the strength of the association between TRBF and SaO2 and SvO2..

<p>This study evaluated SO4 2- removal from circumneutral mine water (CMW) collected from Middleburg coal mine using coal FA collected from Hendrina power station. The following parameters were investigated: the effect of the amount of FA, the effect of the final pH achieved during treatment, the effect of the initial pH of the mine water and the effect of Fe and Al on SO4 2- removal from mine water. The precipitation of ettringite at alkaline pH was evaluated to further reduce the SO4 2- concentration to below the DWAF limit for potable water. Removal of SO4 2- from mine water was found to be dependent on: the final pH achieved during treatment, the amount of FA used to treat the mine water and the presence of Fe and Al in the mine water. Treatment of CMW using different CMW:FA ratios / 5:1, 4:1, 3:1, and 2:1 resulted in 55, 60, 70 and 71 % SO4 2- removal respectively. Treatment of CMW to pH 8.98, 9.88, 10.21, 10.96, 11.77 and 12.35 resulted in 6, 19, 37, 45, 63 and 71 % SO4 2- removal respectively. When the CMW was modified by adding Fe and Al by mixing with Navigation coal mine AMD and treated to pH 10, 93 % SO4 2- removal was observed. Further studies were done to evaluate the effects of Fe and Al separately. Treatment of simulated Fe containing AMD (Fe-AMD) to pH 9.54, 10.2, 11.8, and 12.1 resulted in 47, 52, 65, and 68 % SO4 2- removal respectively. When Al containing AMD was treated to pH 9.46, 10.3, 11.5 and 12 percentage SO4 2- removal of 39, 51, 55 and 67 % was observed respectively.</p>

Introduction In last decade increasing demand for clinical F-18 Fludeoxyglucose requires a greater F-18 fluoride production. From the other side increasing price of enriched O-18 water compel us to find the most effective way of F-18 activity production. One of the possible way, how to optimize and increase yield of F-18, is to increasing target current with retaining the same or less volume of enriched water. Optimization of F-18 production on IBA Large Volume cylindrical target is presented. Material and Methods Irradiations of [18O]H2O by 18MeV proton beams with intensities 40–55 μA were performed on CYCLON 18/9, IBA cyclotron and on LV cylindrical IBA target. Irradiated enriched water was transported to the hot cell using RDS (Radioactive Delivery System) system and was measured in Curriementor 4 Isotope Calibrator made by PTW. At the beginning it was necessary to satisfy several requirements: i) target and water cooling. Using a simple two dimensional equation we can roughly estimate the equilibrium temperature inside the target [1]: Δt = HT/Ak where: Δt = the temperature rise in the target chamber over cooling water temperature H = is the heat load T = thickness of metal wall A = area of metal in contact with target water k = thermal conductivity In our case with heat load 720 W (40 μA×18 MeV) is Δt = 78 oC. From the curve of boiling point of water as a function of pressure [2], we can observe t = 212 °C at 20 bar or 243 °C at 35 bar, respectively, which corresponds to max. heat load up to 90–95 µA of target current. ii) pressure and filling water volume. Filling water volume was from 2 to 2.15 ml to guarantee stop all beam in water. Also during experiments for safety reasons the operating pressure was limited to 35 bar as the window rupture pressure is > 50 bar for used 0.05 mm Havar foil. In this case increasing target volume with increasing current was provided with longer tube. Results and Conclusion The saturated yields of F-18 for 40 µA to 55 µA target currents are given in TABLE 1. No systematic decrease in yields with increasing target current was observed and yields were in line with the 230 ± 10 mCi/µA measured at acceptance test of target. The [18F]FDG yields from productions using the TRACERlab-Mx module are shown in FIGURE 1. All presented productions of F-18 were prepared with LV target with 55 µA. No decrease in the yield was observed with increasing beam current. It has been demonstrated that it is possible to produce routinely 250 GBq/2hr (6.8 Ci/2hr) of 18F-Fluoride using LV cylindrical target (operating conditions: 55 µA, 18 MeV, 98% enriched water). As the next step we want to test dual beam – 2×55 µA with two LV targets and expected activity about 500 GBq of 18F-Fluoride in 2 hours is expected.

Dans cette thèse, on étudie des problèmes liés à la vérification de systèmes (logiciels). On s'intéresse plus particulièrement à la conception sûre de procédures de décision utilisées en vérification. De plus, on considère également un problème de modularité pour un langage de modélisation utilisé dans la plateforme de vérification Why. De nombreux problèmes de vérification peuvent se réduire à un problème de satisfaisabilité modulo des théories (SMT). Pour construire des procédures de satisfaisabilité, Armando et al. ont proposé en 2001 une approche basée sur la réécriture. Cette approche utilise un calcul général pour le raisonnement équationnel appelé paramodulation. En général, une application équitable et exhaustive des règles du calcul de paramodulation (PC) conduit à une procédure de semi-décision qui termine sur les entrées insatisfaisables (la clause vide est alors engendrée), mais qui peut diverger sur les entrées satisfaisables. Mais ce calcul peut aussi terminer pour des théories intéressantes en vérification, et devient ainsi une procédure de décision. Pour raisonner sur ce calcul, un calcul de paramodulation schématique (SPC) a été étudié, en particulier pour prouver automatiquement la décidabilité de théories particulières et de leurs combinaisons. L'avantage de ce calcul SPC est que s'il termine sur une seule entrée abstraite, alors PC termine pour toutes les entrées concrètes correspondantes. Plus généralement, SPC est un outil automatique pour vérifier des propriétés de PC telles que la terminaison, la stable infinité et la complétude de déduction. Une contribution majeure de cette thèse est un environnement de prototypage pour la conception et la vérification de procédures de décision. Cet environnement, basé sur des fondements théoriques, est la première implantation du calcul de paramodulation schématique. Il a été complètement implanté sur la base solide fournie par le système Maude mettant en oeuvre la logique de réécriture. Nous montrons que ce prototype est très utile pour dériver la décidabilité et la combinabilité de théories intéressantes en pratique pour la vérification. Cet environnement est appliqué à la conception d'un calcul de paramodulation schématique dédié à une arithmétique de comptage. Cette contribution est la première extension de la notion de paramodulation schématique à une théorie prédéfinie. Cette étude a conduit à de nouvelles techniques de preuve automatique qui sont différentes de celles utilisées manuellement dans la littérature. Les hypothèses permettant d'appliquer nos techniques de preuves sont faciles à satisfaire pour les théories équationnelles avec opérateurs de comptage. Nous illustrons notre contribution théorique sur des théories représentant des extensions de structures de données classiques comme les listes ou les enregistrements. Nous avons également contribué au problème de la spécification modulaire pour les classes et méthodes Java génériques. Nous proposons des extensions du language de modélisation Krakatoa, faisant partie de la plateforme Why qui permet de prouver qu'un programme C ou Java est correct par rapport à sa spécification. Les caractéristiques essentielles de notre apport sont l'introduction de la paramétricité à la fois pour les types et les théories, ainsi qu'une relation d'instantiation entre les théories. Les extensions proposées sont illustrées sur deux exemples significatifs: tri de tableaux et fonctions de hachage. Les deux problèmes traités dans cette thèse ont pour point commun les solveurs SMT. Les procédures de décision sont les moteurs des solveurs SMT, alors que la plateforme Why engendre des conditions de vérification dérivées d'une programme source annoté, et les transmet aux solveurs SMT (ou assistants de preuve) pour vérfier la correction du programme.

La qualité du transport électronique est l'une des clés permettant de soutenir la progression des performances pour les futures générations de composants. De très nombreux facteurs, comme le choix de l'isolant et du métal de grille, le matériau de canal ou la présence de contraintes mécaniques, affectent de façon négative ou positive ces propriétés de transport. L'épaisseur du canal, qui atteint des dimensions nanométriques joue également un rôle : interactions avec les interfaces, fluctuations d'épaisseurs, effets de couplage électrostatique ou quantique entre ces interfaces. Il est probable que des mécanismes d'interaction associés à la proximité des zones surdopées de source et de drain puissent également intervenir. A ces dimensions, on s'attend à observer des phénomènes de transport hors d'équilibre, voire balistique, qui peuvent remettre en question la validité des paramètres utilisés pour caractériser le transport. Donc avec l'avancement de la technologie, il devient nécessaire de faire évoluer les modèles de transport et les paramètres afin de mieux expliquer le fonctionnement du MOSFET. Cette thèse se concentre sur la compréhension des modèles de transport existants et des méthodes d'extraction pour les noeuds technologiques actuels et futures. Les modèles de transport et les méthodes d'extraction de paramètres en régime linéaire et de saturation ont été explorés au cours de cette thèse. L'impact de la résistance série, qui est une fonction de la tension de grille, dans les MOSFET avancés est pris en compte et une nouvelle méthode d'extraction améliorée a été développée dans le régime linéaire. Des mesures à basse température ont été utilisées en régime linéaire pour l'extraction des mécanismes de diffusion en utilisant le modèle de mobilité. Une nouvelle méthode de correction pour le courant de drain dans le régime de saturation pour les MOSFET canal court est développée en utilisant les mesures à basse température. Cela permet de corriger du DIBL ainsi que des effets de " self heating ". Le modèle de saturation de vitesse et la méthode d'extraction associée sont explorés dans le régime de saturation et sont étudiés en fonction de la température et de la longueur de canal. Les modèles balistique et quasi-balistique avec le concept de la " kT layer " en régime de saturation sont également étudiés pour les noeuds sub 32 nm. Mesurer la magnétorésistance offre des perspectives prometteuses pour les dispositifs à canal court et permettant d'extraire directement la mobilité, sans la nécessité de la connaissance des dimensions du canal. Un modèle analytique pour la magnétorésistance est développé dans le cadre des noeuds technologiques sub 32 nm pour les modèles de transport balistique et quasi-balistique. La mesure de la magnétorésistance est explorée dans la région de saturation pour la première fois jusqu'à 50 nm sur les MOSFET " bulk " afin de comprendre l'applicabilité de cette méthode d'extraction à ce régime. Enfin les dispositifs bulk+ FDSON, FinFET, et GAA sont caractérisés en fonction de la température et les mécanismes de transport dans ces nouveaux dispositifs sont étudiés jusqu'à 35 nm (FinFET). En outre, le paramètre de champ effectif η est extrait pour les dispositifs sSOI. On trouve qu'il est différent du cas " bulk " comme c'était le cas pour les résultats obtenues sur bulk contraint et FDSOI. Cela est interprété par la rugosité de surface et la diffusion des phonons en raison de l'occupation préférentielle de la sous la bande fondamentale dans ces dispositifs avancés.

In this thesis we address problems related to the verification of software-based systems. We aremostly interested in the (safe) design of decision procedures used in verification. In addition, we alsoconsider a modularity problem for a modeling language used in the Why verification platform.Many verification problems can be reduced to a satisfiability problem modulo theories (SMT). In orderto build satisfiability procedures Armando et al. have proposed in 2001 an approach based on rewriting.This approach uses a general calculus for equational reasoning named paramodulation. In general, afair and exhaustive application of the rules of paramodulation calculus (PC) leads to a semi-decisionprocedure that halts on unsatisfiable inputs (the empty clause is then generated) but may diverge onsatisfiable ones. Fortunately, it may also terminate for some theories of interest in verification, and thusit becomes a decision procedure. To reason on the paramodulation calculus, a schematic paramodulationcalculus (SPC) has been studied, notably to automatically prove decidability of single theories and oftheir combinations. The advantage of SPC is that if it halts for one given abstract input, then PC haltsfor all the corresponding concrete inputs. More generally, SPC is an automated tool to check propertiesof PC like termination, stable infiniteness and deduction completeness.A major contribution of this thesis is a prototyping environment for designing and verifying decisionprocedures. This environment, based on the theoretical studies, is the first implementation of theschematic paramodulation calculus. It has been implemented from scratch on the firm basis provided bythe Maude system based on rewriting logic. We show that this prototype is very useful to derive decidabilityand combinability of theories of practical interest in verification. It helps testing new saturationstrategies and experimenting new extensions of the original (schematic) paramodulation calculus.This environment has been applied for the design of a schematic paramodulation calculus dedicated tothe theory of Integer Offsets. This contribution is the first extension of the notion of schematic paramodulationto a built-in theory. This study has led to new automatic proof techniques that are different fromthose performed manually in the literature. The assumptions to apply our proof techniques are easyto satisfy for equational theories with counting operators. We illustrate our theoretical contribution ontheories representing extensions of classical data structures such as lists and records.We have also addressed the problem of modular specification of generic Java classes and methods.We propose extensions to the Krakatoa Modeling Language, a part of the Why platform for provingthat a Java or C program is a correct implementation of some specification. The key features arethe introduction of parametricity both for types and for theories and an instantiation relation betweentheories. The proposed extensions are illustrated on two significant examples: the specification of thegeneric method for sorting arrays and for generic hash map.Both problems considered in this thesis are related to SMT solvers. Firstly, decision procedures areat the core of SMT solvers. Secondly, the Why platform extracts verification conditions from a sourceprogram annotated by specifications, and then transmits them to SMT solvers or proof assistants to checkthe program correctness.

Starting a few decades ago, the unmanned wheeled vehicle research has drawn lately more attention, especially for off-road environment. As the demand to use electric vehicles increased, the need to conceptualize the use of electrically driven vehicles in autonomous operations became a target. That is because in addition to the fact that they are more environmentally friendly, they are also easier to control. This also gives another reason to enhance further the energy economy of those unmanned electric vehicles. Off-road vehicles research was always challenging, but in the present work the nature of the off-road land is utilized to benefit from in order to enhance the energy consumption of those vehicles. An algorithm for energy consumption optimization for electrically driven unmanned wheeled vehicles is presented. The algorithm idea is based on the fact that in off-road conditions, when the vehicle passes a ditch or a hole, the kinetic energy gained while moving downhill could be utilized to reduce the energy consumption for moving uphill if the dimensions of the ditch/hole were known a distance ahead. Two manipulated variables are evaluated: the wheels DC motors supply voltage and the DC armature current. The developed algorithm is analysed and compared to the PID speed iii controller and to the open-loop control of DC motors. The developed predictive controller achieved encouraging results compared to the PID speed control and also compared to the open-loop control. Also, the use of the DC armature current as a manipulated variable showed more noticeable improvement over using the DC input voltage. Experimental work was carried out to validate the predictive control algorithm. A mobile robot with two DC motor driven wheels was deployed to overcome a ditch-like hindrance. The experimental results verified the simulation results. A parametric study for the predictive control is conducted. The effect of changing the downhill angle and the uphill angle as well as the size of the prediction horizon on the consumed electric energy by the DC motors is addressed. The simulation results showed that, when using the proposed approach, the larger the prediction horizon, the lower the energy consumption is.

Open and throughfall precipitation samples were collected at Haliburton Forest for a total of nine events from July – November of 2009. The following species were analyzed quantitatively: NO3-, SO42-, Cl-, HCOO-, C2O42-, NH4+, Na+, K+, Ca2+, and Mg2+. Wet deposition inputs to the system were quantified and the sources of wet-deposited species were probed. The throughfall method was employed to quantify inputs to the forest floor and probe canopy-precipitation interactions. Leaf wash samples at three heights aided in the interpretation of throughfall data and allowed for an examination of vertical profiles of dry deposition to the canopy. Results suggest possible nitrate foliar leaching during the growing season, although this appears to cease during senescence. This finding supports previous evidence that Haliburton Forest has shifted from nitrogen-limitation toward nitrogen-saturation and estimated total atmospheric N inputs to the system are close to the proposed critical load of 10 kg N ha-1 yr-1.