No description available.

No description available.

The need for water conservation continues to increase as global freshwater resources dwindle. In response, many golf course superintendents are implementing new methods and tools to become more frugal with their water applications. For example, scheduling irrigation using time-domain reflectometer (TDR) soil moisture sensors can decrease water usage. Still, TDR measurements are time-consuming and only cover small scales, leading to many locations being unsampled. Remotely sensed data such as the normalized difference vegetation index (NDVI) offer the potential of estimating moisture stress across larger scales; however, NDVI measurements are influenced by numerous stressors beyond moisture availability, thus limiting its reliability for irrigation decisions. An alternative vegetation index, the water band index (WBI), is primarily influenced by water absorption within a narrow spectral range of near-infrared light. Previous research has established strong relationships between moisture stress of creeping bentgrass (CBG) grown on sand-based root zones, a typical scenario for golf course putting greens. However, this relationship characterizes only a small portion of total acreage across golf courses, which limits widespread adoption. In our research, '007' CBG and 'Latitude 36'hybrid bermudagrass (HBG) were grown on three soil textures, USGA 90:10 sand (S), sand loam (SL) and clay (C), arranged in a 2 x 3 factorial design, randomized within six individual dry-down cycles serving as replications. Canopy reflectance and volumetric water content (VWC) data were collected hourly between 0700 and 1900 hr using a hyperspectral radiometer and an embedded soil moisture sensor, until complete turf necrosis. The WBI had the strongest relationship to VWC (r = 0.62) and visual estimations of wilt (r = -0.91) compared to the green-to-red ratio index (GRI) or NDVI. Parameters associated with non-linear regression were analyzed to compare grasses, soils, indices, and their interactions. The WBI and GRI compared favorably with each other and indicated significant moisture stress approximately 28 hr earlier than NDVI (P = 0.0010). WBI and GRI respectively predicted moisture stress 12 to 9 hr before visual estimation of 50% wilt, whereas NDVI provided 2 hr of prediction time (P = 0.0317). When considering the time to significant moisture stress, the HBG lasted 28 hr longer than CBG, while S lasted 42 hr longer than either SL and C (P ≤ 0.0011). Nonlinear regression analysis showed that WBI and GRI can be useful for predicting moisture stress of CBG and HBG grown on three diverse soils in a highly controlled environment. Our results provide substantial evidence and direction for future research investigating how WBI and GRI can expedite moisture stress assessment and prediction on a large-acreage basis. / Master of Science in Life Sciences / Managed turfgrasses provide several benefits including filtering pollutants, cooling their surroundings, generating oxygen, preventing erosion, serving as recreational surfaces, and increasing landscape aesthetics. Intensively managed turfgrass systems, such as on golf courses and sports fields, require more inputs to maintain acceptable conditions. Freshwater use is often excessive on intensively managed turfgrasses to maintain proper plant growth. Drought conditions often limit water availability, especially in regions with limited rainfall. Turf managers tend to over-apply water across large acreage when few localized areas begin to show symptoms of drought. Additionally, turf managers sometimes wrongly identify stressed areas from other factors as ones being moisture-deprived. Advancements such as the use of soil moisture meters have simplified irrigation decisions as an aid to visual inspections for drought stress. While this method enhances detection accuracy, it still provides no solution to increase efficiency. Expanding our current knowledge of turfgrass canopy light reflectance for rapid moisture stress identification can potentially save both time and water resources. The objective of this research was to enhance our ability to identify and predict moisture stress of creeping bentgrass (CBG) and hybrid bermudagrass (HBG) canopies integrated into varying soil textures (USGA 90:10 sand (S), sand loam (SL) and Clay (C)) using light reflectance measurements. Dry-down cycles were conducted under greenhouses conditions collecting soil moisture and light reflectance data every hour from 7 am to 7 pm after saturating and withholding water from established plugs. Moisture stress was most accurately estimated over time using two vegetation indices, the water band index (WBI) and green-to-red ratio index (GRI), with approximately ninety percent accuracy to visible wilt stress. The WBI and GRI predicted moisture stress of CBG in all soil types and HBG in SL and C approximately 14 hours before the grasses reached 50% wilt. While light reflectance varies on exposed soils, our research shows that underlying soils do not interfere with measurements across typical turfgrass stands. This research provides a foundation for future research implementing rapid, aerial measurements of moisture stressed turfgrasses on a broad application of CBG and HBG on constructed or native soils.

Yes / During flooding, the suspended sediment transport usually experiences a wide-range of dilute to hyper-concentrated suspended sediment transport depending on the local flow and ground con-ditions. This paper assesses the distribution of sediment for a variety of hyper-concentrated and dilute flows. Due to the differences between hyper-concentrated and dilute flows, a linear-power coupled model is proposed to integrate these considerations. A parameterised method combining the sediment size, Rouse number, mean concentration, and flow depth parameters has been used for modelling the sediment profile. The accuracy of the proposed model has been verified against the reported laboratory measurements and comparison with other published analytical methods. The proposed method has been shown to effectively compute the concentration profile for a wide range of suspended sediment conditions from hyper-concentrated to dilute flows. Detailed com-parisons reveal that the proposed model calculates the dilute profile with good correspondence to the measured data and other modelling results from literature. For the hyper-concentrated profile, a clear division of lower (bed-load) to upper layer (suspended-load) transport can be observed in the measured data. Using the proposed model, the transitional point from this lower to upper layer transport can be calculated precisely.

Hyper-Raman-Streuung folgt anderen Symmetrieauswahlregeln als Raman-Streuung und profitiert als nicht-linearer Zweiphotonenprozess noch mehr von verstärkten elektromagnetischen Feldern an der Oberfläche plasmonischer Nanostrukturen. Damit könnte die oberflächenverstärkte Hyper-Raman-Streuung (SEHRS) praktische Bedeutung in der Spektroskopie erlangen. Durch die Kombination von SEHRS und oberflächenverstärkter Raman-Streuung (SERS) können komplementäre Strukturinformationen erhalten werden. Diese eignen sich aufgrund der Lokalisierung der Verstärkung auf die unmittelbare Umgebung der Nanostrukturen besonders für die Charakterisierung der Wechselwirkung zwischen Molekülen und Metalloberflächen. Ziel dieser Arbeit war es, ein tieferes Verständnis des SEHRS-Effekts zu erlangen und dessen Anwendbarkeit für analytische Fragestellungen einzuschätzen. Dazu wurden SEHRS-Experimente mit Anregung bei 1064 nm und SERS-Experimente mit Anregung bei derselben Wellenlänge sowie mit Anregung bei 532 nm - für eine Detektion von SEHRS und SERS im gleichen Spektralbereich - durchgeführt. Als Beispiel für nicht-resonante Anregung wurden die vom pH-Wert abhängigen SEHRS- und SERS-Spektren von para-Mercaptobenzoesäure untersucht. Mit diesen Spektren wurde die Wechselwirkung verschiedener Silbernanostrukturen mit den Molekülen charakterisiert. Anhand von beta-Carotin wurden Einflüsse von Resonanzverstärkung im SEHRS-Experiment durch die gleichzeitige Anregung eines molekularen elektronischen Übergangs untersucht. Dabei wurde durch eine Thiolfunktionalisierung des Carotins eine intensivere Wechselwirkung mit der Silberoberfläche erzielt, sodass nicht nur resonante SEHRS- und SERS-Spektren, sondern auch nicht-resonante SERS-Spektren von Carotin erhalten werden konnten. Die Anwendbarkeit von SEHRS für hyperspektrale Kartierung in Verbindung mit Mikrospektroskopie wurde durch die Untersuchung von Verteilungen verschiedener Farbstoffe auf strukturierten plasmonischen Oberflächen demonstriert. / Hyper-Raman scattering follows different symmetry selection rules than Raman scattering and, as a non-linear two-photon process, profits even more than Raman scattering from enhanced electromagnetic fields at the surface of plasmonic nanostructures. Surface-enhanced hyper-Raman scattering (SEHRS) could thus gain practical importance for spectroscopy. The combination of SEHRS and surface-enhanced Raman scattering (SERS) offers complementary structural information. Specifically, due to the localization of the enhancement to the close proximity of the nanostructures, this information can be utilized for the characterization of the interaction between molecules and metal surfaces. The aim of this work was to increase the understanding of the SEHRS effect and to assess its applicability to answer analytical questions. For that purpose, SEHRS experiments with excitation at 1064 nm and SERS experiments with excitation at the same wavelength, as well as with excitation at 532 nm - to detect SEHRS and SERS in the same spectral region - were conducted. As an example for non-resonant excitation, pH-dependent SEHRS and SERS spectra of para-mercaptobenzoic acid were examined. Based on these spectra, the interaction of different silver nanostructures with the molecules was characterized. beta-Carotene was used to study the influence of resonance enhancement by the excitation of a molecular electronic transition during SEHRS experiments. By the thiol-functionalization of carotene, a more intense interaction with the silver surface was achieved, which enables to obtain not only resonant SEHRS and SERS but also non-resonant SERS spectra of carotene. Hyperspectral SEHRS imaging in combination with microspectroscopy was demonstrated by analyzing the distribution of different dyes on structured plasmonic surfaces.

O Paradigma Orientado a Objetos tem sido atualmente a abordagem dominante de desenvolvimento de software. Contudo, ela sofre da Tirania da Decomposição Dominante, pois não permite uma modularização adequada da implementação relativa a interesses estruturais. Como consequência, a implementação relativa a cada interesse estrutural fica espalhada pelos módulos do programa e entrelaçada com a implementação relativa a outros interesses estruturais. Outras abordagens de desenvolvimento de software, como o Desenvolvimento de Software Orientado a Aspectos com AspectJ e a Separação Multidimensional de Interesses em Hiperespaços com Hyper/J e CME, atingem sucesso moderado em oferecer mecanismos que permitem superar as deficiências do Paradigma Orientado a Objetos. No entanto, tais abordagens também possuem deficiências e omissões que devem ser reparadas para que elas possam se tornar utilizáveis em contextos típicos de desenvolvimento de software complexo. Este trabalho especifica uma nova abordagem, denominada Desenvolvimento de Software Orientado a Temas (DSOT), que tem como objetivo superar algumas deficiências das abordagens anteriores por meio de mecanismos que permitem a manipulação da implementação de cada interesse estrutural de forma separada e a manipulação da implementação de cada tipo de dado de forma separada. Além disso, DSOT possui operadores que são ortogonais, isto é, podem ser utilizados de forma combinada ou separada, para efetuar a composição de módulos do programa. Mostra-se o modelo conceitual do DSOT e descrevese um estudo de caso que consiste no desenvolvimento de um programa para demonstrar mais concretamente como o DSOT funciona na prática. Não se demonstra a superioridade do DSOT para o caso geral, mas os resultados alcançados evidenciam que o DSOT é uma abordagem promissora que merece ser investigada mais aprofundadamente em pesquisas futuras / The Object-Oriented Paradigm has currently been the dominant approach for developing software. However, it suffers from the Tyranny of the Dominant Decomposition, as it does not support a suitable modularization to the implementation relative to structural concerns. As a consequence, the implementation relative to each structural concern is scattered throughout the program modules and tangled with the implementation relative to other structural concerns. Some software development approaches, such as Aspect-Oriented Software Development with Aspect and Multidimensional Separation of Concerns in Hyperspaces with Hyper/J and CME, achieve moderate success in offering mechanisms that make it possible to overcome the deficiencies of the Object-Oriented Paradigm. However, such approaches also possess deficiencies and ommissions that must be corrected in order for them to get usable in typical complex software development contexts. This work specifies a new approach, named Theme- Oriented Software Development (TOSD), which aims at overcoming some deficiencies from previous approaches through mechanisms that support the handling of implementation for every structural concern separately and the handling of implementation for every data type separately. Moreover, TOSD contains operators which are orthogonal, that is, they can be used separately or as a combination, in order to perform composition of the program modules. We show the conceptual model of TOSD and describe a case study which consists in the development of a program to demonstrate more concretely how TOSD works in practice. We do not demonstrate the superiority of TOSD for the general case, but the results we have obtained suggest that TOSD is a promissing approach which deserves a deeper investigation in future research

Cette thèse, qui relève de la philosophie de l'esprit, consiste en la défense d'une version de la théorie auto-représentationnelle de la conscience. En acceptant d'une part la notion d'état mental possédant un certain contenu qui peut être conscient ou inconscient, et d'autre part l'hypothèse plausible que le contenu de tout état mental consiste en une représentation, alors le problème de la manifestation de la conscience s'appliquant au contenu de CERTAINS états mentaux acquiert intelligibilité dans ce cadre. Il peut être compris comme la recherche d'une structure de représentation qui donne lieu à cette manifestation. Pour certains auteurs (Fred Dretske, Michael Tye et dautres), des conditions particulières dans la représentation directe de l'objet y suffisent, pour d'autres (en particulier David Rosenthal) il y faut une méta-représentation de l'objet sous certaines conditions. Ni l'une ni l'autre de ces structures ne s'avère cependant suffisante pour justifier la démarcation entre états mentaux conscients et inconscients, et pour caractériser la phénoménalité de la conscience. En prenant alors au sérieux l'intuition forte d'auto-référentialité de la conscience (présente déjà chez Aristote - suivant certaines interprétations -, reprise par Brentano, Sartre, et ces dernières années, par Uriah Kriegel et plusieurs autres), on est conduit à proposer, pour les états mentaux conscients, une structure d'auto-représentation (de la représentation) de l'objet qui sous-tend une intentionnalité consciente duale dirigée vers l'objet et en même temps vers elle-même. on résout ainsi les problèmes de la théorie méta-représentationnelle, mais il faut monter que ce schéma est intelligible, que le risque de régression à l'infini dans les capacités repésentationnelles de la conscience n'existe pas, et que de robustes intuitions sont ainsi éclairées, telles que la structuration du champ conscient entre premier plan et arrière-plan, et le lien entre conscience d'arrière plan, ou marginale, et conscience de soi. Ce lien dérive du fait que la conscience marginale, dans la perspective de l'auto-représentation, est la conscience de la conscience d'objet, et se qualifie aussi comme conscience subjective, c'est à dire conscience "pour moi" de l'objet. Et la conscience de soi se construit à partir des épisodes de conscience subjective. L'étude du rapport entre structures de représentation mentale consciente et configurations neuronales spatio-temporelles qui les produisent dans le cerveau est hors du domaine du présent travail, mais la présence nécessaire de ces relations demeure à l'arrière-plan, et affleure dans la réflexion quand cela peut être éclairant. / This work illustrates a version of the self-representational theory of consciousness. If one accepts on the one hand the notion of mental states that have a given content - conscious or unconscious - and on the other hand the plausible hypothesis that the content of all mental states consists in a representation, then the problem of the manifestation of consciousness for (the content of) SOME states becomes intelligible within this frame. This problem can be understood as the research of the representational structure which gives rise to this manifestation. For some authors ( Fred Dretske, Michael Tye, and others) certain particular conditions in the direct representation of the object are sufficient, for others (particularly David Rosenthal) a meta-representation is necessary, under given conditions. However neither of those structures results sufficient to justify the demarcation between conscious and unconscious states and to characterize the phenomenality of consciousness. If one then takes seriously into account the strong intuition of self-referentiality of consciousness (already present in Aristotle - following some interpretations -, taken up again by Brentano, Sartre, and lately by Uriah Kriegel and several others) one is conducted to propose a self-representational structure for conscious mental states which involves a dual conscious intentionality targeting the object and itself at the same time. The problems of the meta-representational theory are thus resolved, but it remains to be shown that this scheme is intelligible, that the risk of infinite regress of the representing capacity of consciousness does not exist, and that strong intuitions are thus acknowledged : such as the distinction in the conscious field between foreground and background, and the link between background, or marginal consciousness, and self consciousness. Within the self-representational view, this link originates from the fact that marginal consciousness is the consciousness of the consciousness of the object, and qualifies itself as subjective consciousness, that is to say, consciousness "for me" of the object. Self consciousness is then constructed from the episodes of subjective consciousness. The relationship between conscious mental representational structures and the spatio-temporal neuronal configurations which produce them in the brain, is outside the domain of the present work, but it is necessarily present in the background, and it is considered when useful for the argument.

La détection précoce de l’athérosclérose, avant le développement de ses séquellespathologiques, comme l’infarctus du myocarde, l’angine ou l’accident cérébrauxvasculaire(ACV), représente un important défi au niveau de la médecine diagnostiqueactuelle. Malgré les récentes avances technologiques, les maladies cardiovasculairesdemeurent la principale cause de décès dans les pays occidentaux et la détection à unstage plus précoce s’avère nécessaire pour permettre une intervention thérapeutiqueadéquate. Notre étude se concentre sur la détection de l’athérosclérose, plusspécifiquement la vulnérabilité de la plaque, grâce à l’imagerie moléculaire combinée àl’observation pathologique. Afin de prédire la rupture de la plaque, l’imageriemoléculaire a émergé comme outil diagnostique puissant suite au développementcroissant de sondes ayant de l’affinité pour les molécules cibles du processusd’athérosclérose. Comme résultantes, ces molécules sélectives possédant une forteaffinité pour des cibles surexprimées durant le processus de formation de la plaque,comme l’αvβ3 par exemple, devrait représentées des sondes prometteuses pour ladétection de l’athérosclérose.Objectif L’objectif global de notre étude était d’évaluer et de prédire lavulnérabilité de la plaque d’athérome à l’aide de différents marqueurs moléculaires. Leprincipal objectif de notre recherche était d’évaluer la possibilité de détecter précocementla plaque en utilisant une ITOP (integrin targeted optical probe). Cette sonde synthétiquenouvellement développée et ciblant l’intégrine αvβ3 avait déjà démontré une affinité etspécificité particulièrement élevée pour le récepteur de l’αvβ3 dans le cancer. Nousavons également exploré la relation entre cette sonde et l’observation pathologique desplaques d’athéromes sur le modèle animale WHHL et sur des plaques humainesprovenant de différents patients.Procédure et Résultats Les expériences ont été réalisées sur un total de 12 lapinsWatanabe hyperlipidémiques de souche WHHL (Watanabe heritable hyperlipidemic) et 1lapin contrôle NZW (New Zealand White). Premièrement, notre ITOP, marquée avec lafluorescéine isothiocyanate (FITC), a été utilisée pour détecter in vitro et ex vivo laprésence du récepteur de l’αvβ3. La microscopie à fluorescence a révélé un importantmarquage de la plaque d’athérome, lequel était absent dans les tissus provenant des lapinscontrôles NZW. Le marquage a été détecté au niveau de segments de plaques provenantde deux régions distinctes de l’aorte ascendante et descendante dans chaque lapin. Lesignal a été détecté principalement au niveau de l’adventitia et de l’intima proximale desvaisseaux aortiques, correspondant directement à l’expression de l’intégrine αvβ3,déterminée par essai immunochimique avec un anticorps contre l’αvβ3. De plus, uneforte association s’est révélée entre le niveau de marquage de la sonde ciblant l’αvβ3 etl’épaisseur de l’adventitia. Deuxièmement, nous avons évalué notre sonde sur deséchantillons humains affectés par l’athérosclérose et comparé les résultats avec uneévaluation morphologique. Nous avons remarqué la même tendance que chez le lapin, soiun marquage plus important lorsque l’adventitia s’épaissi. Finalement, nous avons testé lasonde sur des artères coronaires provenant d’une autopsie d’un patient affecté par le ADHIESet comparé les résultats avec l’évaluation morphologique de leurs artèrescoronaires. Nous avons trouvé un lien entre la morphologie de la plaque et la prévalenced’anévrysmes coronaires chez ces patients.Conclusion L’expression de l’αvβ3 est reliée à la foi aux processus inflammatoires età la sténose. Notre ITOP à marqué efficacement in vitro le premier type de plaqued’athérome classé comme avancé (type IV) et pouvant produire des manifestationscliniques. En combinaison avec l’imagerie noninvasive détectant la sténose, il pourraits’avéré utile dans la détection de la plaque vulnérable. / Purpose The detection of early atherosclerosis, before the development of its later sequelae of myocardial infarction, angina or stroke, constitutes an important challenge in current diagnostic medicine. Despite all the recent technological advances, cardiovascular disease remains the leading cause of death in the Western World and needs to be detected at an earlier stage to allow for more timely therapeutic intervention. This study is focusing on the detection of atherosclerosis or more specifically plaque vulnerability with the help of molecular imaging and pathological observation. Effectively, to predict plaque rupture, molecular imaging has emerged as a powerful diagnostic tool, consequent to the development of a growing number of new probes with affinity for key molecular targets. As a result, such selective molecule with high affinity for overexpressed target in plaque formation, as αvβ3 integrin, should have promise as a probe for imaging atherosclerosis. With the help of molecular imaging combined with pathological observations, we can better comprehend, predict, and detect plaque vulnerability and rupture. Objectives The overall objective of this study is to evaluate different molecular tools to predict the vulnerability of the atheromatous plaque. The major objective of the research was to investigate the possibility of detecting atherosclerotic plaque by using a newly developed synthetic αvβ3 integrin targeted optical probe (ITOP) showing particularly high affinity and specificity for the αvβ3 receptor. We also investigate the relation between this probe and pathological observation of atherosclerotic plaques from WHHL animal model and different human samples. Procedures and Results For this study, experiments were performed on 12 Watanabe heritable hyperlipidemic (WHHL) rabbits and 1 New Zealand White (NZW) rabbits for control. First, our ITOP labeled with fluorescein isothiocyanate was used for detecting the presence of αvβ3 receptors in vitro and ex vivo on a Watanabe rabbit model. Fluorescence microscopy demonstrated a strong labeling of atherosclerotic plaques, which was absent in tissue from normal NZW rabbits. Segments of plaque accumulation from two distinct regions of ascending and descending aortas were labeled in each rabbit. The signal was found principally in the adventitia and proximal intima of the aortic vessel, corresponding directly to the expression of integrin αvβ3 as determined by antibody assay. Moreover, there was a close association between the level of labeling with the αvβ3 targeted probe and the thickness of the adventitia. Secondly, the ITOP was evaluated on human atherosclerotic samples, and was found to efficiently labeled atherosclerotic plaques. Moreover, we observed the same tendency as in the Watanabe rabbit: the ITOP intensity correlated with the degree of adventitial thickening. Finally, we tested the ITOP on Job's Syndrome coronary arteries, and have been able to detect a plaque corresponding to the first type of advanced atherosclerosis (type IV). We also found a relationship between plaque morphology and predisposition to aneurysms in Job's syndrome. Conclusions αvβ3 expression is related to inflammatory and stenotic processes. Our ITOP can efficiently label in vitro the first type of advanced atherosclerotic plaque. In combination with noninvasive imaging techniques that evaluate stenosis, it has great potential for the detection of vulnerable plaque.

O Paradigma Orientado a Objetos tem sido atualmente a abordagem dominante de desenvolvimento de software. Contudo, ela sofre da Tirania da Decomposição Dominante, pois não permite uma modularização adequada da implementação relativa a interesses estruturais. Como consequência, a implementação relativa a cada interesse estrutural fica espalhada pelos módulos do programa e entrelaçada com a implementação relativa a outros interesses estruturais. Outras abordagens de desenvolvimento de software, como o Desenvolvimento de Software Orientado a Aspectos com AspectJ e a Separação Multidimensional de Interesses em Hiperespaços com Hyper/J e CME, atingem sucesso moderado em oferecer mecanismos que permitem superar as deficiências do Paradigma Orientado a Objetos. No entanto, tais abordagens também possuem deficiências e omissões que devem ser reparadas para que elas possam se tornar utilizáveis em contextos típicos de desenvolvimento de software complexo. Este trabalho especifica uma nova abordagem, denominada Desenvolvimento de Software Orientado a Temas (DSOT), que tem como objetivo superar algumas deficiências das abordagens anteriores por meio de mecanismos que permitem a manipulação da implementação de cada interesse estrutural de forma separada e a manipulação da implementação de cada tipo de dado de forma separada. Além disso, DSOT possui operadores que são ortogonais, isto é, podem ser utilizados de forma combinada ou separada, para efetuar a composição de módulos do programa. Mostra-se o modelo conceitual do DSOT e descrevese um estudo de caso que consiste no desenvolvimento de um programa para demonstrar mais concretamente como o DSOT funciona na prática. Não se demonstra a superioridade do DSOT para o caso geral, mas os resultados alcançados evidenciam que o DSOT é uma abordagem promissora que merece ser investigada mais aprofundadamente em pesquisas futuras / The Object-Oriented Paradigm has currently been the dominant approach for developing software. However, it suffers from the Tyranny of the Dominant Decomposition, as it does not support a suitable modularization to the implementation relative to structural concerns. As a consequence, the implementation relative to each structural concern is scattered throughout the program modules and tangled with the implementation relative to other structural concerns. Some software development approaches, such as Aspect-Oriented Software Development with Aspect and Multidimensional Separation of Concerns in Hyperspaces with Hyper/J and CME, achieve moderate success in offering mechanisms that make it possible to overcome the deficiencies of the Object-Oriented Paradigm. However, such approaches also possess deficiencies and ommissions that must be corrected in order for them to get usable in typical complex software development contexts. This work specifies a new approach, named Theme- Oriented Software Development (TOSD), which aims at overcoming some deficiencies from previous approaches through mechanisms that support the handling of implementation for every structural concern separately and the handling of implementation for every data type separately. Moreover, TOSD contains operators which are orthogonal, that is, they can be used separately or as a combination, in order to perform composition of the program modules. We show the conceptual model of TOSD and describe a case study which consists in the development of a program to demonstrate more concretely how TOSD works in practice. We do not demonstrate the superiority of TOSD for the general case, but the results we have obtained suggest that TOSD is a promissing approach which deserves a deeper investigation in future research

Cette thèse introduit différentes méthodes de vérification (ou model-checking) sur des modèles de systèmes à pile. En effet, les systèmes à pile (pushdown systems) modélisent naturellement les programmes séquentiels grâce à une pile infinie qui peut simuler la pile d'appel du logiciel. La première partie de cette thèse se concentre sur la vérification sur des systèmes à pile de la logique HyperLTL, qui enrichit la logique temporelle LTL de quantificateurs universels et existentiels sur des variables de chemin. Il a été prouvé que le problème de la vérification de la logique HyperLTL sur des systèmes d'états finis est décidable ; nous montrons que ce problème est en revanche indécidable pour les systèmes à pile ainsi que pour la sous-classe des systèmes à pile visibles (visibly pushdown systems). Nous introduisons donc des algorithmes d'approximation de ce problème, que nous appliquons ensuite à la vérification de politiques de sécurité. Dans la seconde partie de cette thèse, dans la mesure où la représentation de la pile d'appel par les systèmes à pile est approximative, nous introduisons les systèmes à surpile (pushdown systems with an upper stack) ; dans ce modèle, les symboles retirés de la pile d'appel persistent dans la zone mémoire au dessus du pointeur de pile, et peuvent être plus tard écrasés par des appels sur la pile. Nous montrons que les ensembles de successeurs post* et de prédécesseurs pre* d'un ensemble régulier de configurations ne sont pas réguliers pour ce modèle, mais que post* est toutefois contextuel (context-sensitive), et que l'on peut ainsi décider de l'accessibilité d'une configuration. Nous introduisons donc des algorithmes de sur-approximation de post* et de sous-approximation de pre*, que nous appliquons à la détection de débordements de pile et de manipulations nuisibles du pointeur de pile. Enfin, dans le but d'analyser des programmes avec plusieurs fils d'exécution, nous introduisons le modèle des réseaux à piles dynamiques synchronisés (synchronized dynamic pushdown networks), que l'on peut voir comme un réseau de systèmes à pile capables d'effectuer des changements d'états synchronisés, de créer de nouveaux systèmes à piles, et d'effectuer des actions internes sur leur pile. Le problème de l'accessibilité étant naturellement indécidable pour un tel modèle, nous calculons une abstraction des chemins d'exécutions entre deux ensembles réguliers de configurations. Nous appliquons ensuite cette méthode à un processus itératif de raffinement des abstractions. / In this thesis, we propose different model-checking techniques for pushdown system models. Pushdown systems (PDSs) are indeed known to be a natural model for sequential programs, as they feature an unbounded stack that can simulate the assembly stack of an actual program. Our first contribution consists in model-checking the logic HyperLTL that adds existential and universal quantifiers on path variables to LTL against pushdown systems (PDSs). The model-checking problem of HyperLTL has been shown to be decidable for finite state systems. We prove that this result does not hold for pushdown systems nor for the subclass of visibly pushdown systems. Therefore, we introduce approximation algorithms for the model-checking problem, and show how these can be used to check security policies. In the second part of this thesis, as pushdown systems can fail to accurately represent the way an assembly stack actually operates, we introduce pushdown systems with an upper stack (UPDSs), a model where symbols popped from the stack are not destroyed but instead remain just above its top, and may be overwritten by later push rules. We prove that the sets of successors post* and predecessors pre* of a regular set of configurations of such a system are not always regular, but that post* is context-sensitive, hence, we can decide whether a single configuration is forward reachable or not. We then present methods to overapproximate post* and under-approximate pre*. Finally, we show how these approximations can be used to detect stack overflows and stack pointer manipulations with malicious intent. Finally, in order to analyse multi-threaded programs, we introduce in this thesis a model called synchronized dynamic pushdown networks (SDPNs) that can be seen as a network of pushdown processes executing synchronized transitions, spawning new pushdown processes, and performing internal pushdown actions. The reachability problem for this model is obviously undecidable. Therefore, we compute an abstraction of the execution paths between two regular sets of configurations. We then apply this abstraction framework to a iterative abstraction refinement scheme.