Abstract FR:

Cette these etudie la verification des programmes ecrits dans le langage parallele synchrone esterel. Nous proposons deux methodes de verification. La premiere est basee sur la logique temporelle: les proprietes que le programme doit satisfaire sont exprimees par des formules de logique temporelle que l'on verifie sur l'automate decrivant le comportement du programme. La seconde utilise la reduction de l'automate pour mettre en evidence des comportements particuliers du programme. On etudie ensuite un exemple: on programme en esterel le modem d'un minitel, et on verifie son fonctionnement. Ceci nous permet de comparer les deux approches de verification proposees