Cette thèse a pour objet l'étude des systèmes de particules et collisions dans les automates cellulaires. En se basant sur des observations expérimentales, nous proposons des définitions formelles de ces objets et montrons qu'ils peuvent être mis en relation avec des coloriages réguliers du plan. À l'aide d'une représentation sous forme syntaxique de ces objets, nous introduisons une opération syntaxique d'assemblage: les schémas de ligature. Cette opération peut être interprétée en termes de coloriage et correspond à une opération intuitive utilisée dans l'étude algorithmique des automates cellulaires. Nous prouvons que, dans le cas d'assemblages finis, le lien entre l'opération syntaxique et l'interprétation peut être complètement caractérisé de façon algorithmique. Nous explorons ensuite des pistes d'extension de ces systèmes facilitant l'encodage et permettant de dépasser le cas fini. Enfin, nous étudions les applications de tels systèmes en lien avec l'universalité dans les automates cellulaires. En particulier, nous donnons une nouvelle preuve de l'universalité de l'automate cellulaire 110 et présentons la construction d'un automate cellulaire intrinsèquement universel de rayon 1 et à 4 états.

Le sujet présenté dans cette thèse consiste à concevoir un langage de programmation, appelé BOCAL, spécialement destiné à la modélisation et à la simulation de systèmes de production. La spécification et la simulation d'automates est également un domaine d'application de BOCAL. Les logiciels sont souvent partagés entre deux caractéristiques importantes : les logiciels extensibles (ouverts) mais pas assez conviviaux et les logiciels conviviaux mais fermés pour les utilisateurs. L'objectif de ce langage est de permettre à tous les niveaux d'utilisation (conception des objets de base, construction du modèle et réglage des paramètres) de fonctionner dans le même environnement sémantique afin de permettre à tous les utilisateurs de bénéficier de la modularité et de l'extensibilité.

La vérification formelle des contrôleurs logiques a donné lieu à de nombreux travaux scientifiques cette dernière décennie. Elle permet de démontrer (obtention d'un niveau requis de sûreté de fonctionnement (SdF) des systèmes industriels, et tout particulièrement des systèmes critiques. Nos travaux portent sur la preuve des propriétés relatives à la qualité du service rendu par le système automatisé, que nous nommons des propriétés quantitatives. Par exemple, au lieu de vérifier que plusieurs produits ont effectivement été dosés avant d'enclencher un mélange puis une réaction chimique, il peut être important de prouver que la bonne quantité de ces produits a été dosée. Autre exemple, au lieu de prouver qu'un mobile s'arrête dans une position donnée, il peut être important de prouver que cet arrêt en position s'effectue avec une précision garantie. Ce sont de telles propriétés quantitatives que nous nous sommes attachés à être capables de prouver pour les systèmes à évènement discrets (SED), et plus exactement pour une sous classe des SED : les systèmes logiques. Dans ce mémoire nous explorons l'apport des automates hybrides pour la prise en compte simultanée du caractère discret du contrôleur et continu du processus. A cette fin, nous introduisons un formalisme d'automates hybrides à transitions typées et nous proposons une méthodologie de modélisation basée sur des automates modulaires génériques. La vérification est alors obtenue par le model checker PHAVer. Deux études de cas sont présentées en fin de mémoire.

Le sujet global de cette thèse est l'étude d'automates cellulaires probabilistes. Elle est divisée en deux grandes parties.<br /><br />Au cours de la première, nous définissons la notion de chaîne partiellement ordonnée qui généralise celle d'automate cellulaire probabiliste. Cette définition se fait par l'intermédiaire de spécification partiellement ordonnée de la même façon que les mesures de Gibbs sont définies à l'aide de spécifications. Nous obtenons des résultats analogues sur l'espace des phases : caractérisation des mesures extrêmes, construction/reconstruction en partant des noyaux sur un seul site, critères d'unicité. Les résultats sont appliqués tout au long du texte à des automates déjà connus.<br /><br />La deuxième partie est essentiellement vouée à l'étude d'automates cellulaires unidimensionnels à deux voisins et deux états. Nous donnons deux décompositions des configurations spatio-temporelles en flot d'information. Ces flots ont une signification géométrique. De cela nous tirons deux critères d'unicité.<br /><br />En annexe, nous donnons une démonstration de transition de phase d'un automate cellulaire défini par A. Toom, le modèle NEC. Tout au long du texte, des simulations sont présentées.

Cette thèse se place dans le cadre de la vérification automatique des systèmes distribués. Elle aborde le problème de la spécification pour de tels systèmes, qui consiste à définir un formalisme logique pour décrire des propriétés des comportements de systèmes. On en attend qu'il soit facile d'exprimer les propriétés courantes (accessibilité, sûreté, exclusion mutuelle, vivacité, etc.). On souhaite par ailleurs que la vérification de ces propriétés soient aisée. Il s'agit donc de trouver un compromis entre pouvoir d'expression et simplicité d'utilisation.<br /><br />On s'intéresse ensuite à la modélisation des systèmes concurrents, en recherchant à nouveau un compromis entre réalisme des modèles et facilité de vérification. Les modèles étudiés dans ce travail sont les automates asynchrones, qui modélisent des processus concurrents communiquant par mémoire partagée.<br /><br />La thèse s'intéresse enfin au problème de la synthèse de contrôleur. Étant donné un système spécifié de façon incomplète, donc non-déterministe, en interaction avec un environnement, il s'agit de calculer de manière automatique comment restreindre son comportement afin qu'il vérifie une spécification donnée (quelles que soient les actions de l'environnement). Ce problème se formule en<br />termes de jeux. Dans le cas distribué, les jeux ont naturellement plusieurs joueurs. Dans ce cadre, la plupart des résultats sont négatifs : il est indécidable de savoir si on peut ou non contrôler un tel système. Cette thèse prouve que certaines propriétés de l'architecture de communication garantissent décidabilité pour toute spécification régulière.

On s'intéresse à l'analyse et la simulation du comportement itératif de réseaux d'automates et plus particulièrement des réseaux d'automates à seuil (avec éventuellement introduction d'une période de réfraction). On donne, on approfondit des résultats concernant la longueur du cycle limite, le nombre de pas nécessaires pour l'atteindre, ainsi que l'organisation spatiale des cellules dans le cycle.

.

Dans le domaine de la sûreté de fonctionnement, le diagnostic joue <br />un rôle primordial dans l'amélioration de la disponibilité opérationnel le <br />des équipements. Dans les systèmes industriels, une part importante <br />(jusqu'à 80%) est consacrée à la maintenance, test et diagnostic. Pour <br />des systèmes complexes, la résolution des problèmes liés au diagnostic <br />et d'une manière générale de la supervision nécessite la mise en oeu- <br />vre d'une approche générique. Le diagnostic concerne les deux phases <br />indissociables de détection et de localisation. Dans cette thèse nous <br />proposons une approche dynamique de diagnostic pour les systèmes à <br />événements discrets. L'approche proposée basée sur l'exploitation du <br />temps, est applicable à tout système dont l'évolution dynamique dépend <br />non seulement de l'ordre des événements discrets mais aussi de la durée <br />des tâches associées comme pour les processus de communication ou les <br />processus batch. Dans cette thèse, le diagnostic des fautes est réalisé <br />grâce à l'implémentation d'un modèle basé sur l'utilisation des auto- <br />mates temporisés. L'objectif est de concevoir un observateur pour un <br />système donné, qui permet de détecter et localiser les éventuel les dé- <br />fail lances du procédé. Cet observateur est appelé “diagnoser”. Une <br />défail lance est constatée lorsque le séquencement temporel en sortie est <br />incorrect. Nous présentons donc les différentes étapes de la démarche <br />de diagnostic : la construction du diagnoser, la vérification du modèle <br />ainsi qu'une l'application de la démarche sur un exemple réel avec son <br />extension aux systèmes hybrides.

Ce travail s'inscrit dans la continuité de l'étude du langage de description de systèmes AltaRica. Ce langage, développé au Labri, permet de modéliser des systèmes réels de manière hiérarchique. L'objectif de la thèse est d'introduire le temps quantitatif dans le but de concevoir des systèmes temps réel, c'est à dire des systèmes assujettis à des contraintes temporelles.<br />Deux extensions du langage sont proposées : une version temporisée et une hybride. Ces extensions respectent les caractéristiques du langage initial et conservent les aspects de hiérarchie, de synchronisation, de partage de variables et de priorité statique. En outre, afin d'améliorer les descriptions temps réel, de nouveaux opérateurs de modélisation, comme l'urgence et les priorités temporelles, ont été ajoutés. Nous obtenons ainsi un langage hiérarchique de haut niveau de modélisation de systèmes temps réel. <br />Une étude formelle complète a été menée sur la sémantique du langage, le pouvoir d'expression des langages AltaRica temps réel et des moyens de traductions automatiques vers des modèles classiques existants. Ces algorithmes reposent sur la notion de mise à plat de modèle, i.e. réécrire le modèle sans sous composant.<br />Enfin, le langage temporisé est implanté dans un prototype qui étant donné un modèle le met à plat puis le traduit en automate temporisé. Ainsi, certains systèmes réels ont pu être modélisés puis des propriétés ont été vérifiées à l'aide du model checker UPPAAL.

Les travaux présentés se situent dans le domaine de l'aide à la décision pour la surveillance de systèmes complexes tels que les procédés chimiques. Pour de tels procédés il n'est pas toujours possible de disposer d'un modèle mathématique ou structurel du système considéré. De ce fait, d'autres types d'approches telles que les méthodes de classification, doivent être envisagées pour l'identification des états fonctionnels dans lesquels le système peut se trouver. Sur la base de telles méthodes notre travail présente une stratégie permettant de construire, à partir de données historiques et de données récupérées en ligne, un modèle discret (états/transitions) du comportement du processus et d'identifier des situations anormales issues des dysfonctionnements. Cette stratégie consiste à générer un premier modèle de référence, sous la forme d'un automate à états finis, du procédé à partir d'un apprentissage, supervisé ou non. Ce modèle est ensuite validé et complété par l'expert. La reconnaissance en ligne permet de suivre l'évolution temporelle des modes de fonctionnement déjà identifiés. Dans le cas où une transition amène à la non-reconnaissance d'un certain nombre d'éléments, c'est-à-dire à la détection d'une déviation par rapport à un comportement connu, l'objectif est de caractériser cette nouvelle situation. Pour cela, nous proposons de faire un nouvel apprentissage hors ligne prenant en compte ces éléments non reconnus. Les nouvelles classes créées permettent, toujours en interaction avec l'expert, de fixer la nature de la déviation observée. Dans le cas d'une défaillance, une analyse portant sur les descripteurs et le profil des classes permet l'isolation de la défaillance. Ces informations sont transmises à l'opérateur pour l'assister dans son diagnostic. Un outil d'aide à la décision pour la surveillance s'appuyant sur cette stratégie a été mis en place. Cet outil appelé SALSA repose sur la méthode LAMDA. Il s'agit d'une méthode de classification avec apprent issage et reconnaissance de formes qui permet l'analyse de données multi-variables et qui utilise des notions de la logique floue pour introduire le concept d'adéquation d'un élément à une classe. Dans le cadre du projet européen CHEM les principaux aspects de nos travaux et les résultats obtenus ont été illustrés sur des unités industrielles de nature différente.