EDF évalue la sécurité logicielle de ses centrales nucléaires à l’aide de méthodes formelles avec Polyspace
Cette approche assure la conformité aux normes internationales tout en minimisant les risques liés aux logiciels
« L’analyse Polyspace renforce la confiance, en fournissant des preuves solides que le code ne présentera aucun problème d’exécution. Nous avons aussi utilisé cet outil à des fins de justification de la sécurité dans notre parc existant de centrales électriques où des dispositifs physiques obsolètes devaient être remplacés par des dispositifs basés sur des logiciels. Notre utilisation des outils Polyspace nous permet de réduire les efforts de tests indépendants. Par exemple, la robustesse des logiciels peut être démontrée dans Polyspace Bug Finder en utilisant des vérifications plus strictes et prouvée avec Polyspace Code Prover, ce qui permet de focaliser les tests sur les propriétés fonctionnelles des logiciels. »
Principaux résultats
- Les outils Polyspace ont permis de prouver l’absence de vulnérabilités et d’erreurs d’exécution dans les logiciels des fournisseurs
- Polyspace Code Prover et Polyspace Bug Finder ont permis à EDF de respecter le cadre de qualification rigoureux de l’industrie nucléaire
- Les outils Polyspace ont aidé à démontrer un taux de défauts inférieur à 0,07 défaut par 1 000 lignes de code
EDF utilise les produits Polyspace afin de répondre à un cadre de qualification rigoureux pour le domaine de l’énergie nucléaire, établissant ainsi une confiance indépendante dans le code critique.
EDF est le plus grand fournisseur d’énergie zéro carbone du Royaume-Uni. Pour assurer un niveau de qualité constant dans les solutions logicielles de sa dernière génération de centrales nucléaires, EDF utilise les outils Polyspace® afin d’évaluer de manière indépendante la sécurité logicielle du code provenant des fournisseurs.
Les exploitants de l’industrie nucléaire civile du Royaume-Uni doivent respecter un cadre de qualification rigoureux pour démontrer que les risques liés aux logiciels des systèmes de sécurité sont réduits au minimum. Ils doivent appliquer des règles de codage et utiliser des fonctionnalités d’analyse statique du code basées sur des méthodes formelles pour prouver l’absence de certains types d’erreurs et de vulnérabilités afin de constituer des preuves solides de la réalisation de cet objectif.
Le cadre de qualification repose sur deux colonnes indépendantes du guide NS-TAST-GD-046 : Production Excellence (PE) et Independent Confidence Building Measures (ICBM). La PE exige que les solutions logicielles satisfassent aux normes internationales pertinentes telles que CEI 61508, CEI 62138 et CEI 60880, tandis que les ICBM consistent en des tests et des analyses supplémentaires réalisés indépendamment du fournisseur. Seulement attendue dans le cadre des ICBM de classe de sécurité 2, l’analyse statique de code devient obligatoire pour les ICBM de classe de sécurité 1. De plus, lorsqu’il s’agit de prouver l’absence de vulnérabilités et d’erreurs d’exécution, l’utilisation de méthodes formelles fournit des preuves solides que les risques logiciels dans les systèmes de sécurité sont réduits.
Au cours du processus de PE, EDF utilise les produits Polyspace pour vérifier les vulnérabilités et renforcer la conformité du codage MISRA™. En ce qui concerne les ICBM, Polyspace Bug Finder™ est généralement utilisé pour les applications de classe 2 afin de détecter les vulnérabilités de sécurité, qui sont ensuite évaluées par l’analyste pour déterminer l’impact sur la sécurité du système. Pour les applications de classe 1, Polyspace Code Prover™ est aussi utilisé pour prouver l’absence d’erreurs d’exécution.
Grâce à ces contrôles, EDF peut aider à prouver que certaines erreurs d’exécution sont réduites au minimum, constituant alors une base solide pour l’approbation et assurant l’excellence tout au long de la chaîne d’approvisionnement. Dans un projet récent, l’équipe d’EDF a démontré un très faible taux de défauts : 0,07 pour 1 000 lignes de code. En raison des avantages qu’ils procurent, les outils Polyspace ont également été utilisés pour aider à la justification de la sécurité dans le parc existant de centrales électriques d’EDF, en supportant l’obsolescence planifiée des dispositifs lorsque les dispositifs physiques ne sont plus disponibles et que les remplacements basés sur les logiciels doivent être justifiés.
