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 progrès récents dans le domaine de l'informatique et des réseaux de communications ont ouvert la voie aux applications distribuées multimédias coopératives. La problématique associée à la conception de telles applications comporte plusieurs points. Tout d'abord, les données multimédias se caractérisent par leur qualité de service en termes de fiabilité, de débit engendré, de synchronisation temporelle¿ Les applications multimédias doivent donc garantir le respect de la qualité de service de chacun des médias, le point essentiel consistant à assurer le respect des contraintes de synchronisation intra et inter-flux. De même, le support de communication doit pouvoir s'adapter aux contraintes des médias transportés et fournir un service adéquat en terme de débit, fiabilité, délai de bout en bout¿ Enfin, les utilisateurs ont de plus en plus besoin de travailler en groupe pour leurs applications informatiques, et des mécanismes de coopération doivent être introduits. Dans cette thèse, des mécanismes ont été proposés pour répondre à cette problématique et ont été mis en oeuvre dans le cadre d'une application de visioconférence. Ainsi, la synchronisation multimédia est réalisée par un moteur utilisant des mécanismes avancés des systèmes opératoires et respectant un scénario modélisé par un réseau de Petri à flux temporels. La communication utilise un transport à ordre partiel qui s'adapte bien aux contraintes de cette application autant en terme de débit que de fiabilité, et permet d'en augmenter les performances. Enfin, cette visioconférence a été étendue pour prendre en compte des notions de travail de groupe et offre, en particulier, un contrôle des entrées/sorties des participants et des interactions au sein du groupe. Une architecture générale garantissant ces contraintes temporelles et de coopération a ainsi été proposée et réalisée. Enfin, ces techniques ont été appliquées à une application de téléformation professionnelle dans le domaine de l'aéronautique.

Les progrès récents dans le domaine des technologies de communications ont ouvert la voie à de nouveaux réseaux et les applications multimédias distribuées se sont développées. Elles ont pour principales caractéristiques des débits élevés, des flux continus avec de fortes contraintes temporelles, et des besoins en synchronisation pour préserver la cohérence de leur présentation. Les réseaux de communication actuels ne pouvant tout offrir à la fois (hauts débits, qualité et respect des contraintes temporelles), la multiplicité des supports de communication et des services permet d'envisager une nouvelle voie : le choix du support de communication en fonction des contraintes de l'application. Si cette multiplicité possède des attraits, elle recèle aussi de nombreuses difficultés qu'il faut maîtriser comme l'hétérogénéité des services de bout en bout. Ceci nous a conduit à concevoir et à réaliser une nouvelle architecture de communication " multi-réseaux " prenant en compte les besoins spécifiques des applications multimédias. D'une part, lorsque plusieurs réseaux sont accessibles, un protocole permettant de sélectionner la meilleure interface de communication en fonction des besoins spécifiques des flux multimédias a été défini. Afin de préserver la synchronisation multimédia, des mécanismes d'ordres partiels sont intégrés au protocole. D'autre part, lorsque des domaines très hétérogènes doivent être traversés par un flux, une solution qui permet de préserver la qualité de service des protocoles de transport est proposée. Elle est basée sur le principe de la rupture des connexions transport par des proxys situés en bordure de domaine. Un modèle de flux associant un langage de spécification des flux multimédias à des mécanismes de traitement de ces flux par le protocole est proposé pour formaliser les spécifications de qualité de service. Enfin, cette thèse a contribué à développer des mécanismes de déploiement dynamique de protocoles de t ransport.

Dès qu’on manipule des ordres partiels (des hiérarchies), il est naturel de se demander comment les représenter dans un système informatique. Parmi les solutions proposées dans la littérature, on retrouve le codage par vecteur de bits. Dans cette thèse, nous nous intéressons au problème de calcul d’un codage des ordres par vecteur de bits de taille minimale, aussi connu par le problème de calcul de la 2-dimension des ordres, qui est NP-complet. Nous proposons des solutions du problème de nature heuristique, pour le cas général et pour des classes d’ordres particulières.Cette thèse présente également des résultats sur des conjectures autour de la 2-dimension des arbres. Notamment celle de Habib et al. à propos de la 2-approximabilité de la 2-dimension des arbres. Nous proposons quelques pistes de preuve de cette conjecture puis une reformulation, permettant d’apporter un nouveau regard sur le problème en question et d’espérer trouver des codages des ordres par vecteur de bits efficaces et de taille inférieure à leur 2-dimension. Nous apportons une réponse négative à deux autres conjectures. / The main question asked when manipulating partial orders (hierarchies), is how to represent them in computer. Among solutions proposed in literature, there is the bit-vector encoding. In this thesis, we consider the problem of computing a bit-vector encoding of orders with minimal size, which is also known as the problem of computing the2-dimension of orders that is NP-complete. We propose heuristics solutions of the problem for the general case and for some particular order classes. In addition, this thesis presents some results about conjectures on the 2-dimension of trees. Especially, the conjecture of Habib et al. about the 2-approximability of the 2-dimension of trees. We propose some ideas of a proof of this conjecture then give a reformulation of it that brings new perspectives on the problem that are finding efficient bits-vector encodings of orders of size less than their 2-dimension. We disprove two other conjectures.

The thesis focuses on two open problems on finite partially ordered sets: the structure of order polytopes and the approximation of the number of linear extensions of a poset by mean of graph entropy. The polytopes considered here are the linear ordering polytope, the semiorder polytope, the interval order polytope, the partial order polytope and also a generalisation of the linear ordering polytope: the linear extension polytope of a fixed poset P. Various results on the structure of theses polytopes are proved in the first part of the thesis. In the second part of the thesis, we improve the existing bounds linking the entropy of the incomparability graph of the poset P and its number of linear extension. / Le but de la thèse est d'étudier deux problèmes ouverts sur les ensembles ordonnés finis: la structure des polytopes d'ordre et l'approximation du nombre d'extensions linéaires d'un ordre partiel au moyen de la notion d'entropie de graphe. Les polytopes considérés sont le polytope des ordres totaux, le polytope des semiordres, le polytope des ordres d'intervalles, le polytope des ordres partiels, ainsi qu'une généralisation du polytope des ordres totaux: le polytope des extensions linéaires d'un ensemble ordonné fixé P. Des résultats sur la structure de ces polytopes sont présentés dans la première partie de la thèse. Dans la deuxième partie de la thèse, nous améliorons les bornes existantes liant l'entropie du graphe d'incomparabilité d'un ordre partiel et son nombre d'extensions linéaires. / Doctorat en Sciences / info:eu-repo/semantics/nonPublished

Un programme concurrent est composé de plusieurs unités logiques : les processus. Chaque processus a un comportement qui lui est propre : il exécute ses actions de façon séquentielle. Un objectif important est de s'assurer que de tels systèmes concurrents complexes soient cependant exempts de défaut. Cette problématique est étudiée dans le cadre de la théorie de la concurrence. Quand plusieurs processus s’exécutent en parallèle, l’ordre d’exécution des actions du programme global n’est plus déterminé. On assiste au fameux phénomène "d’explosion combinatoire" faisant référence au très grand nombre d’exécutions globales possibles. Les diverses techniques et méthodes d'analyse existantes (model checking, analyse statique, tests automatisés, etc) se heurtent irrémédiablement à cette "explosion". Cette thèse s'inscrit dans un projet à long terme d'étude quantitative de ce phénomène et de développement des techniques d’analyse statistique basées sur la génération aléatoire uniforme. Notre objectif dans cette thèse est de traiter une composante fondamentale de la concurrence : la synchronisation. Ce mécanisme permet aux processus de communiquer entre eux. Dans cette thèse nous proposons un modèle combinatoire de structures croissantes pour modéliser les exécutions de programmes concurrents synchronisés. Avec des outils de combinatoire analytique nous obtenons plusieurs résultats exacts et asymptotiques sur le nombre moyen d'exécutions dans des sous-classes de programmes concurrents. Nous présentons aussi plusieurs algorithmes de génération aléatoire uniforme de structures croissantes et de leurs étiquetages. / A concurrent program is a composition of several logical blocks: the processes. Each process has its own behavior, independent from the others: it sequentially runs its actions. An important goal is to ensure that such concurrent complex systems are faultless. This problem is studied in the field of concurrency theory. When several process are running in parallel, the running order of the actions of the total program is no more decided. This is the well-known "combinatorial explosion" phenomena, meaning that the number of possible runs of the global program is huge. The analysis techniques and methods existing (model checking, static analysis, automated testing, etc) are irremediably limited by this "explosion". This thesis is a part of a long-term project about the quantitative study of this phenomena and the development of statistic analysis methods based on the uniform random generation. Our specific goal is to study a fundamental principle of the concurrency theory: the synchronization. This mechanism allows communications between the processes. In this thesis we propose a combinatorial model of increasingly labeled structures to deal with runs of synchronized concurrent programs. Using the tools of analytic combinatorics we obtain close formulas and asymptotic equivalents for the average number of runs in several subclasses of concurrent programs. We also present algorithms of uniform random generation of increasingly labeled structures and for their increasing labelings.

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 et sont par conséquent difficiles à reproduire 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. 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 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 / Designing sound algorithms for concurrent and distributed systems is subtle and challenging. These systems are prone to deadlocks and race conditions, and are therefore hard to reproduce. Formal verification is a key technique to model the system and its properties and then perform verification by means of model checking. Formal languages like TLA+ have the ability to describe complicated algorithms quite concisely, but algorithm designers often find it difficult to model an algorithm in the form of formulas. In this thesis, we present PlusCal-2 that aims at being similar to pseudo-code while being formally verifiable. PlusCal-2 improves upon Lamport?s PlusCal algorithm language by lifting some of its restrictions and adding new constructs. Our language is intended for describing algorithms at a high level of abstraction. Finite instances of algorithms described in PlusCal-2 can be verified through the TLC model checker. The second contribution presented in this thesis is a study of partial-order reduction methods using conditional and constant dependency relation. To compute conditional dependency for PlusCal-2 algorithms, we exploit their locality information and present them in the form of independence predicates. We also propose an adaptation of a dynamic partial-order reduction algorithm for a variant of the tlc model checker. As an alternative to partial order reduction based on conditional dependency, we also describe a variant of a static partial-order reduction algorithm for the tlc model checker that relies on constant dependency relation. We also present our results for the experiments along with the proof of correctness

Nous proposons une technique de dépliage pour vérifier les systèmes concurrents infinis bien structurés. Certaines propriétés d'intérêt comme la bornitude, la couverture et la terminaison sont décidables grâce à la bonne structure de ces systèmes. D'autre part, le dépliage réduit efficacement l'explosion combinatoire en exploitant l'ordre partiel entre les événements des systèmes concurrents. Nous proposons une modélisation par structure d'événements pour des systèmes bien structurés élémentaires, tels les compteurs et les files de communication. Le dépliage d'un réseau de structures d'événements étant une structure d'événements, nous proposons ensuite une approche hiérarchique à la modélisation et à la vérification des systèmes, qui préserve la bonne structure. Enfin, nous proposons une technique d'élimination des événements redondants. La mise en œuvre de notre approche dans l'outil ESU nous permet de conclure à son efficacité. / We propose an unfolding technique for verifying concurrent infinite-state systems that are well-structured. Some properties of interest such as boundedness, coverability and termination are decidable thanks to the well-structure of these systems. Moreover, the unfolding effectively reduces the combinatorial explosion by exploiting the partial order between events of concurrent systems. We propose a modelization using event structures for basic well-structured systems, such as counters and communication channels. As the unfolding of a synchronized product of event structures is an event structure, we obtain a hierarchical approach to modeling as well as to verifying systems, which preserves the well-structure. Finally, we propose a technique for eliminating redundant events. The implementation of our approach in the ESU tool allows us to conclude on its efficiency.