Représentations formelles efficaces pour l'aide à la certification de contrôleurs logiques industriels

Ce mémoire propose des représentations formelles pour contrôleurs logiques industriels qui visent à améliorer le passage à l'échelle des techniques de model-checking. Ces vérifications, focalisées sur les propriétés extrinsèques, permettent d'améliorer la sûreté et aident à la certification de ces contrôleurs. Premièrement, la représentation de contrôleurs ne comprend que les états qui sont pertinents pour la preuve de propriétés et minimise le nombre de variables qui caractérisent chaque état. Puis une représentation de chaque bloc fonctionnel, décrit dans un nouveau langage formel adapté à nos besoins, est incluse dans la représentation du contrôleur. Ces représentations permettent la vérification formelle du contrôleur, même avec des programmes de grande taille. La comparaison avec de précédentes représentations, ainsi que leur utilisation dans un contexte industriel, valide nos représentations et quantifie leur efficacité.