L'objectif principal de cette thèse est de proposer une approche efficace de modélisation et de résolution pour le problème d’ordonnancement, en mettant l’accent sur le partage multi-ressources et sur l’incertitude potentielle d’occurrence de certains événements. L'ordonnancement a pour objectif de réaliser un ensemble de tâches à la fois en respectant des contraintes prédéfinies et en optimisant le temps. Ce travail s’intéresse en particulier à la minimisation du temps total d’exécution. La plupart des approches existantes préconisent une modélisation mathématique exprimant des équations et des contraintes pour décrire et résoudre des problèmes d’ordonnancement. De telles démarches ont une complexité inhérente. Cependant dans l’industrie, la tâche de planification est récurrente et peut requérir des changements fréquents des contraintes. Outre cela, la prise en compte d’événements incertains est peu supportée par les approches existantes; cela peut toutefois augmenter la robustesse d’un ordonnancement. Pour répondre à ces problématiques, après une introduction, le chapitre 2 aborde le problème de l’ordonnancement à travers une démarche de modélisation visuelle, expressive et formelle, s’appuyant sur les automates pondérés et sur la théorie des automates temporisés. L’originalité des modèles proposés réside aussi dans leur capacité de décrire le partage de ressources multiples et proposer une approche de résolution efficace. Ces modèles ont l’avantage d’être directement exploitables par des outils de vérification formelle, à travers une démarche de preuve par contradiction vis-à-vis de l’existence d’une solution. Les résultats effectifs sont obtenus grâce à l’outil UPPAAL. La complexité inhérente à la production d’une solution optimale est abordée à travers un algorithme de recherche et d’amélioration itérative de solutions, offrant une complexité très prometteuse sur la classe de problèmes étudiés. Dans le chapitre 3, une composition synchrone est d’automates pondérés est proposée dans le but de résoudre le problème d’ordonnancement en effectuant une analyse d’atteignabilité optimale directement sur les modèles automates pondérés. Dans le quatrième chapitre, divers comportements incontrôlables tels que le temps de début, la durée de la tâche et l'occurrence d’échec dans un problème d‘ordonnancement sont modélisés par des automates de jeu temporisés. Ensuite, le problème est résolu en effectuant une synthèse de stratégie optimale dans le temps dans l'outil de synthèse TIGA. / The objective of scheduling problems is to find the optimal performing sequence for a set of tasks by respecting predefined constraints and optimizing a cost: time, energy, etc. Despite classical approaches, automata models are expressive and also robust against changes in the parameter setting and against changes in the problem specification. Besides, few studies have used formal verification approaches for addressing scheduling problems; yet none of them considered challenging and practical issues such as multi-resource sharing aspect, uncontrollable environment and reaching the optimal schedule in a reasonable time for industrializing the model. The main objective of this thesis is to propose an efficient modeling and solving approach for the scheduling problem, considering multi-resource sharing and potential uncertainty in occurrence of certain events. For this purpose, after an introduction in Chapter 1, Chapter 2 addresses the problem of scheduling through a visual, expressive and formal modeling approach, based on weighted automata and the theory of timed automata. The originality of the proposed approach lies in ability of handling the sharing of multiple resources and proposing an efficient solving approach. The proposed models have the advantage of being directly exploitable by means of formal verification tools. The results are obtained using the UPPAAL tool. To solve the problem, an algorithm is developed based on iterating reachability analysis to obtain sub-optimal makespan. Results show the proposed model and solving approach provides a very promising complexity on the class of studied problems and can be applied to industrial cases. In Chapter 3, a synchronous composition of weighted automata is proposed to solve the scheduling problem by performing an optimal reachability analysis directly on the weighted automata models. In the fourth chapter, various uncontrollable behaviors such as the start time, the duration of the task and the failure occurrence in a scheduling problem are modeled by timed game automata. Then, the problem is solved by performing an optimal strategy synthesis over time in TIGA as a synthesis tool.

Dans cette thèse, nous nous sommes intéressés aux protocoles pair-à-pair (P2P), qui représentent une solution prometteuse pour la diffusion et le partage de données à faible coût sur Internet. Nous avons mené, dans un premier temps, une étude comportementale de différents protocoles P2P pour le partage de fichier (distribution de contenus sans contrainte de temps) puis le live. Dans la première étude centréesur le partage de fichier, nous avons montré l’impact d’Hadopi sur le comportement des utilisateurs et discuté l’efficacité des protocoles en fonction du contenu et l’efficacité protocolaire, en se basant sur les choix des utilisateurs. BitTorrent s’est nettement démarqué au cours de cette étude, notamment pour les grands contenus. En ce qui concerne le live, nous nous sommes intéressés à la qualité de servicedu réseau de distribution live Sopcast, car plus de 60% des événements live diffusés en P2P le sont sur ce réseau. Notre analyse approfondie de ces deux modes de distribution nous a fait nous recentrer sur BitTorrent, qui est à la base de tous les protocoles P2P Live, et est efficace en partage de fichier et complètement open source. Dans la seconde partie de la thèse, nous avons proposé et implémenté dansun environnement contrôlé un nouveau protocole sur la base de BitTorrent avec des mécanismes protocolaires impliquant tous les pairs dans la gestion du réseau. Ces nouveaux mécanismes permettent d’augmenter l’efficacité du protocole via une meilleure diffusion, tant pour le live que le partage de fichier, de métadonnées (la pièce la plus rare) et via une méthode dite de push, par laquelle un client va envoyer du contenu aux pairs les plus dans le besoin / In this study, we focused on peer-to-peer protocols (P2P), which represent a promising solution for data dissemination and content delivery at low-cost in the Internet. We performed, initially, a behavioral study of various P2P protocols for file sharing (content distribution without time constraint) and live streaming. Concerning file sharing, we have shown the impact of Hadopi on users’ behavior and discussed the effectiveness of protocols according to content type, based on users’ choice. BitTorrent appeared as the most efficient approach during our study, especially when it comes to large content. As for streaming, we studied the quality of service of Sopcast, a live distribution network that accounts for more than 60% of P2P broadcast live events. Our in-depth analysis of these two distributionmodes led us to focus on the BitTorrent protocol because of its proven efficiency in file sharing and the fact that it is open source. In the second part of the thesis, we proposed and implemented a new protocol based on BitTorrent, in a controlled environment. The modifications that we proposed allow to increase the efficiency of the protocol through improved dissemination of metadata (the rarest piece), both for live and file sharing. An enhanced version is introduced with a push method, where nodes that lag behind receive an extra service so as to improve the overall performance