Le but de la thèse est de développer une nouvelle approche de surveillance des systèmes à événements discrets. La méthode proposée est basée sur la surveillance du temps de service en utilisant l'automate temporisé comme outil de modélisation.<br />Partant d'un système commandé, le premier objectif est la surveillance des différentes activités de ce système afin d'améliorer sa disponibilité. Ceci se traduit par la minimisation du nombre d'arrêts qui pénalisent la production, en suivant en temps réel, l'état de fonctionnement des différents capteurs du système. Ainsi pour chaque tâche, la surveillance du temps écoulé entre deux événements (l'instant où la commande a donné l'ordre de démarrer une tâche et l'instant où le capteur indique la fin d'exécution de la tâche) permet de détecter au plutôt d'éventuelles défaillances. La deuxième phase correspond au diagnostic qui consiste en la détermination des causes du problème observé.<br />Jusqu'à présent les approches de surveillance utilisent un modèle de référence basé sur la connaissance à priori de toutes les situations interdites du système. Le modèle de surveillance proposé présente un réel avantage. En effet, la détection d'éventuelles défaillances ne nécessite pas une liste exhaustive de toutes les défaillances possibles du système. En fonction de la catégorie du système de production et de la nature des tâches à surveiller nous introduisons une tolérance sur la durée de la tâche à surveiller. Ainsi, la notion de fonctionnement en ‘ mode dégradé' est introduite. Au-delà de cette tolérance, le système sera effectivement dans un état de ‘défaillance'. Différents exemples illustrent la démarche proposée. Ils permettent de montrer la puissance d'une telle approche. De plus, un algorithme permettant le calcul du seuil optimal de tolérance est proposé, ainsi que l'évaluation des performances du système de surveillance.

Les Réseaux de Petri (RdP) sont actuellement les approches les plus prometteuses pour modéliser et vérifier les systèmes complexes tels que les Systèmes Multi Agents (SMA). De nombreuses solutions ont été proposées pour remédier aux problèmes de communication, de coordination et d’interaction entre les Agents. Cependant, il n’existe aucune en mesure de traiter, à la fois les aspects structurels et comportementaux, du moins à notre connaissance. La thèse s'intéresse à la problématique de modélisation formelle et de vérification automatique et semi-automatique de propriétés pour les Systèmes Multi Agents. Plus précisément, l'objectif consiste à proposer un nouveau modèle formel original basé sur les réseaux de Petri, les Réseaux de Petri à Agents (RdPA), qui permettent d’exprimer de manière consistante et plus précise les systèmes Multi Agents. Il s’intéresse de plus à l’extension de ce modèle aux fins de modéliser la migration des agents dans le cadre des systèmes à agents mobiles. Cette classe de modèle permet de s’intéresser à la vérification formelle de propriétés classiques comme notamment la vivacité ou l’absence d’interblocage dans le cadre des Systèmes Multi-Agent. / Petri nets (PN) are currently the most promising approaches to model and to verify complex systems such as Multi Agent Systems (MAS). Several solutions have been proposed to solve the problems of communication, coordination and interaction among Agents. However, to best of our knowledge, none of this solution has able to handle both aspects: structural and behavioral. The thesis focuses on the problem of formal modeling and automatic and semi-automatic verification of properties in Multi Agent Systems. More specifically, the objective is to propose a new original formal model based on Petri nets, Agents Petri nets (APN), which express consistently more accurate a Multi Agent Systems. There is growing interest in the extension of this model for modeling the migration of Agents within the mobile Agent systems. This class of model allows focusing on the formal verification of classical properties such as alertness or absence of deadlock in the context of Multi Agent Systems.