Étude de méthodes de spécification et vérification des protocoles de communication. La méthode de vérification mise en œuvre consiste a évaluer les spécifications du protocole sur un modèle fini qui le représente. Le langage de spécification est basé sur un mu calcul permettant l'expression aussi bien de comportements que de propriétés

Le système de vérification propose permet de réduire et de comparer des systèmes de transitions étiquetées en tenant compte d'une relation d'équivalence. Les relations d'équivalence considérées sont la congruence forte, l'équivalence et la congruence observationnelles et la congruence par modèle d'acceptation. Les bases théoriques d'Aldebaran sont présentées ainsi que des algorithmes efficaces pour la comparaison et les réductions de systèmes de transition étiquetées et une réalisation en langage C

Cette thèse porte sur la réalisation d'une maquette du système CESAR, système d'aide à l'analyse d'applications réparties. L'outil réalisé permet de comparer une application décrite par un programme parallèle avec ses spécifications données par un ensemble de formules d'une logique temporelle.

Le système CESAR proposé dans cette thèse est un système d'aide à la conception des applications reparties. Il permet de décrire l'application étudiée dans un langage algorithmique en termes de processus communiquant par rendez-vous; de spécifier les propriétés de comportement souhaitées au moyen d'une logique temporelle. Le modèle sur lequel ces formules sont analysées est un réseau de Petri interprété généré automatiquement à partir de la description fournie. L'analyse repose sur une évaluation des opérateurs temporels comme points fixes de transformateurs de prédicats sur l'espace d'états du modèle.

L'approche objet permet des applications plus évoluées et plus fiables et des développements spécifiques moins coûteux et évolutifs. Les objectifs de ce travail sont, d'une part, de contribuer à la conceptualisation complète de modèles de simulation à objet et d'autre part, de les implémenter en utilisant des techniques de programmation concurrente. Après une présentation, au chapitre I, des concepts des systèmes de production et de leur gestion, nous avons évalué, au chapitre II, les différents modèles de structure et de simulation pour les systèmes de production. Le chapitre ID propose une démarche d'analyse pour identifier des classes d'objets en cinq types du domaine: physiques, rôles, incidents, interactions et spécifications. Chacune de ces classes est spécifiée par quatre modèles: communication, information, transition d'état et processus. Dans le chapitre IV, nous avons conceptualisé une architecture générale des objets actifs, une plateforme de simulation à objets concurrents et des classes d'objets sémantiques tels que les transactions, les moyens de production et les décisions pour l'établissement des modèles de simulation de production. Nous avons illustré, au chapitre V, l'implémentation des coopérations spatiales et temporelles entre objets concurrents dans la simulation avec des concepts processus "légers" basés sur l'outil Meijin++.

Cette thèse aborde un ensemble de problèmes lies a la conception et a la mise en œuvre d'un noyau de communication faisant partie de Parx, un noyau de système d'exploitation pour machines multiprocesseurs sans mémoire, développe dans le cadre du projet de recherche européen esprit supernode. Le noyau réalisé une machine virtuelle, vis-a-vis des communications, dans laquelle l'ensemble de processeurs est complètement connecte indépendamment de la topologie du réseau d'interconnexion sous-jacent. La machine virtuelle offre une interface qui facilite l'exploitation correcte du haut degre de parallélisme physique des machines visées. Après un état de l'art des architectures d'ordinateurs massivement parallèles, il est propose un modèle de processus et une structure de noyau de système parallèle. Le modèle est base sur un ensemble d'entités bien adaptées au contrôle de l'exécution des programmes parallèles composes de processus communicants. Ces entités, qui étendent la notion traditionnelle de processus, intègrent des concepts nouveaux visant la meilleure exploitation de l'architecture physique. Dans le modèle de processus communicants, ceux-ci ne coopèrent que par échange de messages. Le contrôle, correct et efficace, de la communication et la synchronisation entre processus s'exécutant sur une architecture multi-processeurs sans mémoire commune est le thème central de cette thèse. Notre étude s'oriente vers la conception d'un noyau de communication, pour lequel les problèmes concernant essentiellement le routage de messages sans interblocage dans le réseau de processeurs et les protocoles de communication entre processus adéquats au modèle de programmation utilisé

Ce travail a pour objet l'étude de méthodes de diagnostic d'erreurs de systèmes parallèles communicants, pour des spécifications exprimées dans une logique temporelle arborescente. Sa motivation est l'élaboration de diagnostics d'erreurs détectées par Xesar, outil de vérification de protocoles décrits dans une variante du langage Estelle. Xesar génère a partir du programme décrivant un protocole, un graphe fini dont les séquences représentent les exécutions. Vérifier consiste a comparer ce graphe aux spécifications. En cas de non satisfaction des spécifications, un diagnostic doit etre fourni, permettant de cerner la cause de l'erreur. On s'intéresse aux erreurs dont les diagnostics sont des séquences d'exécution du graphe représentant le comportement du programme. Un prototype d'un système de diagnostics d'erreurs, Cleo, a été réalisé et intégré a Xesar. Générer un diagnostic consiste a calculer un ensemble de séquences d'exécution dont l'existence est la cause de l'erreur. L'utilisation de Cleo nous a conduit a étudier les points suivants: définition d'un critère de minimalité d'un ensemble de diagnostics. Une relation d'ordre dans l'ensemble (éventuellement infini) des diagnostics est définie. Dans le cas des systèmes finis, il existe un sous-ensemble fini de diagnostics minimaux tel que chaque diagnostic a un minorant minimal. Simplification des diagnostics. Les diagnostics sont fournis sous une forme simplifiée, modulo une classe d'actions observables. Nous définissons une relation d'équivalence entre modèles appelée équivalence explicationnelle, qui préserve les diagnostics simplifies, et dont l'originalité est de dépendre de la formule exprimant les spécifications. Les diagnostics simplifies sont calcules dans un modèle réduit équivalent

Cette thèse propose un environnement pour la spécification et l'analyse des processus parallèles communicants et décrit en détail la partie de cet environnement qui permet de spécifier chaque processus et de construire des réseaux de processus. Un langage permet de décrire l'activité de communication de chaque processus et des opérateurs décrivent les constructions de réseaux. De plus, toute description de processus ou de réseau peut être rangée dans une base de données et associées à une représentation graphique. Cette représentation peut être utilisée pour construire des réseaux et de telles constructions sont traduites sous forme d'expression utilisant les opérateurs de construction. Enfin, le calcul du processus résultant d'une construction est présenté et un algorithme d'optimisation est proposé