Seguridad en energa nuclear: desarrollan metodologas de verificacin formal de software para sistemas crticos
La empresa INVAP, junto con investigadores del Conicet, desarrollan herramientas que permiten verificar el software utilizado en la generacin de energa nuclear para garantizar su calidad y detectar errores de manera temprana.
El proyecto «Desarrollo de metodologas de verificacin para componentes de software de sistemas relevantes para la seguridad» cuenta con el financiamiento y la gestin de la Fundacin Sadosky, institucin pblico privada que favorece la articulacin entre el sistema cientfico-tecnolgico, por tratarse de una de las 16 propuestas seleccionadas en la edicin 2022 de la convocatoria Soluciones Innovadoras para Desafos de Software, que llevaron a cabo junto con el Ministerio de Ciencia, Tecnologa e Innovacin.
El objetivo de esta iniciativa es adaptar diversas tcnicas de verificacin de software, utilizando lenguajes y procesos de diseo para garantizar sistmicamente el correcto funcionamiento de componentes crticos. Los sistemas crticos son aquellos que tienen tiempos de accin muy especficos al estar involucrados, por ejemplo, en las cadenas de medicin 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 propsito, se encuentra en desarrollo un lenguaje de programacin de un nivel avanzado que pueda ser examinado con las herramientas de verificacin. Esto permitir la generacin de cdigo ejecutable que integre las propiedades verificadas durante su diseo.
«Buscamos obtener un set de herramientas que permitan la verificacin formal de un software especfico y, complementariamente, generar metodologas que se puedan aplicar a otras ramas de la empresa donde se utilice software en sistemas crticos», explic Andrs Daro Cassagnes, ingeniero electrnico del departamento de Instrumentacin 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 simulacin, se inyectan una serie de seales de entrada y luego se reciben las seales de salida, para verificar que esas salidas sean las esperadas.
El prximo paso consiste en generalizar ese banco de pruebas para extender a otros softwares y proceder a metodologas de anlisis 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 informacin y la asistencia necesarias al grupo de trabajo del Instituto de Ciencias de la Computacin (ICC) de la Facultad de Ciencias Exactas y Naturales (UBA), a cargo del investigador y especialista en verificacin de software Carlos Lpez Pombo.
«La Fundacin Sadosky tiene un rol fundamental principalmente en el project management de la iniciativa, porque la vinculacin 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 Vinculacin Tecnolgica de la Fundacin Sadosky expres: «un proceso de verificacin generalizable va a permitir el diseo y construccin de sistemas ms seguros, contribuyendo a las posibilidades de innovacin y aprovechamiento eficiente de las nuevas tecnologas».
