Le projet « Action Incitative » fait suite de l’interaction Filtre/Diagnostic du projet ADEXEC. En effet, afin d’assurer la robustesse du filtre en mode dégradé, face aux erreurs de commande, une approche de vérification par model-checker a été mise en place. Cette vérification formelle a nécessité la modélisation de la partie opérative, des diagnostiqueurs, du filtre, de la commande la plus permissive et de l’environnement de calcul. Ce travail a permis de constituer un sujet de thèse débuté par Mehdi Chankate fin 2016.