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.

Un modèle de validation automatique de mécanismes de sécurisation des communications

Mémoire numérisé par la Direction des bibliothèques de l'Université de Montréal.

Synthèse formelle de l’hormaomycine et de la bélactosine A par utilisation d’une réaction de cyclopropanation intramoléculaire catalysée par un complexe de rhodium (II)

Ce mémoire présente trois approches différentes vers la synthèse du 3–(trans–2–nitrocyclopropyl)alanine, un intermédiaire synthétique de la hormaomycine. Cette molécule naturelle démontre d’intéressantes activités biologiques et pharmacologiques. Il est intéressant de souligner que ce dérivé donne facilement accès au 3–(trans–2–aminocyclopropyl)alanine, unité centrale de la bélactosine A. Ce composé naturel possédant lui aussi d’intéressantes propriétés biologiques, plusieurs études relationnelles structures-activités menant à des dérivés plus actifs de cette molécule ont été entreprises, démontrant l’intérêt toujours présent de synthétiser de façon efficace et optimale ces dérivés cyclopropaniques. Une méthodologie développée au sein de notre groupe de recherche et basée sur une réaction de cyclopropanation intramoléculaire diastéréosélective sera mise à profit afin d’élaborer une nouvelle voie de synthèse aussi élégante qu’efficace à la construction du 3–(trans–2–nitrocyclopropyl) alanine. En utilisant un carbène de rhodium généré soit par la dégradation d’un dérivé diazoïque, soit par la formation d’un réactif de type ylure d’iodonium, une réaction de cyclopropanation diastéréosélective permettra la formation de deux autres centres contigus et ce, sans même utiliser d’auxiliaire ou de catalyseur énantioenrichis. Ensuite, un réarrangement intramoléculaire précédant deux réactions synchronisées d’ouverture de cycle et de décarboxylation permettront l’obtention du composé d’intérêt avec un rendement global convenable et en relativement peu d’étapes. De cette manière, la synthèse formelle de la bélactosine A et de l’hormaomycine a été effectuée. Cette synthèse se démarque des autres par l’utilisation d’une seule transformation catalytique énantiosélective.

La plasticité cérébrale dans le vieillissement normal : effet de l’éducation formelle et de l’entraînement cognitif sur les mesures de potentiels évoqués

Le vieillissement normal est souvent associé à des changements cognitifs négatifs, notamment sur les performances cognitives. Cependant, des changements comportementaux et cérébraux positifs ont aussi été observés. Ces modifications indiquent l’existence d’une plasticité cérébrale dans le vieillissement normal. Ainsi, plusieurs facteurs ont été étudiés afin de mieux connaitre les modulateurs de cette plasticité dite positive. La plupart des études évaluant ce phénomène ont utilisé la technique d’imagerie par résonance magnétique alors que la technique des potentiels évoqués a été beaucoup moins utilisée. Cette technique est basée sur les enregistrements de l’activité électrique cérébrale très sensible aux changements anatomiques associés au vieillissement et permet donc d’observer de manière précise les variations du décours temporel des ondes éléctrophysiologiques lors du traitement des informations. Les travaux de cette thèse visent à étudier les modifications de plasticité cérébrale induites par des facteurs protecteurs/préventifs du vieillissement normal et notamment lors de la réalisation de tâches impliquant le contrôle attentionnel, grâce à l’analyse de signaux électroencéphalographiques en potentiels évoqués. Dans un premier temps, une description de l’analyse des données EEG en potentiels évoqués sera fournie, suivie d’une revue de littérature sur le contrôle attentionnel et les facteurs de plasticité dans le vieillissement normal (Chapitre 1). Cette revue de littérature mettra en avant, d’une part la diminution des capacités de contrôle de l’attention dans le vieillissement et d’autre part, les facteurs protecteurs du vieillissement ainsi que la plasticité cérébrale qui leur est associée. Ces facteurs sont connus pour avoir un effet positif sur le déficit lié à l’âge. La première étude de ce projet (Chapitre 2) vise à définir l’effet d’un facteur de réserve cognitive, le niveau d’éducation, sur les composantes des potentiels évoqués chez les personnes âgées. Cette étude mettra en avant une composante des potentiels évoqués, la P200, comme indice de plasticité lorsqu’elle est liée au niveau d’éducation. Cet effet sera observé sur deux tâches expérimentales faisant intervenir des processus de contrôle attentionnel. De plus, une différence d’épaisseur corticale sera observée : les personnes âgées ayant un plus haut niveau d’éducation ont un cortex cingulaire antérieur plus épais. La deuxième étude (Chapitre 3) cherche à déterminer, chez les personnes âgées, les modifications comportementales et en potentiels évoqués induites par trois entraînements cognitifs, entrainements visant l’amélioration de processus attentionnels différents : l’attention focalisée, l’attention divisée, ainsi que la modulation de l’attention. Au niveau comportemental, les entraînements induisent tous une amélioration des performances. Cependant, l’entraînement en modulation de l’attention est le seul à induire une amélioration du contrôle attentionnel. Les résultats éléctrophysiologiques indiquent la N200 comme composante sensible à la plasticité cérébrale à la suite d’entraînements cognitifs. L’entraînement en modulation de l’attention est le seul à induire une modification de cette composante dans toutes les conditions des tests. Les résultats de ces études suggèrent que les facteurs protecteurs du vieillissement permettent des changements positifs observés en potentiels évoqués. En effet, nous mettons en évidence des phénomènes de plasticité cérébrale des personnes âgées qui diffèrent selon leurs origines. L’impact de ces résultats ainsi que les limites et perspectives futures seront présentés en fin de thèse (Chapitre 4).

Le portail de Notre-Dame de Vermenton : étude formelle et iconographique de la sculpture de la deuxième moitié du XIIe siècle

Mémoire numérisé par la Division de la gestion de documents et des archives de l'Université de Montréal

La stratégie sénégalaise du faire faire et la construction du sens de la gouvernance de l’éducation non formelle

Traduction du titre en anglais: Making sense of governance in non-formal education : A critical analysis of the Senegalese faire faire strategy

Incidence des développements du paramètre harmonique sur la périodisation et la structuration formelle des mélodies de Serge Garant.

La version intégrale de ce mémoire est disponible uniquement pour consultation individuelle à la Bibliothèque de musique de l’Université de Montréal (www.bib.umontreal.ca/MU).

Histoire formelle du jeu d’aventure sur ordinateur (le cas de l’Amérique du Nord de 1976-1999)

Cette étude s’intéresse à l’évolution formelle du jeu d’aventure de 1976 à 1999. Elle se propose de mieux comprendre les facteurs historiques contribuant à l’apparition du genre, son institution et ses transformations. La recherche est fondée sur l’analyse du discours de la presse spécialisée en jeux d’ordinateur et d’un corpus étendu d’œuvres. L’une des thèses proposées est que l’identité générique du jeu d’aventure est fondée sur une expérience vidéoludique demeurant relativement constante malgré des variations importantes de formes. Cette expérience est assurée par la reproduction des principaux éléments d’une architecture générale de design de jeu inaugurée par Adventure en 1977. Les variations formelles ponctuelles résultent d’une négociation entre la volonté de s’adapter aux changements de contexte de l’écologie du jeu d’ordinateur et la résistance d’une architecture ludique établie. La pertinence d’une histoire d’un genre vidéoludique est justifiée au premier chapitre en fonction de l’état actuel des connaissances sur l’histoire du jeu vidéo et du jeu d’aventure. On y précise également le cadre théorique, la méthodologie et les sources étudiées. Le deuxième chapitre s’intéresse à la genèse d’Adventure de Crowther et Woods (1976; 1977) en fonction des diverses pratiques culturelles dans lesquelles l’œuvre s’inscrit. Cette analyse permet d’en dégager l’architecture ludique. Le troisième chapitre porte sur le « tournant narratif » du jeu d’aventure ayant lieu au début des années 1980. On y décrit différents facteurs historiques poussant le genre vers l’enchâssement d’histoires pré-écrites afin d’en faire un véhicule narratif. Le quatrième chapitre décrit le contexte du « tournant graphique », passage du jeu d’aventure d’une représentation textuelle à un régime visuel, ainsi que ses conséquences expérientielles. Le « tournant ergonomique » décrit au cinquième chapitre traite de l’apparition du modèle « pointer et cliquer » en fonction des avancées des connaissances concernant les interactions humain-machine ainsi que de la maturation du design de jeu comme pratique autonome. Le dernier chapitre relate l’apogée du jeu d’aventure au début de la révolution multimédia sous ses formes de film interactif et « Myst-like » puis du ralentissement – voire de l’arrêt – de son évolution formelle.

Insertion socioprofessionnelle des sortants de la formation agricole non formelle sur le marché de l’emploi au Burkina Faso et importance accordée à la production céréalière : cas des sortants du centre de promotion rurale de Goundi

L'étude combine les méthodes qualitative et qualitative à travers l’utilisation du questionnaire et du canevas d’entrevue. Elle s’appuie sur un cadre conceptuel élaboré à partir de revue de littérature et de concepts clefs tels que : le capital social, le capital humain, l’identité personnelle, l’identité professionnelle et la socialisation, Les résultats déterminent le profil d’un céréalier indiquant son attachement aux valeurs professionnelles liées au transfert de ses connaissances, à la modernisation de l’exploitation, à la recherche de l’amélioration du rendement et à l’utilisation d’outils modernes.

Latent Variable Models for Stochastic Discount Factors.

Latent variable models in finance originate both from asset pricing theory and time series analysis. These two strands of literature appeal to two different concepts of latent structures, which are both useful to reduce the dimension of a statistical model specified for a multivariate time series of asset prices. In the CAPM or APT beta pricing models, the dimension reduction is cross-sectional in nature, while in time-series state-space models, dimension is reduced longitudinally by assuming conditional independence between consecutive returns, given a small number of state variables. In this paper, we use the concept of Stochastic Discount Factor (SDF) or pricing kernel as a unifying principle to integrate these two concepts of latent variables. Beta pricing relations amount to characterize the factors as a basis of a vectorial space for the SDF. The coefficients of the SDF with respect to the factors are specified as deterministic functions of some state variables which summarize their dynamics. In beta pricing models, it is often said that only the factorial risk is compensated since the remaining idiosyncratic risk is diversifiable. Implicitly, this argument can be interpreted as a conditional cross-sectional factor structure, that is, a conditional independence between contemporaneous returns of a large number of assets, given a small number of factors, like in standard Factor Analysis. We provide this unifying analysis in the context of conditional equilibrium beta pricing as well as asset pricing with stochastic volatility, stochastic interest rates and other state variables. We address the general issue of econometric specifications of dynamic asset pricing models, which cover the modern literature on conditionally heteroskedastic factor models as well as equilibrium-based asset pricing models with an intertemporal specification of preferences and market fundamentals. We interpret various instantaneous causality relationships between state variables and market fundamentals as leverage effects and discuss their central role relative to the validity of standard CAPM-like stock pricing and preference-free option pricing.

Exact Tests for Contemporaneous Correlation of Disturbances in Seemingly Unrelated Regressions.

This paper proposes finite-sample procedures for testing the SURE specification in multi-equation regression models, i.e. whether the disturbances in different equations are contemporaneously uncorrelated or not. We apply the technique of Monte Carlo (MC) tests [Dwass (1957), Barnard (1963)] to obtain exact tests based on standard LR and LM zero correlation tests. We also suggest a MC quasi-LR (QLR) test based on feasible generalized least squares (FGLS). We show that the latter statistics are pivotal under the null, which provides the justification for applying MC tests. Furthermore, we extend the exact independence test proposed by Harvey and Phillips (1982) to the multi-equation framework. Specifically, we introduce several induced tests based on a set of simultaneous Harvey/Phillips-type tests and suggest a simulation-based solution to the associated combination problem. The properties of the proposed tests are studied in a Monte Carlo experiment which shows that standard asymptotic tests exhibit important size distortions, while MC tests achieve complete size control and display good power. Moreover, MC-QLR tests performed best in terms of power, a result of interest from the point of view of simulation-based tests. The power of the MC induced tests improves appreciably in comparison to standard Bonferroni tests and, in certain cases, outperforms the likelihood-based MC tests. The tests are applied to data used by Fischer (1993) to analyze the macroeconomic determinants of growth.

Simulation-Based Finite-Sample Tests for Heteroskedasticity and ARCH Effects.

A wide range of tests for heteroskedasticity have been proposed in the econometric and statistics literature. Although a few exact homoskedasticity tests are available, the commonly employed procedures are quite generally based on asymptotic approximations which may not provide good size control in finite samples. There has been a number of recent studies that seek to improve the reliability of common heteroskedasticity tests using Edgeworth, Bartlett, jackknife and bootstrap methods. Yet the latter remain approximate. In this paper, we describe a solution to the problem of controlling the size of homoskedasticity tests in linear regression contexts. We study procedures based on the standard test statistics [e.g., the Goldfeld-Quandt, Glejser, Bartlett, Cochran, Hartley, Breusch-Pagan-Godfrey, White and Szroeter criteria] as well as tests for autoregressive conditional heteroskedasticity (ARCH-type models). We also suggest several extensions of the existing procedures (sup-type of combined test statistics) to allow for unknown breakpoints in the error variance. We exploit the technique of Monte Carlo tests to obtain provably exact p-values, for both the standard and the new tests suggested. We show that the MC test procedure conveniently solves the intractable null distribution problem, in particular those raised by the sup-type and combined test statistics as well as (when relevant) unidentified nuisance parameter problems under the null hypothesis. The method proposed works in exactly the same way with both Gaussian and non-Gaussian disturbance distributions [such as heavy-tailed or stable distributions]. The performance of the procedures is examined by simulation. The Monte Carlo experiments conducted focus on : (1) ARCH, GARCH, and ARCH-in-mean alternatives; (2) the case where the variance increases monotonically with : (i) one exogenous variable, and (ii) the mean of the dependent variable; (3) grouped heteroskedasticity; (4) breaks in variance at unknown points. We find that the proposed tests achieve perfect size control and have good power.

Logique et tests d'hypotheses: reflexions sur les problemes mal poses en econometrie

Dans ce texte, nous analysons les développements récents de l’économétrie à la lumière de la théorie des tests statistiques. Nous revoyons d’abord quelques principes fondamentaux de philosophie des sciences et de théorie statistique, en mettant l’accent sur la parcimonie et la falsifiabilité comme critères d’évaluation des modèles, sur le rôle de la théorie des tests comme formalisation du principe de falsification de modèles probabilistes, ainsi que sur la justification logique des notions de base de la théorie des tests (tel le niveau d’un test). Nous montrons ensuite que certaines des méthodes statistiques et économétriques les plus utilisées sont fondamentalement inappropriées pour les problèmes et modèles considérés, tandis que de nombreuses hypothèses, pour lesquelles des procédures de test sont communément proposées, ne sont en fait pas du tout testables. De telles situations conduisent à des problèmes statistiques mal posés. Nous analysons quelques cas particuliers de tels problèmes : (1) la construction d’intervalles de confiance dans le cadre de modèles structurels qui posent des problèmes d’identification; (2) la construction de tests pour des hypothèses non paramétriques, incluant la construction de procédures robustes à l’hétéroscédasticité, à la non-normalité ou à la spécification dynamique. Nous indiquons que ces difficultés proviennent souvent de l’ambition d’affaiblir les conditions de régularité nécessaires à toute analyse statistique ainsi que d’une utilisation inappropriée de résultats de théorie distributionnelle asymptotique. Enfin, nous soulignons l’importance de formuler des hypothèses et modèles testables, et de proposer des techniques économétriques dont les propriétés sont démontrables dans les échantillons finis.

Wage Policy of Firms: an Empirical Investigation.

This paper analyzes the dynamics of wages and workers' mobility within firms with a hierarchical structure of job levels. The theoretical model proposed by Gibbons and Waldman (1999), that combines the notions of human capital accumulation, job rank assignments based on comparative advantage and learning about workers' abilities, is implemented empirically to measure the importance of these elements in explaining the wage policy of firms. Survey data from the GSOEP (German Socio-Economic Panel) are used to draw conclusions on the common features characterizing the wage policy of firms from a large sample of firms. The GSOEP survey also provides information on the worker's rank within his firm which is usually not available in other surveys. The results are consistent with non-random selection of workers onto the rungs of a job ladder. There is no direct evidence of learning about workers' unobserved abilities but the analysis reveals that unmeasured ability is an important factor driving wage dynamics. Finally, job rank effects remain significant even after controlling for measured and unmeasured characteristics.