Résumé
Les travaux de cette thèse s’intègrent dans un projet industriel mené par la R&D de EDF visant à automatiser la génération de tests pour les systèmes de contrôle-commande des centrales nucléaires du palier N4. Les fonctions et les commandes remplies par ces systèmes sont exprimées sous la forme de Diagrammes Logiques (schémas comportant des portes ET, OU, des mémoires etc.) implémentés par des Automates Programmables Industriels (API). Les traitements exécutés par les systèmes de contrôle-commande évoluent tout au long de la vie d’une installation nucléaire suite à des évolutions réglementaires (post-Fukushima), suite à des évolutions fonctionnelles (amélioration des performances, impact de la transition énergétique) ou suite à des actions de maintenance (changements de certains composants). L’assurance du bon fonctionnement de ces traitements, la non-régression des parties non modifiées ainsi que le respect des normes de sûreté contrôlés par les autorités concernées fait l’objet de tout une procédure de test. Cette procédure consiste à jouer des scénarios de test sur le système modifié en comparant son comportement aux spécifications. Aujourd’hui, les scénarios de test sont générés manuellement par une équipe d’experts à partir de nombreux diagrammes logiques. Beaucoup de ces diagrammes sont de tailles importantes et comportent des boucles entre les blocs logiques ce qui rend la tâche de génération manuelle assez complexe et coûteuse. Cette thèse s’intéresse à la mise en place de méthodes formelles permettant de générer automatiquement des scenarios de tests fonctionnels à partir des Diagramme Logiques de spécification et de règles métier à valider sur les systèmes de contrôle-commande. Le diagramme logique est un langage métier facilement interprétable par les experts sans qu’il présente de sémantiques formelles. Une définition formelle a été donc établie ainsi qu’une modélisation par des graphes d’états/transitions dans la fin de permettre l’utilisation des méthodes formelles de la théorie des graphes pour la vérification de certaines propriétés intrinsèques ainsi que la génération de séquences de tests de validation. Cependant, la représentation exhaustive de l’ensemble des états et transitions possibles s’est avéré assez complexe pour les diagrammes de grandes tailles. Une deuxième approche de modélisation des diagrammes logiques par les formalismes de la Logique Linéaire Temporelle (LTL) a donc été proposée. Cela a rendu possible l’exploitation des techniques de Model-Checking pour la génération de scénarios répondant à des objectifs fonctionnels de test donnés. Une implémentation de cette approche a été réalisée et testée sur des cas réels de diagrammes et a permis de fournir, dans des délais raisonnables, les scénarios de tests voulus. Plus de tests sur d’autre cas de diagrammes de tailles et complexités structurelles différentes sont prévus avant son intégration dans l’outil final développé dans le cadre du projet.