La empresa INVAP, junto con investigadores del Conicet, desarrollan herramientas que permiten verificar el software utilizado en la generación de energía nuclear para garantizar su calidad y detectar errores de manera temprana.
El proyecto "Desarrollo de metodologías de verificación para componentes de software de sistemas relevantes para la seguridad" cuenta con el financiamiento y la gestión de la Fundación Sadosky, institución público privada que favorece la articulación entre el sistema científico-tecnológico, por tratarse de una de las 16 propuestas seleccionadas en la edición 2022 de la convocatoria Soluciones Innovadoras para Desafíos de Software, que llevaron a cabo junto con el Ministerio de Ciencia, Tecnología e Innovación.
El objetivo de esta iniciativa es adaptar diversas técnicas de verificación de software, utilizando lenguajes y procesos de diseño para garantizar sistémicamente el correcto funcionamiento de componentes críticos. Los sistemas críticos son aquellos que tienen tiempos de acción muy específicos al estar involucrados, por ejemplo, en las cadenas de medición de un reactor, en las que se calculan variables como la reactividad o la potencia y que forman parte, a su vez, de las cadenas de seguridad del reactor.
Con el fin de lograr este propósito, se encuentra en desarrollo un lenguaje de programación de un nivel avanzado que pueda ser examinado con las herramientas de verificación. Esto permitirá la generación de código ejecutable que integre las propiedades verificadas durante su diseño.
"Buscamos obtener un set de herramientas que permitan la verificación formal de un software específico y, complementariamente, generar metodologías que se puedan aplicar a otras ramas de la empresa donde se utilice software en sistemas críticos", explicó Andrés Darío Cassagnes, ingeniero electrónico del departamento de Instrumentación Nuclear de INVAP.
En el marco del proyecto, ya se generó un prototipo funcional de un banco de pruebas que se encarga de indicarle al software que se está analizando, que debe funcionar como si estuviera conectado al hardware del reactor. Mediante esta simulación, se inyectan una serie de señales de entrada y luego se reciben las señales de salida, para verificar que esas salidas sean las esperadas.
El próximo paso consiste en generalizar ese banco de pruebas para extender a otros softwares y proceder a metodologías de análisis temporales. "La idea es avanzar a un banco de pruebas mejorado, que pueda analizar no solo que las salidas sean las que corresponden, sino que ocurran en el tiempo esperado en el que tienen que ocurrir", comentó Cassagnes, quien se ocupa de brindar la información y la asistencia necesarias al grupo de trabajo del Instituto de Ciencias de la Computación (ICC) de la Facultad de Ciencias Exactas y Naturales (UBA), a cargo del investigador y especialista en verificación de software Carlos López Pombo.
"La Fundación Sadosky tiene un rol fundamental principalmente en el project management de la iniciativa, porque la vinculación entre la industria y la academia suele tener inconvenientes por los tiempos y los idiomas que se hablan en cada ámbito. Tenemos la expectativa de que esta sea la primera de muchas colaboraciones con la academia para mejorar nuestros propios procesos de trabajo y mejorar nuestros productos", agregó Cassagnes.
Ricardo Medel, director del área de Vinculación Tecnológica de la Fundación Sadosky expresó: "un proceso de verificación generalizable va a permitir el diseño y construcción de sistemas más seguros, contribuyendo a las posibilidades de innovación y aprovechamiento eficiente de las nuevas tecnologías".
