Th. doct.-ing.--Inform.--Toulouse--I.N.P., 1984. N°: 314.

Nous nous intéressons aux approches formelles pour le développement de systèmes réactifs critiques. Le langage synchrone Lustre pour la spécification de tels systèmes a subit des évolutions majeurs au cours des dernières années en intégrant dans sa sémantique à base flots de données synchrones des constructions de plus haut-niveau appelées automates de modes (dans le langage Scade 6). Ceux-ci mettent en œuvre l’activation de modes de calculs en fonction des états et des transitions de l’automate, et reposent pour cela sur la sémantique des horloges du langage Lustre. En particulier, nous étudiions la prise en compte des horloges et des automates de modes dans l’outil de génération de tests GATeL dédié à l’origine au langage Lustre mono-horloge (flots de données purs). GATeL génère automatiquement des séquences de tests pour un modèle à partir d’un objectif de test décrit en Lustre à travers une exploration en arrière des dépendances entre flots et selon des teniques de résolution de contraintes. Nous présentons ces différents domaines et la mise en oeuvre des modifications apportées à l’outil pour prendre en compte les automates de modes. Enfin, nous définissons des critères de couverture structurelle pour les automates de modes et montrons alors comment, en les traduisant de manière automatique sous forme d’objectifs de tests, GATeL permet de générer des séquences couvrant ces critères. / Lustre is a synchronous dataflow-oriented language for the specification of reactive systems. Since its definition, it has been extended to support mode automata, a formalism in which computation modes are activated according to an extended state-machine. The semantics of mode-automata is heavily based on an appropriate use of the clock sampling features of Lustre. We present the modifications made in GATeL, an automatic test sequences generator originally designed for a mono-rate subset of Lustre. GATeL performs a lazy goal-oriented test sequences generation, based on constraint logic programming. We modify it so that it can handle the temporal constraints of clocks internally and efficiently generate tests sequences from state-maines specifications. We also present some existing structural test criteria for state-machines and adapt them to the specific case of mode-automata.

Mémoire numérisé par la Direction des bibliothèques de l'Université de Montréal.

Thèse numérisée par la Direction des bibliothèques de l'Université de Montréal.

Ce projet de recherche traite du domaine de l’intelligence artificielle, plus précisément de la programmation logique, un type de programmation utilisée pour concevoir des systèmes dits intelligents. Ce type de programmation est toutefois assez complexe à assimiler et il n’existe, à notre connaissance, aucun outil interactif qui permette de montrer efficacement le processus d’exécution d’un programme logique. L’objectif de cette recherche consistait donc à proposer un modèle d’outil facilitant la compréhension de la résolution d’un programme logique. Le modèle proposé permet de représenter graphiquement et dynamiquement la trace de résolution d’un programme logique. Un prototype a été construit pour valider ce modèle avec des programmes écrits en langage Prolog. L’utilisateur peut ainsi suivre les étapes d’exécution à travers l’affichage dynamique d’un arbre de dérivation. Actuellement, le modèle ne permet pas de prendre en compte des programmes écrits avec différents langages de programmation, une telle généralisation serait une bonne amélioration.

Ce mémoire présente l'étude d'une approche particulière des langages de programmation logico-fonctionnels, fondée sur la logique des clauses de Horn avec égalité. Nous définissons d'abord la syntaxe et la sémantique des programmes que nous considérons. La syntaxe est celle de la logique des clauses de Horn avec égalité. La sémantique est donnée par le plus petit e-modele de Herbrand associe a un programme. Nous nous intéressons ensuite au calcul dans ce langage. Nous proposons pour cela une nouvelle règle appelée sldei-resolution comme seule règle de calcul. Nous montrons sa cohérence, sa complétude ainsi que sa completude forte. La mise en œuvre de la règle sldei-resolution nécessite un algorithme de resolution d'équations. Nous étudions de tels algorithmes fondes sur la relation de surreduction, et améliorons ces algorithmes par l'utilisation de stratégies de surreduction. Cependant, ces stratégies ne sont pas complètes dans le cas général. Nous proposons alors des conditions suffisantes sur ces stratégies afin de préserver la complétude des algorithmes considérés. Nous caractérisons ensuite une classe de programmes, dits uniformes, pour lesquels l'utilisation de n'importe quelle stratégie de surreduction donne un algorithme complet de resolution d'équations. Nous donnons de plus une methode de vérification de l'uniformité d'un programme. Par ailleurs, nous proposons des conditions syntaxiques pour qu'un programme soit uniforme. Enfin, nous décrivons les principaux traits d'un langage de programmation fonde sur l'approche présentée dans ce mémoire, et l'implantation que nous avons réalisée

Approche pour la réalisation d'outils de vérification des masques de circuit intégrés. Le système Comfor est un extracteur de schéma électrique paramétrable par la technologie. Il analyse des images de C.I. pour reconnaitre les composants électriques et calculer leurs caractéristiques. Comfor base à la fois sur des notions de programmation logique et des techniques de reconnaissance syntaxique de formes

Ce travail se situe dans le cadre des systèmes informatiques pour l'enseignement intégrant des capacités de raisonnement. Les exigences de ces EIAO (Environnement Interactif d'Apprentissage avec Ordinateur) sont à la fois d'ordre didactique et d'ordre informatique : exigence d'un contrat didactique à la sémantique claire et pré­cise; exigence d'une liberté maximale donnée à l'enseignant dans la formulation de ce contrat; exigence de capacités de déduction complètes; exigence de performances garantissant un niveau d'interactivité suffisant. Concrétement, nous avons conçu et réalisé le système TALC (Tuteur d'Aide Logique à la Construction) pour l'enseignement de la géométrie, dont l'objectif est de diagnostiquer la correction de la construction d'un apprenant vis-à-vis de la spécification d'une figure donnée par un enseignant. La définition du contrat didactique constitue le point central de notre travail. Notre point de vue est que son expression à l'aide de la logique du premier ordre est nécessaire à la fois pour obtenir une définition claire et pour fournir de bonnes explications à l'apprenant. Nous donnons ainsi une sémantique précise aux langages manipulés par le système : le langage logique LDL - à partir duquel est déterminé le diagnostic - et les langages d'interface. Nous présentons aussi les principes de la formulation de la théorie logique représentant les connaissances présupposées de l'élève. Nous établissons, par étapes de dérivation successives, l'expression logique de la correction d'une construction. Cette attitude est fructueuse. Elle nous a amenés à proposer le concept d'extension logique d'une formule par rapport à une autre, nécessaire pour prendre en compte des objets non décrits dans la spécification. Les perspectives ouvertes sont les suivantes : amélioration de la formulation du contrat didactique (par une meilleure définition de la négation), extension des langages d'interface, constitution de séquences didactiques, construction d'un modèle de l'apprenant à l'aide de techniques d'apprentissage et définition d'un langage d'expression des dialogues à tenir.

Les flux de télévision sont structurés : ils sont en effet composés de programmes successifs (journaux, films, magazines, etc.) et entrecoupés par des inter-programmes (publicités, bandes annonces, parrainages, etc.). Dès que les flux sont diffusés sur les ondes, ils perdent malheureusement toute information de structure. La problématique de la délinéarisation automatique est de retrouver la structure des flux TV, avec en particulier le début précis et la fin précise de chaque programme, à partir des signaux audiovisuels reçus et des métadonnées éventuellement fournies par les chaînes TV. Cette thèse présente un système complet de délinéarisation automatique rigoureusement évalué sur quatre semaines de flux TV réels, pour deux chaînes de télévision différentes. Les travaux se basent sur la propriété de répétition des inter-programmes. Cette propriété est exploitée à travers la détection de toutes les répétitions d'un flux grâce à une technique de clustering des images clés du flux. Ces répétitions servent à la création de segments qui sont ensuite classés en segments de programme ou en segments d'inter-programme suivant les caractéristiques des répétitions et les relations entre les segments. Pour cela, le système utilise la programmation logique inductive. Une fois les segments classés, les segments de programme appartenant à un même programme sont étiquetés et réunifiés grâce aux métadonnées éventuelles. En l'absence de métadonnées, les segments de programme d'un même programme peuvent être seulement réunifiés grâce à des similarités visuelles.

L'acquisition et la représentation des connaissances est un aspect central dans le domaine de l'Intelligence Artificielle car une machine intelligente doit avant tout s'appuyer sur des informations représentant le monde de façon suffisamment précise. Cette difficulté à disposer d'une représentation correcte du monde est particulièrement importante lorsque l'on a à faire à un monde changeant ou à des informations provenant de sources multiples. Nous proposons dans cette thèse une méthode de fusion syntaxique de croyances dans le cas où les croyances sont représentées dans le cas où il n'existe pas de priorités explicites ni entre les agents, ni entre les croyances exprimées par les agents. Cette méthode, appelée fusion par R-ensembles, repose sur la recherche des sous-ensembles de formules à retirer afin de restaurer la cohérence. Nous avons réalisé une mise en œuvre de cette méthode basée sur la traduction du problème de fusion en un programme logique avec sémantique des modèles stables. Nous avons d'abord proposé deux implantations : une adaptation de l'algorithme smodels ainsi qu'une autre implantation basée sur les instructions fournies par Lparse/Gringo. Nous avons testé cette dernière implantation avec des expérimentations portant sur des profils de croyances générés aléatoirement ainsi que sur les données issues d'un projet européen portant sur le relevé en archéologie sous-marine. Dans un deuxième temps, cette thèse propose une extension de la fusion par R-ensembles dans deux directions. Nous nous sommes ainsi intéressés au cas où des préférences sont exprimées entre les agents ou entre les croyances exprimées par chaque agent. Nous nous sommes également penchés sur le cas où les croyances sont exprimées sous forme de programmes logiques.