Abstract FR:

Ce travail se place dans le cadre général de l'étude de méthodes, langages et outils permettant la spécification et le développement d'applications de type contrôle-commande temps-réel. Nous nous intéresserons d'une part à un langage métier de l'automatisme, le GRAFCET, et d'autre part à la méthodologie de programmation synchrone et en particulier au langage SIGNAL. Le premier formalisme est depuis longtemps utilisé dans l'industrie en raison de son pouvoir d'expression important et de son aspect graphique attractif. Mais sa sémantique n'est définie que de manière informelle, ce qui constitue une limite, en particulier, au niveau de la sûreté d'utilisation. Les formalismes synchrones sont quant à eux clairement définis et reposent sur une hypothèse de synchronisme des entrées et des sorties. Cette hypothèse permet de simplifier la construction de programmes et d'utiliser des systèmes de preuves. Nous montrons dans ce travail, que les apports méthodologiques de l'approche synchrone peuvent aider à la définition de la sémantique du GRAFCET et nous en présentons l'application avec le langage SIGNAL. Nous exposons aussi deux méthodes de preuves applicables au GRAFCET: la première est basée sur l'étude directe de système de transitions et la seconde utilise l'outil de vérification développé pour le langage SIGNAL