Cette thèse a pour objectif de donner une définition générale et mesurable de la difficulté du gameplay dans un jeu vidéo. Elle propose une méthode et un outil pour mesurer cette difficulté. La méthode de mesure couramment employée est en effet principalement heuristique et propre au contexte de chaque jeu. Nous proposons une approche générique d'analyse du gameplay qui prend en compte l'apprentissage du joueur et permet une évaluation statistique de la difficulté d'un gameplay. Dans un premier temps, la thèse explore les liens entre difficulté, game design, et plaisir de jouer. Nous étudions diverses formes de difficultés : sensorielles, logiques et motrices. Après diverses expérimentations d'analyse automatique de gameplay, nous détaillons notre modèle de mesure de la difficulté, et l'analyse en challenges et capacités d'un gameplay, ainsi que le logiciel associé. Finalement, nous présentons une expérience, dont l'objectif est de tester la faisabilité et la précision de notre modèle.

L'informatique dans les nuages propose une alternative économique et performante au déploiement traditionnel sur site. Une utilisation efficace des nuages passe par une diminution des ressources consommées et une adaptation du déploiement à l'environnement cible. Nous proposons, dans cette thèse, une solution pour le déploiement de logiciels à la juste taille, c'est-à-dire en ne déployant que les dépendances nécessaires sur un environnement cible. Nous suivons une définition du déploiement basée sur les architectures à composants. Le contenu et les dépendances d'un logiciel sont capturés grâce au modèle à composants Fractal SoftwareUnit. Ce modèle offre une fine granularité de la représentation, le support de l'hétérogénéité des logiciels et des environnement cibles, ainsi qu'un contrôle distribué des logiciels. Nous proposons une mise en œuvre du modèle au travers du canevas SU Framework. Enfin, nous décrivons comment résoudre deux problèmes issus de besoins industriels, à l'aide de ce canevas : la définition de profils pour le serveur d'applications JOnAS et le déploiement d'applications hétérogènes sur cibles hétérogènes.

Ma thèse porte sur l'étude des couplages, et plus particulièrement leur utilisation en cryptographie. Mes premiers travaux ont portés sur l'arithmétique des couplages à travers une comparaison des complexités en nombre d'opérations des couplages de Weil et Tate. Puis je me suis intéressée à l'étude de l'arithmétique utile pour les couplages. Un de mes travaux propose d'utiliser une représentation alternative des corps finis pour améliorer l'efficacité des calculs impliqués dans les couplages. Le second étudie en détail l'arithmétique des couplages pour les courbes dont le degré d'enfoncement est 15. Ces premiers travaux m'ont permis de me familiariser avec les couplages et je me suis alors orientée vers la résistance aux attaques par canaux cachés des algorithmes de couplage. J'ai étudié les faiblesses de l'algorithme de Miller lorsqu'il subit des attaques par analyse de consommation de courant et par injection de fautes.

Cette thèse traite deux types de problèmes algorithmiques : des problèmes de triangularisation de matrices booléennes par permutation des lignes et des colonnes et des problèmes de découverte de structures secondaires d'ARN. Nous étudions des problèmes de triangularisation de matrices booléennes par permutation des lignes et des colonnes. Ce problème apparaît, par exemple, lorsque l'on souhaite calculer "en place" un système d'équations. Une façon naturelle d'aborder ce problème est de se placer dans le cadre général de la théorie des graphes et des graphes bipartis en particulier. Nous présentons de nombreux résultats de complexité - essentiellement de NP-complétude - liés à ce problème et introduisons quelques extensions dont nous précisons toujours la complexité. Certaines familles d'ARN sont très précisément définies par des motifs de séquence, et des contraintes structurelles secondaires et tertiaires. La plupart des outils ne sont pas adaptés puisqu'ils n'intègrent pas toutes les connaissances sur la molécule lors de l'exploration des banques de séquences. D'où l'intérêt d'algorithmes de recherche assurant une recherche en séquence et structure par le biais d'un descripteur défini par l'utilisateur intégrant l'ensemble des connaissances caractérisant l'ARN à détecter. Une nouvelle façon d'aborder ce problème consiste en l'étude de problèmes algorithmiques sur les graphes d'intersection d'un ensemble de 2-intervalles. Cette notion de 2-intervalles se trouve dans la lignée des études actuelles en matière d'algorithmique de graphes où l'on étudie de plus en plus les structures des graphes issues de modèles géométriques. Nous présentons plusieurs résultats de complexité et montrons en particulier que la recherche de motifs dans un ensemble de 2-intervalles est un problème NP-complet. Nous nous intéressons, plus particulièrement, à appliquer ces travaux pour la prédiction de motifs biologiques structurés. Plus spécifiquement, nous avons mis au point l'algorithme ORANGE pour la prédiction des introns auto-catalytiques de groupe 1 dans de grandes séquences génomiques. Cet algorithme est une amélioration de l'algorithme CITRON mis au point par F. Lisacek et F. Michel du point de vue de la rapidité d'exécution. De plus, une mise-en-œuvre de l'algorithme ORANGE est accessible en ligne sur Internet.

La technologie de workflow, tendant à automatiser les processus d'entreprise et à fournir un support pour leur gestion, est aujourd'hui un secteur actif de recherche. C'est dans ce contexte que se situent ces travaux de thèse qui portent aussi bien sur la modélisation des processus workflow que sur leur vérification. Ces processus, pouvant être contraints par des ressources partagées ou encore par des durées de traitement, doivent être vérifiés avant d'être confiés aux systèmes de gestion de workflow qui vont les exécuter. Nous nous sommes intéressés par la vérification de la propriété de cohérence (soundness) des réseaux de workflow (WF-net) : sous-classes des réseaux de Petri (RdPs) modélisant les processus workflow.Dans ce cadre, en explorant la théorie structurelle des RdPs, nous avons identifié des sous-classes de WF-nets pour lesquelles la cohérence peut être vérifiée et caractérisée efficacement. Nous nous sommes focalisés en outre sur l'extension de ces sous-classes en tenant compte de la présence de ressources partagées et sur la propriété de cohérence en présence d'un nombre arbitraire d'instances prêtes à s'exécuter. Dans cette partie, nous avons dû automatiser le calcul des siphons minimaux dans un RdP. Pour ce faire, nous avons choisi un algorithme de la littérature et l'amélioré par la recherche et la contraction de circuits alternés.Ensuite, nous avons abordé la modélisation et la vérification de processus workflow tenant compte des contraintes temporelles. Nous avons en premier lieu proposé un modèle de TWF-net (WF-net Temporisé). Pour ce modèle, nous avons défini la propriété de cohérence temporelle et proposé une condition nécessaire et suffisante pour la vérifier. En deuxième lieu, nous avons relaxé les contraintes temporelles adoptées par la proposition d'un modèle temporel visant des processus à contraintes temporelles variant dans des intervalles de temps. Nous avons défini formellement le modèle de ITWF-net (Interval Timed WF-net) et donné sa sémantique. Par ailleurs, nous avons développé et testé un prototype de modélisation et de simulation des ITWF-nets.La dernière partie de cette thèse a concerné la vérification formelle des processus workflow par SPIN model checker. Nous avons dû en premier lieu traduire la spécification des workflows adoptée vers Promela : le langage de description des modèles à vérifier par SPIN. En second lieu, nous avons exprimé les propriétés de cohérence en Logique Linéaire Temporelle (LTL) et utilisé SPIN pour tester si chaque propriété est satisfaite par le modèle Promela du WF-net en question. Enfin, nous avons exprimé les propriétés de k-cohérence pour les WF-nets modélisant plusieurs instances et de (k,R)-cohérence pour les processus workflow concurrents et qui possèdent des ressources partagées.

Dans le cadre de cette thèse, nous nous intéressons à l'acquisition automatique de réseau de contraintes, aussi appelée apprentissage automatique de réseau de contraintes, qui consiste à développer des solutions capables d'aider un utilisateur à modéliser un problème combinatoire sous la forme d'un réseau de contraintes. Notre travail se focalise plus précisément sur la plate-forme d'acquisition automatique de réseau de contraintes CONACQ. Dans son implémentation standard, CONACQ est passive vis-à-vis de l'utilisateur, c'est-à-dire basée sur la capacité de ce dernier à fournir des instances significatives de son problème. Dans la première partie de cette thèse, nous proposons une version interactive de CONACQ, capable de poser à l'utilisateur des questions dont le but est d'augmenter plus rapidement et de manière conséquente la connaissance acquise par la plate-forme. Afin de limiter le nombre d'interactions, nous proposons différentes stratégies de questionnement que nous validons ensuite empiriquement. Dans la seconde partie, nous nous intéressons à une utilisation pratique de l'acquisition automatique de réseau de contraintes qui vise à automatiser le processus de définitions de comportements sensorimoteurs en robotique. Dans cette optique, nous proposons une architecture logicielle, complémentaire aux architectures de contrôle existantes, qui utilise le paradigme de la programmation par contraintes pour modéliser, planifier et superviser l'exécution de comportements sensorimoteurs. Elle utilise la plate-forme CONACQ étudiée dans la première partie de cette thèse pour modéliser automatiquement les actions élémentaires d'un robot sous la forme de réseaux de contraintes. Notre architecture utilise par ailleurs un planificateur de tâches inspiré de CSP-Plan pour combiner les réseaux de contraintes acquis et ainsi définir automatiquement des comportements sensorimoteurs. Différents résultats expérimentaux sont par ailleurs présentés afin de valider notre approche.

Dans les environnements pervasifs, le constant changement du contexte d'utilisation des applications et des services distribués (i.e., des ressources) impose de nouvelles exigences pour la définition des solutions de contrôle d'accès. Celles-ci concernait notamment la sensibilité au contexte et la mise en œuvre distribuée des politiques d'accès. Pour prendre en compte ces besoins, nous proposons une famille de modèles de contrôle d'accès, appelé CxtBAC (Context-Based Access Control), qui se compose de huit modèles conceptuels et permet d'explorer les informations contextuelles caractérisant les entités suivantes : le propriétaire de la ressource, l'environnement, l'utilisateur et la ressource elle-même. Contrairement aux propositions existantes, basées sur le modèle RBAC (Role-Based Access Control), la famille de modèle proposé est centrée sur la notion de contexte et non de rôle. Par conséquent, les décisions d'accès aux ressources protégées sont prises en considérant les informations contextuelles qui caractérisent la situation des entités impliquées. Pour décrire les règles d'accès, les permissions sont associées à des contextes d'accès et les utilisateurs sont associés dynamiquement à ces dernières. Les modèles proposés sont indépendants du langage de spécification de la politique de sécurité. Dans le cadre de cette thèse, nous proposons une solution pour la mise en ?uvre basée sur un formalisme d'ontologies.

Cette thèse porte sur le développement de méthodes et de modèles permettant de quantifier la sûreté de fonctionnement d'applications embarquées sur des systèmes mobiles. L'objectif est de fournir des indicateurs pour l'analyse et la sélection des architectures les plus adaptées pour satisfaire les exigences de sûreté de fonctionnement. Nous considérons le cas des applications véhiculaires utilisant des communications inter-véhicules basées sur des réseaux ad-hoc et pouvant avoir accès à des services situés sur des infrastructures fixes. Nous proposons une approche combinant: 1) des modèles de sûreté de fonctionnement utilisant des réseaux d'activités stochastiques permettant de décrire les modes défaillances et de restauration des systèmes considérés et 2) des simulations et des modèles analytiques de scénarios de mobilité permettant d'estimer des caractéristiques de connectivité de ces systèmes. Cette approche est illustrée sur trois cas d'études dont un système d'autoroute automatisée, et une boîte noire virtuelle basée sur la réplication et la sauvegarde coopérative des données.

Dans ce manuscrit, nous proposons de concevoir et de mettre en oeuvre un environnement logiciel pour une "gestion guidée par les modèles" des changements dans les architectures des applications distribuées coopératives. Les aspects adaptabilité des applications, les aspects transformations de graphe et les aspects particuliers des applications distribuées coopératives sont étudiés. Une approche d'adaptation s'appuyant sur une modélisation par les graphes et un style architectural de type Poducteur/Consommateur est présentée pour des applications communicantes collaboratives sensibles au contexte. Une démarche de raffinement est proposée permettant de garantir un certain degré d'adaptabilité en faisant un compromis entre les différents paramètres du contexte. Ces travaux de recherche ont aussi permis de définir un cadre algorithmique générique de reconfiguration architecturale multi-niveaux pour la sélection des architectures de déploiement les plus adaptées à un contexte et aux situations associées. Ce cadre a été appliqué au cas de la communication et de la coopération de groupe. Elle a aussi permis de modéliser le style architectural Producteur/Consommateur pour une communication orientée évènement. Des règles d'adaptation ont été définies. Elles comportent une partie basée sur SWRL pour la description du contexte et des règles d'adaptation, et une partie basée sur les grammaires de graphes pour la transformation des configurations de déploiement

L'objectif de cette thèse est de développer une théorie de types pour le λ-calcul linéaire-algébrique, une extension du λ-calcul motivé par l'informatique quantique. Cette extension algébrique comprend tous les termes du λ-calcul plus leurs combinaisons linéaires, donc si t et r sont des termes, α.t+β.r est aussi un terme, avec α et β des scalaires pris dans un anneau. L'idée principale et le défi de cette thèse était d'introduire un système de types où les types, de la même façon que les termes, constituent un espace vectoriel, permettant la mise en évidence de la structure de la forme normale d'un terme. Cette thèse présente le système Lineal , ainsi que trois systèmes intermédiaires, également intéressants en eux-même : Scalar, Additive et λCA, chacun avec leurs preuves de préservation de type et de normalisation forte.