Un cadre formel pour le développement orienté aspect : modélisation et vérification des interactions dues aux aspects

Thèse numérisée par la Division de la gestion de documents et des archives de l'Université de Montréal

Analyse des traces d'exécution pour la vérification des protocoles d'interaction dans les systèmes multiagents

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

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

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

Application du concept des transactions pour la modélisation et la simulation multicoeur des systèmes sur puce

Avec la complexité croissante des systèmes sur puce, de nouveaux défis ne cessent d’émerger dans la conception de ces systèmes en matière de vérification formelle et de synthèse de haut niveau. Plusieurs travaux autour de SystemC, considéré comme la norme pour la conception au niveau système, sont en cours afin de relever ces nouveaux défis. Cependant, à cause du modèle de concurrence complexe de SystemC, relever ces défis reste toujours une tâche difficile. Ainsi, nous pensons qu’il est primordial de partir sur de meilleures bases en utilisant un modèle de concurrence plus efficace. Par conséquent, dans cette thèse, nous étudions une méthodologie de conception qui offre une meilleure abstraction pour modéliser des composants parallèles en se basant sur le concept de transaction. Nous montrons comment, grâce au raisonnement simple que procure le concept de transaction, il devient plus facile d’appliquer la vérification formelle, le raffinement incrémental et la synthèse de haut niveau. Dans le but d’évaluer l’efficacité de cette méthodologie, nous avons fixé l’objectif d’optimiser la vitesse de simulation d’un modèle transactionnel en profitant d’une machine multicoeur. Nous présentons ainsi l’environnement de modélisation et de simulation parallèle que nous avons développé. Nous étudions différentes stratégies d’ordonnancement en matière de parallélisme et de surcoût de synchronisation. Une expérimentation faite sur un modèle du transmetteur Wi-Fi 802.11a a permis d’atteindre une accélération d’environ 1.8 en utilisant deux threads. Avec 8 threads, bien que la charge de travail des différentes transactions n’était pas importante, nous avons pu atteindre une accélération d’environ 4.6, ce qui est un résultat très prometteur.

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.

Algorithmique et complexité des systèmes à compteurs

Réalisé en cotutelle avec l'École normale supérieure de Cachan – Université Paris-Saclay

L'Hypothèse des déficits jumeaux: vérification dans le cadre de pays de la Caraïbe.

Rapport de recherche

Le modèle de convergence vu selon l'approche de Dan, Ben-David: une vérification empirique par rapport au 8e cycle du GATT; le cas de l'ALENA versus l'Union Européenne (période 1970-2000).

Rapport de recherche

Changement structurel en Haïti, une vérification empirique.

Rapport de recherche

L’allocation d’antiviraux dans un contexte de pandémie : vérification de critères auprès des professionnels de la santé pour le développement d’un cadre éthique

Cette étude a pour objectif d’évaluer la stratégie d’utilisation de critères de base, d’un point de vue éthique, dans l’allocation d’une quantité limitée d’antiviraux pour une utilisation préventive, lors d’une pandémie. Il est entendu qu’une réserve publique pour la prévention n’est pas présentement en vue. Ainsi un des objectifs de cette recherche est de servir de guide aux personnes ressources en positions décisionnelles, à savoir si l’acquisition d’une telle réserve est justifiée, et dans l’affirmatif, à qui elle serait destinée. La perspective spécifique de deux groupes de professionnels de la santé œuvrant en première ligne est considérée. Le premier groupe est constitué de professionnels provenant des hôpitaux de la région de Toronto qui ont vécu l’expérience du SRAS en 2003. Le second groupe est composé de travailleurs en santé de la région de Montréal qui n’auront pas vécu cette crise sanitaire. Les deux groupes sont analysés ensemble sur leur discours verbal et sur leurs réponses à un questionnaire bâti afin d’évaluer quel poids les participants donnent aux critères proposés.

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).

Vérification des liens entre les stresseurs, le soutien social, la santé psychologique au travail et la qualité de la relation élève-enseignant

La relation élève-enseignant (REE) est reconnue comme étant optimale lorsqu’elle est fortement chaleureuse et faiblement conflictuelle. Sur le plan empirique, plusieurs évidences montrent que la qualité de la REE est liée significativement à divers indicateurs de la réussite scolaire. De façon générale, celles-ci affirment que plus un élève entretient une relation optimale avec son enseignant, plus ses résultats scolaires sont élevés, plus il adopte des comportements prosociaux, et plus il présente des affects et des comportements positifs envers l’école. Des études précisent également que l’influence de la qualité de la REE est particulièrement importante chez les élèves à risque. Si les effets positifs d’une REE optimale sont bien connus, les facteurs favorisant son émergence sont quant à eux moins bien compris. En fait, bien que certains attributs personnels de l’élève ou de l’enseignant aient été identifiés comme participant significativement à la qualité de la REE, peu d’études ont investigué l’importance des facteurs psychologiques et contextuels dans l’explication de ce phénomène. Souhaitant pallier cette lacune, la présente étude poursuit trois objectifs qui sont: 1) d’examiner les liens entre les stresseurs, le soutien social, la santé psychologique au travail (SPT) et la qualité de la REE; 2) de vérifier l’effet médiateur de la SPT dans la relation entre les stresseurs, le soutien social et la qualité de la REE, et; 3) d’examiner les différences quant aux liens répertoriés auprès d’élèves réguliers et à risque. Afin d’atteindre ces objectifs, 231 enseignants québécois de niveau préscolaire et primaire ont été investigués. Les résultats des analyses montrent que les comportements perturbateurs des élèves en classe prédisent positivement le conflit entre l’enseignant et les élèves à risque. Ils montrent également que le soutien des parents et le soutien du supérieur prédisent respectivement la présence de REE chaleureuses chez les élèves réguliers et à risque. La SPT de l’enseignant prédit quant à elle positivement la présence de REE chaleureuses et négativement la présence de REE conflictuelles. Les résultats de cette recherche montrent aussi que le soutien social affecte indirectement la présence de REE chaleureuses par le biais de la SPT de l’enseignant.

Vérification temporelle des systèmes cycliques et acycliques basée sur l’analyse des contraintes

Nous présentons une nouvelle approche pour formuler et calculer le temps de séparation des événements utilisé dans l’analyse et la vérification de différents systèmes cycliques et acycliques sous des contraintes linéaires-min-max avec des composants ayant des délais finis et infinis. Notre approche consiste à formuler le problème sous la forme d’un programme entier mixte, puis à utiliser le solveur Cplex pour avoir les temps de séparation entre les événements. Afin de démontrer l’utilité en pratique de notre approche, nous l’avons utilisée pour la vérification et l’analyse d’une puce asynchrone d’Intel de calcul d’équations différentielles. Comparée aux travaux précédents, notre approche est basée sur une formulation exacte et elle permet non seulement de calculer le maximum de séparation, mais aussi de trouver un ordonnancement cyclique et de calculer les temps de séparation correspondant aux différentes périodes possibles de cet ordonnancement.

Système de listes de vérification interactives du niveau de conformité des maquettes avec les recommandations des fabricants de plateformes mobiles

L'ensemble de mon travail a été réalisé grâce a l'utilisation de logiciel libre.