EDF evalúa la seguridad de software de centrales nucleares con métodos formales y Polyspace
Este enfoque garantiza la conformidad con estándares internacionales y reduce al máximo los riesgos relacionados con software
“El análisis de Polyspace fomenta la confianza y proporciona pruebas sólidas de que el código estará libre de problemas en tiempo de ejecución. También lo usamos como ayuda para justificar la seguridad de nuestro parque de centrales eléctricas donde era necesario sustituir instrumentos de hardware obsoletos por otros basados en software. El uso de Polyspace fundamenta la reducción de pruebas independientes. Por ejemplo, la solidez del software se puede demostrar en Polyspace Bug Finder empleando comprobaciones más estrictas, y luego corroborarla con Polyspace Code Prover; esto permite centrar las pruebas en propiedades funcionales del software”.
Resultados principales
- Las herramientas de Polyspace ayudaron a demostrar la ausencia de errores y vulnerabilidades en tiempo de ejecución en el software del proveedor
- Polyspace Code Prover y Polyspace Bug Finder permitieron a EDF cumplir con el exigente marco de calificación de la industria nuclear
- Las herramientas de Polyspace ayudaron a demostrar una densidad de errores de tan solo 0,07 errores por cada 1000 líneas de código
EDF es el mayor proveedor de energía sin emisiones de carbono del Reino Unido. Para garantizar una calidad constante del software en su última generación de centrales nucleares, EDF utiliza las herramientas de Polyspace® para evaluar de manera independiente la seguridad del software de código proporcionado por el proveedor.
Los operadores de la industria nuclear civil del Reino Unido deben cumplir con un exigente marco de calificación para demostrar que los riesgos relacionados con software de sistemas de seguridad se reducen al máximo. La aplicación de reglas de codificación y el uso de análisis estático de código basado en métodos formales para demostrar la ausencia de ciertos tipos de errores y vulnerabilidades proporcionan pruebas contundentes de que se está logrando este objetivo.
El marco de calificación se basa en dos elementos independientes descritos en NS-TAST-GD-046: Excelencia en la producción (PE) y Medidas independientes de fomento de la confianza (ICBM). Para la PE se requiere que el software cumpla con estándares internacionales relevantes, tales como IEC 61508, IEC 62138 e IEC 60880, mientras que las ICBM exigen la realización de pruebas y análisis adicionales de manera independiente del proveedor. En el caso de las ICBM con seguridad de Clase 2, se espera análisis estático de código, que es obligatorio para las ICBM con seguridad de Clase 1. Además, el uso de métodos formales para demostrar la ausencia de errores y vulnerabilidades en tiempo de ejecución proporciona pruebas contundentes de que se reducen los riesgos del software de sistemas de seguridad.
Durante el proceso de PE, EDF utiliza los productos de Polyspace para comprobar vulnerabilidades y mantener la conformidad con codificación MISRA™. En el caso de las ICBM, se emplea Polyspace Bug Finder™ típicamente en aplicaciones de Clase 2, para detectar vulnerabilidades de seguridad y protección, que luego se evalúan y analizan para determinar su impacto en la seguridad del sistema. En aplicaciones de Clase 1, también se utiliza Polyspace Code Prover™, para comprobar la ausencia de errores en tiempo de ejecución.
Estas comprobaciones ayudan a EDF a demostrar que ciertos errores en tiempo de ejecución se reducen al máximo, lo que constituye una base sólida para obtener aprobación y garantiza la excelencia en toda la cadena de suministro. En un proyecto reciente, el equipo de trabajo de EDF demostró una densidad de errores muy baja, de tan solo 0,07 errores por cada 1000 líneas de código. Dadas estas ventajas, las herramientas de Polyspace también se usan como ayuda para justificar la seguridad del parque de centrales eléctricas de EDF, ya que han permitido la obsolescencia planificada de instrumentos donde ya no están disponibles instrumentos basados en hardware y se deben justificar sus sustitutos basados en software.
Productos utilizados