Abstract FR:

Cette thèse décrit l'application de techniques de vérification automatiques aux systèmes réactifs synchrones. Cette étude a mené à l'implantation d'outils de vérification de la partie contrôle de programmes ESTEREL validés sur divers programmes. Cette thèse présente enfin une étude pour étendre ces outils de vérification à l'interprétation des données. La vérification de propriétés s'obtient par abstractions et parcours exhaustifs d'un modèle des comportements du programme. Ce modèle peut-être, soit explicite et décrit par un automate, soit implicite et décrit par un système d'équations booléennes avec registres. Un algorithme de minimisation à partir de la représentation explicite est proposé et implémenté. La vérification par observateur de propriétés de sûreté et de vivacité a aussi été implantée. L'automate global du programme ne peut-pas toujours être directement construit. Pour le construire ont été implantées les techniques d'abstraction et de réduction compositionnelle. Ces outils ont été validés notamment sur le cas d'étude d'une turbine à vapeur et d'une cellule de production. Des algorithmes efficaces de calcul d'espace des états à partir de la représentation implicite du programme permettent de traiter des programmes de taille importante. Nous présentons une étude pour étendre ce calcul à l'interprétation de données dans des types finis en codant séparement les parties opérations sur le contrôle et opérations sur les données.