Analyse prévisionnelle des fautes des systèmes embarqués discrets par vérification model-based

Les méthodes usuelles d'analyse prévisionnelle des fautes s'intéressent principalement aux fautes aléatoires de composants physiques. Dans le cas des systèmes embarqués, qui comportent de nombreuses boucles de commande, il importe de vérifier également si une commande propage (ou ne propage pas) les fautes aléatoires du processus qu'elle contrôle, ceci afin d'éviter une défaillance du système. Ce papier propose une telle méthode d'analyse, basée sur une technique de vérification formelle model-based. Le principe de cette méthode est de vérifier qu'une propriété traduisant l'absence de défaillance est satisfaite (ou non) par un modèle formel du système bouclé. Si cette propriété est vérifiée, la commande ne propage pas la faute ; sinon, l'analyse d'un contre-exemple permet de modifier la commande afin d'améliorer la sûreté globale du système.