Détermination de l'équivalence comportementale d'algorithmes de contrôle - commande

La norme IEC 61508 sur la sécurité fonctionnelle des systèmes critiques préconise l'utilisation de méthodes formelles pour les logiciels de niveau SIL (Safety Integrated Level) 3 et 4. Cependant aucune précision sur l'utilisation de ces méthodes formelles dans le cycle de développement n'est indiquée. Le but général des travaux présentés dans cet article, et réalisés dans le cadre d'un contrat de recherche financé par Alstom Power Plant Information and Control Systems, est d'introduire des méthodes formelles pour aider à la réalisation d'applications de contrôle commande certifiées. Plus précisément cet article propose une méthode s'appuyant sur un outil de vérification formelle et permettant de vérifier que les représentations du même algorithme de commande dans des langages différents conduisent au même comportement si on se réfère aux entrées/sorties du système de commande. Cette méthode repose sur une représentation par automates à états traduisant, à un niveau d'abstraction adéquat, le comportement des langages d'automatismes du point de vue des entrées/sorties et traductible dans la syntaxe d'un outil de model - checking. Enfin, une application de cette méthode formelle dans le cadre industriel est présentée, montrant les résultats d'expériences sur un cas réel de contrôle de centrale thermique en utilisant l'outil de model - checking NuSMV et un outil de traduction automatique, développé dans le cadre de ces travaux.