Verificación formal de software para reactores nucleares

Investigadores de CONICET desarrollan un proyecto orientado a aplicar técnicas de verificación formal de software, destinadas a sistemas críticos en el campo de la producción de reactores nucleares de INVAP. El equipo está integrado por Carlos López Pombo (CITECCA, UNRN), Juan Pablo Galeotti (ICC UBA/CONICET) y Germán Regis (Departamento de Computación, UNRC).

INVAP es una empresa estatal argentina que desarrolla y comercializa productos tecnológicos de avanzada. Está dedicada al diseño, integración y construcción de plantas, equipamientos y dispositivos en áreas de alta complejidad como energía nuclear, tecnología aeroespacial, tecnología industrial, sistemas médicos y defensa, seguridad y ambiente. Se fundó en 1976 y, a raíz de su importante crecimiento, se constituyó en un caso paradigmático de desarrollo al conectar la investigación básica con la industria y alcanzar así la vanguardia en estas áreas.

A partir del contacto con la Gerencia de Tecnología de INVAP, por parte de un investigador especializado en software de la Universidad Nacional de Río Negro, se buscó encontrar problemas comunes de interés entre ambas partes y así surgió la posibilidad de la colaboración académica para la verificación formal de software de sistemas críticos, en este caso reactores nucleares. Todo ello teniendo en cuenta que -debido a las técnicas y metodologías muy específicas requeridas en las soluciones- el proyecto necesitaba de la intervención de científicos del ámbito académico.

La finalidad del proyecto es realizar un diagnóstico general de una familia de artefactos de software, utilizados como parte de la cadena de monitoreo de un reactor nuclear producido por INVAP, para luego proceder a su análisis formal a fin de certificar el cumplimiento de ciertas propiedades de interés. Tal es así que encarar este problema supone la creación de herramientas que permitan verificar los programas, previamente a su utilización, para garantizar la calidad de los mismos, detectar errores de manera temprana y poder corregirlos antes de que sean utilizados directamente en la planta.

El equipo que realiza la verificación formal del software está conformado por Juan Pablo Galeotti (Investigador del Instituto de Ciencias de la Computación UBA-CONICET, Profesor y Director del Departamento de Computación, Exactas-UBA), Germán Regis (Profesor e Investigador del Departamento de Computación de la Universidad Nacional de Río Cuarto) y Carlos López Pombo (Investigador de CONICET en el Centro Interdisciplinario de Telecomunicaciones, Electrónica, Computación y Ciencia Aplicada, CITECCA, de la Sede Andina de la Universidad Nacional de Río Negro y actualmente de licencia como Profesor del DC-Exactas-UBA), quien coordina el proyecto desde San Carlos de Bariloche.

En una reciente entrevista con un medio local, López Pombo destaca: “En este proyecto ofrecemos técnicas y metodologías capaces de asegurar la calidad de los elementos de software involucrados en la operación del reactor nuclear, teniendo en cuenta que para un artefacto con la complejidad de esta naturaleza se necesita no sólo de seguridad sino de calidad operativa con altos niveles de certificación, especialmente a la hora de evaluar potenciales problemas”. Y complementa que gran parte de su carrera en investigación la dedicó a problemáticas de verificación de software, incluyendo diversos proyectos de vinculación tecnológica. “En este caso cuando uno tiene sistemas críticos, es decir sistemas cuyos fallos pueden generar graves consecuencias, tanto humanas como materiales, es necesario aplicar técnicas que provean mayores niveles de certeza acerca del comportamiento de esos sistemas”, concluye. En otras palabras, el trabajo de los investigadores resultará clave para generar un estándar de calidad de estos artefactos de energía nuclear y, al mismo tiempo, ofrecer garantías de comportamiento sobre el producto del que forman parte.

Actualmente el proyecto cuenta con el apoyo y financiamiento de la Fundación Sadosky, institución público-privada cuyo objetivo es favorecer la articulación entre el sistema científico-tecnológico y la estructura productiva en todo lo referido a la temática de las Tecnologías de la Información y la Comunicación.

En este video, elaborado por la Fundación Sadosky, se puede conocer más acerca de la iniciativa: