No description available.

La sécurité est un élément crucial dans le développement d'un système d'information. On ne peut pas concevoir un système bancaire sans préoccupation sécuritaire. La sensibilité des données d'un système hospitalier nécessite que la sécurité soit la composante majeure d'un tel logiciel. Le contrôle d'accès est un des nombreux aspects de la sécurité. Il permet de définir les conditions de l'exécution d'actions dans un système par un utilisateur. Entre les différentes phases de conception d'une politique de contrôle d'accès et son application effective sur un système déployé, de nombreuses étapes peuvent introduire des erreurs ou des failles non souhaitables. L'utilisation de méthodes formelles est une réponse à ces préoccupations dans le cadre de la modélisation de politiques de contrôle d'accès. L'algèbre de processus EB3 permet une modélisation formelle de systèmes d'information. Son extension EB3SEC a été conçue pour la spécification de politiques de contrôle d'accès. Le langage ASTD, combinaison des statecharts de Harel et des opérateurs de EB3, permet de modéliser graphiquement et formellement un système d'information. Cependant, ces deux méthodes manquent d'outils de vérification et de validation qui permettent de prouver ou de vérifier des propriétés de sécurité indispensables à la validation de politiques de contrôle d'accès. De plus, il est important de pouvoir prouver que l'implémentation d'une politique correspond bien à sa spécification abstraite. Cette thèse définit des règles de traduction de EB3 vers ASTD, d'ASTD vers event-B et vers B. Elle décrit également une architecture formelle exprimée en B d'un filtre de contrôle d'accès pour les systèmes d'information. Cette modélisation en B permet de prouver des propriétés à l'aide du prouveur B ou de vérifier des propriétés avec ProB, un vérificateur de modèles. Enfin, une stratégie de raffinement B pour obtenir une implémentation de ce filtre de contrôle d'accès est présentée. Les raffinements B étant prouvés, l'implémentation correspond donc au modèle initial de la politique de contrôle d'accès / Security is a key aspect in information systems (IS) development. One cannot build a bank IS without security in mind. In medical IS, security is one of the most important features of the software. Access control is one of many security aspects of an IS. It defines permitted or forbidden execution of system's actions by a user. Between the conception of an access control policy and its effective deployment on an IS, several steps can introduce unacceptable errors. Using formal methods may be an answer to reduce errors during the modeling of access control policies. Using the process algebra EB3, one can formally model IS. Its extension, EB3SEC, was created in order to model access control policies. The ASTD notation combines Harel's Statecharts and EB3 operators into a graphical and formal notation that can be used in order to model IS. However, both methods lack tools allowing a designer to prove or verify security properties in order to validate an access control policy. Furthermore, the implementation of an access control policy must correspond to its abstract specification. This thesis defines translation rules from EB3 to ASTD, from ASTD to event-B and from ASTD to B. It also introduces a formal architecture expressed using the B notation in order to enforce a policy over an IS. This modeling of access control policies in B can be used in order to prove properties, thanks to the B prover, but also to verify properties using ProB, a model checker for B. Finally, a refinement strategy for the access control policy into an implementation is proposed. B refinements are proved, this ensures that the implementation corresponds to the initial model of the access control policy

La sécurité est un élément crucial dans le développement d'un système d'information. On ne peut pas concevoir un système bancaire sans préoccupation sécuritaire. La sensibilité des données d'un système hospitalier nécessite que la sécurité soit la composante majeure d'un tel logiciel. Le contrôle d'accès est un des nombreux aspects de la sécurité. Il permet de définir les conditions de l'exécution d'actions dans un système par un utilisateur. Entre les différentes phases de conception d'une politique de contrôle d'accès et son application effective sur un système déployé, de nombreuses étapes peuvent introduire des erreurs ou des failles non souhaitables. L'utilisation de méthodes formelles est une réponse à ces préoccupations dans le cadre de la modélisation de politiques de contrôle d'accès. L'algèbre de processus EB3 permet une modélisation formelle de systèmes d'information. Son extension EB3SEC a été conçue pour la spécification de politiques de contrôle d'accès. Le langage ASTD, combinaison des statecharts de Harel et des opérateurs de EB3, permet de modéliser graphiquement et formellement un système d'information. Cependant, ces deux méthodes manquent d'outils de vérification et de validation qui permettent de prouver ou de vérifier des propriétés de sécurité indispensables à la validation de politiques de contrôle d'accès. De plus, il est important de pouvoir prouver que l'implémentation d'une politique correspond bien à sa spécification abstraite. Cette thèse définit des règles de traduction de EB3 vers ASTD, d'ASTD vers event-B et vers B. Elle décrit également une architecture formelle exprimée en B d'un filtre de contrôle d'accès pour les systèmes d'information. Cette modélisation en B permet de prouver des propriétés à l'aide du prouveur B ou de vérifier des propriétés avec ProB, un vérificateur de modèles. Enfin, une stratégie de raffinement B pour obtenir une implémentation de ce filtre de contrôle d'accès est présentée. Les raffinements B étant prouvés, l'implémentation correspond donc au modèle initial de la politique de contrôle d'accès

<p dir="ltr">Cancer biological mechanisms are a vastly researched area in the field, yet they are not well understood in the various contexts in which cancer is found. Cancerous tumors often exist in harsh, stressful environments for normal cells, but cancer cells can thrive in these conditions. The tumor microenvironment (TME) typically has low oxygen levels (hypoxia), high acidity, and low nutrition. Exposure to the TME leads to many metabolic changes in the cells, enabling cancer to continue proliferating and migrating. However, these metabolic changes are not well understood, especially at the single-cell level. The ability to monitor cells in real time to determine the physical characteristics they undergo is critical to understanding the impact of these metabolic changes. Conventional methods focus on determining the genomic and proteomic changes in large numbers of cells, which may be overlooked if the changes are homogeneous across samples. In this work, we demonstrate the power of using multiple imaging techniques in combination with biochemical methods to visualize metabolic changes and determine the causes in various cancer cells under extreme hypoxia conditions.</p><p dir="ltr">The changes in the microtubule network that occur under hypoxia at the single-cell level are not widely researched. The use of confocal fluorescence microscopy can determine microtubule polymerization in conjunction with eGFP-transfected EB3, a protein that assists in microtubule polymerization. We have determined that hypoxic HeLa cells produce finger-like protrusions when exposed to hypoxia that help with cell migration and, ultimately, cancer cell metastasis. The formation of these protrusions is facilitated by localized mitochondria activities in the protrusions.</p><p dir="ltr">The metabolic changes in lipid droplets (LDs) under hypoxia at the single-cell level remain an elusive topic. The use of stimulated Raman spectroscopy (SRS) and coherent anti-Stokes Raman scattering (CARS) can determine the quantity and spatial-temporal distribution of LDs in cancer cells. We have found that LDs redistribute to the endoplasmic reticulum (ER) and increase in intensity in hypoxic MIA PaCa-2 and A549 cells. Time-lapse CARS microscopy revealed a release-accumulate process of these LDs on ER in hypoxia. We also studied the impact of carbon sources on LD formation and found that MIA PaCa2 cells prefer direct lipid uptake while glucose is also essential to reduce lipotoxicity. The use of hyperspectral stimulated Raman scattering (hSRS) also reveals that the content of the LDs changes to include less cholesteryl ester and a decrease in lipid saturation level.</p><p dir="ltr">Collectively, these findings shed new light on the understanding of cytoskeleton dynamics and lipid metabolism in hypoxic conditions. The discoveries made within this research would lead to better treatment strategies for effective treatment of hypoxia-resistant cancer cells.</p>