Au sein de cette thèse, nous étudions l'utilisation de codes dans les systèmes de diffusion distribués et dans les systèmes de stockage auto-réparant. Les codes ont été largement utilisés afin de construire des systèmes fiables à partir d'éléments non fiables. A ce titre, les codes sont très utiles dans les systèmes distribués et surpassent les approches sans codes. Cependant, dans la pratique, les codes sont souvent délaissés notamment à cause de leurs coûts de décodage élevés et de leurs coûts de réparation plus élevés. Nous étudions la possibilité de réduire les coûts annexes afin de rendre les codes plus attrayants. Ainsi, nous proposons d'adapter un protocole de diffusion épidémique afin de profiter au plus des codes fontaines et nous construisons de nouveaux codes réseau basse complexité. Puis nous étudions l'utilisation de codes réseaux dans les systèmes de stockage afin d'offrir des compromis optimaux entre coûts de stockage et de réparation.

Mesurer les performances d'une application est devenue une tâche incontournable pour mieux comprendre sa dynamique et anticiper son évolution. Cette tâche nécessite des outils de supervision qui s'adaptent aux différentes spécificités de l'application et de son environnement de déploiement (distribution, hétérogénéité, etc.). Ces outils doivent également être les moins intrusifs possibles pour ne pas perturber le fonctionnement de l'application. Notre contribution dans cette thèse est de concevoir et d'implémenter une plateforme de supervision basée sur le déploiement dynamique de sondes pour collecter des informations sur l'utilisation des ressources systèmes. Ces sondes sont choisies pour leurs faibles degrés d'intrusivité. Elles fonctionnent en mode « offline » en enregistrant localement et sans traitement préalable les informations collectées au lieu de les transmettre sur le réseau. Ce mode de fonctionnement est moins intrusif car il optimise l'utilisation des ressources systèmes et réseaux. La plateforme intègre également un moteur générique d'analyse qui assure la transformation des formats hétérogènes des informations collectées vers un format pivot basé sur XML ce qui facilite la phase de corrélation. Ce travail de thèse, réalisé dans un cadre industriel, définit une plateforme pour fédérer des sondes de supervision. Le concept de cette plateforme peut être étendue pour faciliter la construction de systèmes nécessitant de vérifier l'état des ressources. C'est le cas par exemple des systèmes qui vérifient les contrats de performances.

Les nouvelles technologies en matière d'accès à l'information, de communication sans-fil et de localisation d'informations ouvrent la voie à des innovations majeures dans l'utilisation des systèmes informatiques. Ces avancées permettent d'imaginer de nouveaux usages informatiques dont la mise en œuvre motive le développement de méthodes de conception appropriées. Plus particulièrement, l'informatique mobile combine désormais des enjeux conceptuels tels que l'accès à des services par un utilisateur en mobilité, la généralisation d'outils de localisation, la compréhension de systèmes complexes par un public non-expert ou l'importante variabilité des situations d'exécution. Cette thèse propose un cadre de conception qui adresse certains des enjeux pour la mobilité des systèmes d'information. Dans cette perspective, les attentes des utilisateurs et les contraintes technologiques inhérentes à la mobilité des constituants du système définissent un espace contextuel dont les dimensions sont prises en compte dès les premières étapes de la conception. Le modèle proposé établit comme point d'entrée une description de l'espace géographique du système pour différencier un ensemble de contextes d'exécution. L'énoncé de ces contextes permet de corréler les attentes des utilisateurs avec les capacités techniques de la plate-forme et d'offrir le niveau fonctionnel le plus acceptable dans une situation donnée. Dans un second temps, les différentes fonctionnalités et les données mises en œuvre dans chaque contexte d'exécution peuvent être ordonnées ou filtrées afin d'optimiser la présentation des informations aux utilisateurs. Ces recommandations sont produites par l'analyse conjointe des préférences d'utilisateurs selon leurs interactions et leurs comportements spatiaux. Deux cadres expérimentaux viennent illustrer les propositions du modèle. La conception d'un système mobile de suivi de compétition nautique prend en compte différents contextes d'exécution et adapte un niveau de service à des situations dégradées. Un système de documentation et de visite de campus illustre les algorithmes de recommandation et affine la présentation d'informations localement à chaque contexte d'exécution.

La conception d'algorithmes pour les systèmes concurrents et répartis est subtile et difficile. Ces systèmes sont enclins à des blocages et à des conditions de course qui peuvent se produire dans des entrelacements particuliers d'actions de processus et sont par conséquent difficiles à reproduire. Il est souvent non-trivial d'énoncer précisément les propriétés attendues d'un algorithme et les hypothèses que l'environnement est supposé de satisfaire pour que l'algorithme se comporte correctement. La vérification formelle est une technique essentielle pour modéliser le système et ses propriétés et s'assurer de sa correction au moyen du model checking. Des langages formels tels TLA+ permettent de décrire des algorithmes compliqués de manière assez concise, mais les concepteurs d'algorithmes trouvent souvent difficile de modéliser un algorithme par un ensemble de formules. Dans ce mémoire nous présentons le langage PlusCal-2 qui vise à allier la simplicité de pseudo-code à la capacité d'être vérifié formellement. PlusCal-2 améliore le langage algorithmique PlusCal conçu par Lamport en levant certaines restrictions de ce langage et en y ajoutant de nouvelles constructions. Notre langage est destiné à la description d'algorithmes à un niveau élevé d'abstraction. Sa syntaxe ressemble à du pseudo-code mais il est tout à fait expressif et doté d'une sémantique formelle. Des instances finies d'algorithmes écrits en PlusCal-2 peuvent être vérifiées à l'aide du model checker tlc. La deuxième contribution de cette thèse porte sur l'étude de méthodes de réduction par ordre partiel à l'aide de relations de dépendance conditionnelle et constante. Pour calculer la dépendance conditionnelle pour les algorithmes en PlusCal-2 nous exploitons des informations sur la localité des actions et nous générons des prédicats d'indépendance. Nous proposons également une adaptation d'un algorithme de réduction par ordre partiel dynamique pour une variante du model checker tlc. Enfin, nous proposons une variante d'un algorithme de réduction par ordre partiel statique (comme alternative à l'algorithme dynamique), s'appuyant sur une relation de dépendance constante, et son implantation au sein de tlc. Nous présentons nos résultats expérimentaux et une preuve de correction.

Les systèmes de production manufacturiers sont une classe des systèmes à événements discrets. Leur taille nécessite de distribuer le logiciel de contrôle sur une architecture industrielle de plusieurs ordinateurs reliés en réseau. Dans ce contexte, il devient essentiel d'être capable d'évaluer l'impact d'une architecture réseau spécifique sur les services des systèmes manufacturiers en termes de la performance et la qualité. Les performances du réseau sous-jacent peuvent notamment nuire à la productivité du système. Dans la méthodologie traditionnelle proposée dans la littérature, cet aspect n'est pas pris en compte au niveau conception. Cependant, la modélisation de tels systèmes est importante pour vérifier certaines propriétés. Dans cette thèse, nous proposons une approche de modélisation par composants à l'aide des réseaux de Petri haut niveau pour la modélisation de certains protocoles de réseaux afin d'évaluer les systèmes manufacturiers comme étant des systèmes distribués. La sélection des réseaux de Petri est justifiée par leur pouvoir d'expression en ce qui concerne la modélisation des systèmes distribués et concurrents. L'approche par composants permet de diminuer la complexité de la modélisation et encourage la généricité, la modularité et la réutilisabilité des composants prêt-à-utiliser. Cela permet de construire facilement de nouveaux modèles et de réduire les coûts de développement de systèmes. En outre, cela peut aider à une meilleure gestion des services et des protocoles et à changer facilement/modifier un élément du système. Notre modélisation permet enfin d'évaluer ces systèmes par le biais de simulations centralisées

L'évolution rapide du web a changé la façon dont l'information est créée, distribuée, évaluée et consommée. L'utilisateur est dorénavant mis au centre du web en devenant le générateur de contenu le plus prolifique. Pour évoluer dans le flot d'informations, les utilisateurs ont besoin de filtrer le contenu en fonction de leurs centres d'intérêts. Pour bénéficier de contenus personnalisés, les utilisateurs font appel aux réseaux sociaux ou aux systèmes de recommandations exploitant leurs informations privées. Cependant, ces systèmes posent des problèmes de passage à l'échelle, ne prennent pas en compte la nature dynamique de l'information et soulèvent de multiples questions d'un point de vue de la vie privée. Dans cette thèse, nous exploitons les architectures pair-à-pair pour implémenter des systèmes de recommandations pour la dissémination personnalisée des news. Une approche pair-à-pair permet un passage à l'échelle naturel et évite qu'une entité centrale contrôle tous les profils des utilisateurs. Cependant, l'absence de connaissance globale fait appel à des schémas de filtrage collaboratif qui doivent palier les informations partielles et dynamiques des utilisateurs. De plus, ce schéma de filtrage doit pouvoir respecter la vie privée des utilisateurs. La première contribution de cette thèse démontre la faisabilité d'un système de recommandation de news totalement distribué. Le système proposé maintient dynamiquement un réseau social implicit pour chaque utilisateur basé sur les opinions qu'il exprime à propos des news reçues. Les news sont disséminées au travers d'un protocole épidémique hétérogène qui (1) biaise l'orientation des cibles et (2) amplifie la dissémination de chaque news en fonction du niveau d'intérêt qu'elle suscite. Ensuite, pour améliorer la vie privée des utilisateurs, nous proposons des mécanismes d'offuscation permettant de cacher le profil exact des utilisateurs sans trop dégrader la qualité de la recommandation fournie. Enfin, nous explorons un nouveau modèle tirant parti des avantages des systèmes distribués tout en conservant une architecture centralisée. Cette solution hybride et générique permet de démocratiser les systèmes de recommandations en offrant aux fournisseurs de contenu un système de personnalisation à faible coût.

Le travail coopératif est un domaine qui étudie le travail de groupes d'utilisateurs de façon générale. Sa finalité est la conception de collecticiels, ensembles logiciels qui contiennent les outils, les applications, et les plate-formes qui supportent les activités de groupes d'utilisateurs. La gestion de ces groupes et les échanges d'information entre leurs membres nécessitent la définition de nouveaux services de communication adaptés aux besoins des agents en coopération. Les travaux menés dans ce mémoire ont consisté à définir, à concevoir et à gérer la structuration des groupes coopératifs. Un modèle à base de graphes a été proposé à partir du partage de données, pour représenter les relations entre les divers membres d'un groupe coopératif. A partir de ce modèle, un service pour l'entrée et la sortie en coopération des agents coopérants a été défini. Un protocole de communication sous-jacent a été spécifié en utilisant le langage de description formelle Estelle. Le protocole proposé a été vérifié en utilisant l'environnement à base de réseaux de Petri VAL, puis a été implanté en langage C sous UNIX à partir du code Estelle généré. Une extension de ce travail permet la formation d'apartés qui sont des sous-groupes très dynamiques créés à l'intérieur de la coopération. Un autre protocole spécifié en Estelle a été proposé pour gérer la formation de ces apartés et leur évolution au sein de la coopération. En plus de la structuration des groupes, une étude des données qui peuvent être échangées entre des agents coopérants a mené à la définition d'un service de gestion des dépendances de données. Ce service, spécifié également en Estelle, permet de créer, supprimer ou modifier des dépendances entre données, et répercute les modifications de valeurs vers l'ensemble des données dépendantes.

Ce mémoire présente des travaux concernant la spécification, la modélisation et l'analyse de systèmes de contrôle-commande temps réel répartis sur un réseau de terrain. La problématique de modélisation de tels systèmes, qui doivent satisfaire des contraintes temporelles, réside dans la maîtrise de la taille et de la complexité des modèles. Pour cela, une méthodologie de modélisation est proposée ; elle repose sur les concepts de structuration, de modélisation et de validation modulaires au moyen du modèle formel Réseaux de Petri Temporisés Stochastiques. La structuration consiste en une décomposition hiérarchisée en blocs fonctionnels élémentaires. Une structure est proposée pour des entités de communication d'un réseau local temps réel, ainsi que pour un système temps réel de commande et surveillance réparties. La modélisation repose sur la construction et la composition de modèles de modules élémentaires. Les principes énoncés concernent la définition de règles de composition. Des modèles d'assertions logiques sont également proposés pour faciliter le passage des descriptions de comportements exprimées en langage naturel, à une modélisation en Réseaux de Petri Temporisés Stochastiques. La validation repose sur des étapes de composition partielle qui utilisent la modularité pour effectuer des vérifications ascendantes du comportement. Cette méthodologie est appliquée au réseau de terrain FIP, ainsi qu'au futur système de contrôle-commande de poste de transformation d'énergie électrique d'EDF. L'étude du réseau FIP porte plus particulièrement sur les services et mécanismes périodiques de couche application pour les échanges temps réel. Les analyses (qualitatives et quantitatives) effectuées sur l'application de EDF répartie sur le réseau FIP portent sur la vérification des propriétés fonctionnelles et des contraintes temporelles du système.

Les probabilités sont de plus en plus utilisées dans la conception et l'analyse des systèmes logiciels et matériels informatiques. L'introduction des tirages aléatoires dans les algorithmes concurrents et distribués permet de résoudre certains problèmes insolubles dans le cadre déterministe et de réduire la complexité de nombreux autres. Nous avons été amenés à étudier deux types de propriétés probabilistes. La convergence : cette propriété assure que, quel que soit l'état de départ et quel que soit l'enchainement des actions, le système atteindra toujours (avec probabilité 1) un ensemble donné d'états d'arrivée en un nombre fini d'actions (auto-stabilisation).L'accessibilité : ce type de propriété répond à des questions telles que "quelle est la probabilité p qu'une exécution partant d'un état initial donné atteigne un état final donné ? Quelles sont les bornes maximales et minimales de p ?" En ce qui concerne le premier point, nous avons développé de nouveaux critères permettant d'assurer la convergence et d'en calculer la vitesse (mixing time). Ces crotères utilisent l'analogie avec des modèles de physiquestatistique (champs de Markov) et exploitent des outils d'analyse probabiliste classiques (coupling, chaînes de Markov, processus de décision markoviens). Pour le second point, nous avons obtenu des résultats pratiques sur la vérification de protocoles de communication, comme le protocole Ethernet, en les modélisant à l'aide d'automates temporisés probabilistes et utilisant des outils de model-checking temporisés (HyTech) et probabiliste (PRISM, APMC).

Cette thèse s'inscrit dans le cadre général de l'utilisation des techniques formelles lors de la phase conceptuelle des systèmes distribués temps-réel, et concerne plus précisément l'extension des pouvoirs d'expression et d'analyse du modèle Réseaux de Petri Temporisés Stochastiques. Ce modèle, qui appartient à la classe des Réseaux de Petri Stochastiques, associe à chaque transition un intervalle de temps, et une distribution de probabilité sur cet intervalle (ceci permet de représenter des caractéristiques temporelles variées et en particulier des contraintes) En ce qui concerne le pouvoir d'expression, nous avons introduit, d'une part, la notion de mémoire temporelle de toutes les sensibilisations (ceci est important pour l'étude des phénomènes de préemption que l'on rencontre dans des algorithmes d'ordonnancement et dans des problèmes de sûreté de fonctionnement) et, d'autre part, plusieurs règles de tir de transitions (en particulier les règles MIN et MAX qui permettent des études des cas pires, aspect important dans les systèmes temps-réels). Les graphes ainsi obtenus ont été également situés par rapport à la référence comportementale que constitue le graphe des classes d'états (obtenu à partir des Réseaux de Petri Temporels). En ce qui concerne le pouvoir d'analyse, nous avons défini le concept d'automate quotient quantifié (concept basé, à la fois, sur la relation d'équivalence de Milner et les règles de réduction de Beizer), qui a deux qualités importantes : il permet, d'une part, d'obtenir des modèles, à la fois qualitatifs et quantitatifs de services de communication ; et, d'autre part, de contrôler les dimensions des modèles à traiter lors de la modélisation d'architectures de communication multicouches. Ce modèle a été appliqué à un exemple industriel, le protocole embarqué temps-réel ARINC 629 CP. L'étude faite a mis en évidence les propriétés temps-réel et de tolérance aux pannes de ce protocole.