Opinion et curiosités Touchant la mathématique

UANL

La convergence de la sécurité informatique et de la protection des renseignements personnels : vers une nouvelle approche juridique

"Mémoire présenté à la Faculté des études supérieures en vue de l'obtention du grade de maîtrise en droit (LL.M.) option Nouvelles technologies de l'information"

Évolution des systèmes quantiques ouverts : décohérence et informatique quantique

Ce travail de maîtrise a mené à la rédaction d'un article (Physical Review A 80, 062319 (2009)).

Un formalisme pour la traçabilité des transformations

Dans le développement logiciel en industrie, les documents de spécification jouent un rôle important pour la communication entre les analystes et les développeurs. Cependant, avec le temps, les changements de personel et les échéances toujours plus courtes, ces documents sont souvent obsolètes ou incohérents avec l'état effectif du système, i.e., son code source. Pourtant, il est nécessaire que les composants du système logiciel soient conservés à jour et cohérents avec leurs documents de spécifications pour faciliter leur développement et maintenance et, ainsi, pour en réduire les coûts. Maintenir la cohérence entre spécification et code source nécessite de pouvoir représenter les changements sur les uns et les autres et de pouvoir appliquer ces changements de manière cohérente et automatique. Nous proposons une solution permettant de décrire une représentation d'un logiciel ainsi qu'un formalisme mathématique permettant de décrire et de manipuler l'évolution des composants de ces représentations. Le formalisme est basé sur les triplets de Hoare pour représenter les transformations et sur la théorie des groupes et des homomorphismes de groupes pour manipuler ces transformations et permettrent leur application sur les différentes représentations du système. Nous illustrons notre formalisme sur deux représentations d'un système logiciel : PADL, une représentation architecturale de haut niveau (semblable à UML), et JCT, un arbre de syntaxe abstrait basé sur Java. Nous définissons également des transformations représentant l'évolution de ces représentations et la transposition permettant de reporter les transformations d'une représentation sur l'autre. Enfin, nous avons développé et décrivons brièvement une implémentation de notre illustration, un plugiciel pour l'IDE Eclipse détectant les transformations effectuées sur le code par les développeurs et un générateur de code pour l'intégration de nouvelles représentations dans l'implémentation.

Timing verification in transaction modeling

Les systèmes Matériels/Logiciels deviennent indispensables dans tous les aspects de la vie quotidienne. La présence croissante de ces systèmes dans les différents produits et services incite à trouver des méthodes pour les développer efficacement. Mais une conception efficace de ces systèmes est limitée par plusieurs facteurs, certains d'entre eux sont: la complexité croissante des applications, une augmentation de la densité d'intégration, la nature hétérogène des produits et services, la diminution de temps d’accès au marché. Une modélisation transactionnelle (TLM) est considérée comme un paradigme prometteur permettant de gérer la complexité de conception et fournissant des moyens d’exploration et de validation d'alternatives de conception à des niveaux d’abstraction élevés. Cette recherche propose une méthodologie d’expression de temps dans TLM basée sur une analyse de contraintes temporelles. Nous proposons d'utiliser une combinaison de deux paradigmes de développement pour accélérer la conception: le TLM d'une part et une méthodologie d’expression de temps entre différentes transactions d’autre part. Cette synergie nous permet de combiner dans un seul environnement des méthodes de simulation performantes et des méthodes analytiques formelles. Nous avons proposé un nouvel algorithme de vérification temporelle basé sur la procédure de linéarisation des contraintes de type min/max et une technique d'optimisation afin d'améliorer l'efficacité de l'algorithme. Nous avons complété la description mathématique de tous les types de contraintes présentées dans la littérature. Nous avons développé des méthodes d'exploration et raffinement de système de communication qui nous a permis d'utiliser les algorithmes de vérification temporelle à différents niveaux TLM. Comme il existe plusieurs définitions du TLM, dans le cadre de notre recherche, nous avons défini une méthodologie de spécification et simulation pour des systèmes Matériel/Logiciel basée sur le paradigme de TLM. Dans cette méthodologie plusieurs concepts de modélisation peuvent être considérés séparément. Basée sur l'utilisation des technologies modernes de génie logiciel telles que XML, XSLT, XSD, la programmation orientée objet et plusieurs autres fournies par l’environnement .Net, la méthodologie proposée présente une approche qui rend possible une réutilisation des modèles intermédiaires afin de faire face à la contrainte de temps d’accès au marché. Elle fournit une approche générale dans la modélisation du système qui sépare les différents aspects de conception tels que des modèles de calculs utilisés pour décrire le système à des niveaux d’abstraction multiples. En conséquence, dans le modèle du système nous pouvons clairement identifier la fonctionnalité du système sans les détails reliés aux plateformes de développement et ceci mènera à améliorer la "portabilité" du modèle d'application.

Analyse de la corrélation conditionnelle dérivée de la coévolution d’un système de trois gènes par un modèle du maximum de vraisemblance

Les gènes codant pour des protéines peuvent souvent être regroupés et intégrés en modules fonctionnels par rapport à un organelle. Ces modules peuvent avoir des composantes qui suivent une évolution corrélée pouvant être conditionnelle à un phénotype donné. Les gènes liés à la motilité possèdent cette caractéristique, car ils se suivent en cascade en réponse à des stimuli extérieurs. L’hyperthermophilie, d’autre part, est interreliée à la reverse gyrase, cependant aucun autre élément qui pourrait y être associé avec certitude n’est connu. Ceci peut être dû à un déplacement de gènes non orthologues encore non résolu. En utilisant une approche bio-informatique, une modélisation mathématique d’évolution conditionnelle corrélée pour trois gènes a été développée et appliquée sur des profils phylétiques d’archaea. Ceci a permis d’établir des théories quant à la fonction potentielle du gène du flagelle FlaD/E ainsi que l’histoire évolutive des gènes lui étant liés et ayant contribué à sa formation. De plus, une histoire évolutive théorique a été établie pour une ligase liée à l’hyperthermophilie.

Automaticité dans le coeur ischémique : analyse de bifurcation d’un modèle mathématique de cellule ventriculaire humaine

L’ischémie aigüe (restriction de la perfusion suite à l’infarctus du myocarde) induit des changements majeurs des propriétés électrophysiologique du tissu ventriculaire. Dans la zone ischémique, on observe une augmentation du potassium extracellulaire qui provoque l’élévation du potentiel membranaire et induit un "courant de lésion" circulant entre la zone affectée et saine. Le manque d’oxygène modifie le métabolisme des cellules et diminue la production d’ATP, ce qui entraîne l’ouverture de canaux potassique ATP-dépendant. La tachycardie, la fibrillation ventriculaire et la mort subite sont des conséquences possibles de l’ischémie. Cependant les mécanismes responsables de ces complications ne sont pas clairement établis. La création de foyer ectopique (automaticité), constitue une hypothèse intéressante expliquant la création de ses arythmies. Nous étudions l’effet de l’ischémie sur l’automaticité à l’aide d’un modèle mathématique de la cellule ventriculaire humaine (Ten Tusscher, 2006) et d’une analyse exhaustive des bifurcations en fonction de trois paramètres : la concentration de potassium extracellulaire, le "courant de lésion" et l’ouverture de canaux potassiques ATP-dépendant. Dans ce modèle, nous trouvons que seule la présence du courant de lésion peut entrainer une activité automatique. Les changements de potassium extracellulaire et du courant potassique ATP-dépendant altèrent toutefois la structure de bifurcation.

Là où il y a des gènes, il y a du plaisir: réalisation et évaluation d’une formation en bio-informatique

La consultation de bases de données publiques en bio-informatique est essentielle pour quiconque a un intérêt pour la biologie cellulaire, la génétique ou la biologie des systèmes. Les notices de ces bases contiennent surtout des données spécialisées: séquences de nucléotides ou d’acides aminés, structures de protéines en trois dimensions, ou encore composantes de sentiers biologiques. Cependant, il peut être difficile de localiser l’information souhaitée parmi les centaines de bases de données disponibles. La Bibliothèque de la santé de l’Université de Montréal offre depuis janvier 2010 une activité de découverte des bases de données du National Center for Biotechnology Information; on y explore une vingtaine de bases et d’outils à l’aide d’exercices pratiques. Les moyens utilisés pour réaliser, publiciser et évaluer cette nouvelle activité de formation seront présentés.

La logique et les logiques : la question du pluralisme

Partant des travaux séminaux de Boole, Frege et Russell, le mémoire cherche à clarifier l‟enjeu du pluralisme logique à l‟ère de la prolifération des logiques non-classiques et des développements en informatique théorique et en théorie des preuves. Deux chapitres plus « historiques » sont à l‟ordre du jour : (1) le premier chapitre articule l‟absolutisme de Frege et Russell en prenant soin de montrer comment il exclut la possibilité d‟envisager des structures et des logiques alternatives; (2) le quatrième chapitre expose le chemin qui mena Carnap à l‟adoption de la méthode syntaxique et du principe de tolérance, pour ensuite dégager l‟instrumentalisme carnapien en philosophie de la Logique et des mathématiques. Passant par l‟analyse d‟une interprétation intuitive de la logique linéaire, le deuxième chapitre se tourne ensuite vers l‟établissement d‟une forme logico-mathématique de pluralisme logique à l‟aide de la théorie des relations d‟ordre et la théorie des catégories. Le troisième chapitre délimite le terrain de jeu des positions entourant le débat entre monisme et pluralisme puis offre un argument contre la thèse qui veut que le conflit entre logiques rivales soit apparent, le tout grâce à l‟utilisation du point de vue des logiques sous-structurelles. Enfin, le cinquième chapitre démontre que chacune des trois grandes approches au concept de conséquence logique (modèle-théorétique, preuve-théorétique et dialogique) forme un cadre suffisamment général pour établir un pluralisme. Bref, le mémoire est une défense du pluralisme logique.

Les infractions portant atteinte à la sécurité du système informatique d’une entreprise

Les nouvelles technologies de l’information et des communications occupent aujourd’hui une place importante dans les entreprises, quelle que soit la taille ou le(s) domaine(s) d’activité de ces dernières. Elles participent de manière positive au développement de la vie économique. Elles sont toutefois à l’origine d’une nouvelle forme de criminalité qui menace la sécurité et l’intégrité des systèmes informatiques dans l’entreprise. Celle-ci est d’une ampleur difficile à évaluer, mais surtout difficile à maîtriser avec les dispositions législatives déjà en place, laissant par là même apparaître qu’une adaptation au niveau juridique est inévitable. Certains pays industrialisés ont ainsi décidé de mettre en place un cadre juridique adéquat pour garantir aux entreprises la sécurité de leurs systèmes informatiques. Notre étude va justement porter sur les dispositifs mis en place par deux systèmes juridiques différents. Forcés de prendre en compte une réalité nouvelle – qui n’existait pas nécessairement il y a plusieurs années –, la France et le Canada ont décidé de modifier respectivement leurs codes pénal et criminel en leur ajoutant des dispositions qui répriment de nouvelles infractions. À travers cet exposé, nous allons analyser les infractions qui portent atteinte à la sécurité du système informatique de l’entreprise à la lumière des outils juridiques mis en place. Nous allons mesurer leur degré d’efficacité face à la réalité informatique. En d’autres termes, il s’agit pour nous de déterminer si le droit va répondre ou non aux besoins de l’informatique.

Conception d'un outil informatique basé sur un réseau de neurones artificiels pour la classification automatique des stades du sommeil

L’objectif de notre travail est de développer un outil d’analyse automatique des stades du sommeil basé sur les réseaux de neurones artificiels (RNA). Dans ce papier nous présentons notre démarche pour la conception de cet outil. La première difficulté consiste dans le choix de la représentation des signaux physiologiques et en particulier de l’électroencéphalogramme (EEG). Une fois la représentation adoptée, l’étape suivante est la conception du réseau de neurones optimal déterminé par un processus d’apprentissage et de validation sur les données issues d’un ensemble d'enregistrements de nuits de sommeil. Le résultat obtenu avec un taux de 63% de bonne classification pour six stades, nous incite à approfondir l’étude de cette problématique aux niveaux représentation et conception pour améliorer les performances de notre outil.

Identification de nouveaux substrats des kinases Erk1/2 par une approche bio-informatique, pharmacologique et phosphoprotéomique

La phosphorylation est une modification post-traductionnelle omniprésente des protéines Cette modification est ajoutée et enlevée par l’activité enzymatique respective des protéines kinases et phosphatases. Les kinases Erk1/2 sont au cœur d’une voie de signalisation importante qui régule l’activité de protéines impliquées dans la traduction, le cycle cellulaire, le réarrangement du cytosquelette et la transcription. Ces kinases sont aussi impliquées dans le développement de l’organisme, le métabolisme du glucose, la réponse immunitaire et la mémoire. Différentes pathologies humaines comme le diabète, les maladies cardiovasculaires et principalement le cancer, sont associées à une perturbation de la phosphorylation sur les différents acteurs de cette voie. Considérant l’importance biologique et clinique de ces deux kinases, connaître l’étendue de leur activité enzymatique pourrait mener au développement de nouvelles thérapies pharmacologiques. Dans ce contexte, l’objectif principal de cette thèse était de mesurer l’influence de cette voie sur le phosphoprotéome et de découvrir de nouveaux substrats des kinases Erk1/2. Une étude phosphoprotéomique de cinétique d’inhibition pharmacologique de la voie de signalisation Erk1/2 a alors été entreprise. Le succès de cette étude était basé sur trois technologies clés, soit l’enrichissement des phosphopeptides avec le dioxyde de titane, la spectrométrie de masse haut débit et haute résolution, et le développement d’une plateforme bio-informatique nommée ProteoConnections. Cette plateforme permet d’organiser les données de protéomique, évaluer leur qualité, indiquer les changements d’abondance et accélérer l’interprétation des données. Une fonctionnalité distinctive de ProteoConnections est l’annotation des sites phosphorylés identifiés (kinases, domaines, structures, conservation, interactions protéiques phospho-dépendantes). Ces informations ont été essentielles à l’analyse des 9615 sites phosphorylés sur les 2108 protéines identifiées dans cette étude, soit le plus large ensemble rapporté chez le rat jusqu’à ce jour. L’analyse des domaines protéiques a révélé que les domaines impliqués dans les interactions avec les protéines, les acides nucléiques et les autres molécules sont les plus fréquemment phosphorylés et que les sites sont stratégiquement localisés pour affecter les interactions. Un algorithme a été implémenté pour trouver les substrats potentiels des kinases Erk1/2 à partir des sites identifiés selon leur motif de phosphorylation, leur cinétique de stimulation au sérum et l’inhibition pharmacologique de Mek1/2. Une liste de 157 substrats potentiels des kinases Erk1/2 a ainsi été obtenue. Parmi les substrats identifiés, douze ont déjà été rapportés et plusieurs autres ont des fonctions associées aux substrats déjà connus. Six substrats (Ddx47, Hmg20a, Junb, Map2k2, Numa1, Rras2) ont été confirmés par un essai kinase in vitro avec Erk1. Nos expériences d’immunofluorescence ont démontré que la phosphorylation de Hmg20a sur la sérine 105 par Erk1/2 affecte la localisation nucléocytoplasmique de cette protéine. Finalement, les phosphopeptides isomériques positionnels, soit des peptides avec la même séquence d’acides aminés mais phosphorylés à différentes positions, ont été étudiés avec deux nouveaux algorithmes. Cette étude a permis de déterminer leur fréquence dans un extrait enrichi en phosphopeptides et d’évaluer leur séparation par chromatographie liquide en phase inverse. Une stratégie analytique employant un des algorithmes a été développée pour réaliser une analyse de spectrométrie de masse ciblée afin de découvrir les isomères ayant été manqués par la méthode d’analyse conventionnelle.

Analyse de descendances : une approche bio-informatique pour estimer le risque d'hypertension et d'obésité

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

Problématique de l'apprentissage de la mathématique en pédagogie du projet

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

Les processus additifs markoviens et leurs applications en finance mathématique

Cette thèse porte sur les questions d'évaluation et de couverture des options dans un modèle exponentiel-Lévy avec changements de régime. Un tel modèle est construit sur un processus additif markovien un peu comme le modèle de Black- Scholes est basé sur un mouvement Brownien. Du fait de l'existence de plusieurs sources d'aléa, nous sommes en présence d'un marché incomplet et ce fait rend inopérant les développements théoriques initiés par Black et Scholes et Merton dans le cadre d'un marché complet. Nous montrons dans cette thèse que l'utilisation de certains résultats de la théorie des processus additifs markoviens permet d'apporter des solutions aux problèmes d'évaluation et de couverture des options. Notamment, nous arrivons à caracté- riser la mesure martingale qui minimise l'entropie relative à la mesure de probabilit é historique ; aussi nous dérivons explicitement sous certaines conditions, le portefeuille optimal qui permet à un agent de minimiser localement le risque quadratique associé. Par ailleurs, dans une perspective plus pratique nous caract érisons le prix d'une option Européenne comme l'unique solution de viscosité d'un système d'équations intégro-di érentielles non-linéaires. Il s'agit là d'un premier pas pour la construction des schémas numériques pour approcher ledit prix.