Les systèmes hybrides sont des systèmes qui combinent des composantes discrètes et des composantes continues. Les composantes continues peuvent représenter un environnement physique obéissant à des règles de changement continu, par contre les composantes discrètes peuvent représenter des contrôleurs discrets qui sondent et manipulent les composantes continues en temps réel. Deux approches peuvent être adoptées pour spécifier ces systèmes, la première étant basée sur des automates (hybrides) et utilise des méthodes d'analyse algorithmiques. La seconde est basée sur les logiques et utilise des preuves formelles comme méthodes d'analyse. Dans une première partie de cette thèse nous considérons l'approche basée sur les automates. Nous étudions la décidabilité du problème de la vérification pour certaines classes de systèmes hybrides linéaires. Nous prenons comme modèles des automates hybrides linéaires avec des structures de données discrètes non bornées. Nous exhibons différents cas de tels systèmes dont le problème de la vérification est décidable. Dans une seconde partie nous considérons l'approche basée sur les logiques et plus particulièrement celle basée sur le «Calcul de Durées». Nous étudions les relations existantes entre cette approche et la précédente ; nous montrons comment cette liaison permet de mettre en évidence un fragment important du «Calcul de Durées» pour lequel le problème de la vérification est décidable

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.

Dans ce travail, nous mettons en place une méthode fournissant des bornes à la fois garanties et précises de l'erreur de discrétisation commise sur des quantités locales lors de simulations numériques menées par la Méthode des Éléments Finis. On se focalise sur les problèmes de viscoélasticité linéaire décrits par variables internes. A partir d'une méthode générale développée au LMT Cachan, plusieurs optimisations sont abordées parmi lesquelles la prise en compte des effets d'histoire, le caractère non intrusif de la méthode ou l'estimation de l'erreur de modèle. La pertinence de la méthode est démontrée sur diverses applications numériques en 1D, 2D et 3D.

Lustre est un langage de programmation spécialement conçu pour la réalisation des systèmes réactifs. Le besoin de garantir que ces systèmes ont un comportement conforme a celui attendu nécessite de définir et de mettre en œuvre des méthodes de vérification formelle des programmes lustre, qui sont relatées dans cette thèse. La vérification d'un système consiste a contrôler que tous ses comportements sont corrects vis-a-vis de ses spécifications. Les comportements d'un programme lustre peuvent classiquement être représentés par une machine d'états finis, dont la génération permet de vérifier ses spécifications. La methode standard mettant en œuvre ce principe est limitée par le probleme d'explosion de la machine générée, qui n'est pas minimale. Un nouvel algorithme évitant ce probleme est présenté. Son implémentation nécessite l'emploi d'une technique de représentation et de manipulation symbolique de la machine (bdds), dont le cout d'utilisation est largement abaisse grâce a de nombreuses optimisations. Basées sur cette technique, deux autres implémentations originales de la methode standard et de la nouvelle methode proposée ci-dessus sont décrites. Les aspects de diagnostic correspondant au cas ou les programmes sont incorrects vis-a-vis de leurs spécifications sont aussi abordes

Dans le cadre de cette thèse, nous nous intéressons à la vérification de systèmes réactifs critiques et temps réel développés a l'aide de langages flots de données synchrones. Plus particulièrement nous avons considéré les propriétés de sureté pour les applications réalisées dans un des deux langages, saga produit de Merlin Gerin/ses, ou lustre crée au LGI. La méthode de vérification, pour laquelle un prototype a été réalise, est l'évaluation de propriétés sur un modèle des programmes. Un langage de spécification adapte au contexte des systèmes réactifs temps réel, avec sa sémantique formelle, est défini; ce langage comprend plusieurs opérateurs temporels. Le désir d'automatiser la vérification a nécessité la définition de la sémantique formelle de saga. Plusieurs modèles pour les programmes ont alors été étudiés: les arbres des exécutions comme base d'expression commune des sémantiques, les graphes d'états et automates de contrôle pour la mise en œuvre de la vérification. L'utilisation de moyens existants de vérification, fondée sur l'évaluation de propriétés sur un modèle des programmes, a été étudiée et évaluée. Ces moyens sont relatifs a des logiques temporelles arborescentes et des mu-calculs propositionnels. Une nouvelle approche pour la spécification et la vérification de propriétés de sureté, mettant en œuvre les caractéristiques du langage lustre, est développée. Elle s'appuie sur l'utilisation de lustre lui-même comme langage de spécification et présente les avantages suivants: formalisme commun pour la programmation et la spécification, utilisation du compilateur pour la vérification, possibilité de preuves modulaires

Contribution à l'approche inferentielle pour l'introduction de la notion de type en Prolog. Cette approche consiste à déduire automatiquement d'un programme les types des prédicats. Le programmeur peut ainsi s'assurer de la conformité du programme à ses intentions. Une méthode d'inférence de type pour Prolog est présentée. Elle se base sur une simulation de l'unification et une simulation de la résolution, avec un traitement particulier sur les appels récursifs

É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

Description d'un outil d'aide à la conception et à la vérification de systèmes communicants qui est basé sur le calcul CCS de Milner.

Dans le monde des systèmes qui utilisent des communications sous forme de diffusion de groupes, le critère de sécurité devient un facteur de plus en plus important. Le choix des mécanismes pour la protection de cette communication, mécanismes basés sur des échanges de clés symétriques et asymétriques, influe sur l'efficacité du système. Nous avons procédé à l'analyse des besoins et nous avons défini un modèle qui permet de représenter la dynamique des groupes et la communication entre leurs membres. Nous avons défini l'architecture d'un système dont l'élément central est la fonction de création, d'échange et de mise en place correcte des clés. La modélisation de ce système dans un environnement UML 2.0 a permis son analyse en termes de garantie de propriétés temporelles et de sécurité. L'approche suivie pour l'étude des exigences temporelles est généralisable à de nombreux systèmes distribués. La valorisation de nos études a été faite dans le cadre du projet national RNRT SAFECAST.