{"id":2486,"date":"2023-05-09T10:21:37","date_gmt":"2023-05-09T13:21:37","guid":{"rendered":"https:\/\/icc.fcen.uba.ar\/?p=2486"},"modified":"2023-06-21T12:12:33","modified_gmt":"2023-06-21T15:12:33","slug":"verificacion-formal-de-software-para-reactores-nucleares","status":"publish","type":"post","link":"https:\/\/icc.fcen.uba.ar\/en\/verificacion-formal-de-software-para-reactores-nucleares\/","title":{"rendered":"Verificaci\u00f3n formal de software para reactores nucleares"},"content":{"rendered":"<div class=\"fusion-fullwidth fullwidth-box fusion-builder-row-1 fusion-flex-container nonhundred-percent-fullwidth non-hundred-percent-height-scrolling\" style=\"--awb-border-radius-top-left:0px;--awb-border-radius-top-right:0px;--awb-border-radius-bottom-right:0px;--awb-border-radius-bottom-left:0px;--awb-flex-wrap:wrap;\" ><div class=\"fusion-builder-row fusion-row fusion-flex-align-items-flex-start fusion-flex-content-wrap\" style=\"max-width:1144px;margin-left: calc(-4% \/ 2 );margin-right: calc(-4% \/ 2 );\"><div class=\"fusion-layout-column fusion_builder_column fusion-builder-column-0 fusion_builder_column_1_1 1_1 fusion-flex-column\" style=\"--awb-bg-size:cover;--awb-width-large:100%;--awb-margin-top-large:0px;--awb-spacing-right-large:1.92%;--awb-margin-bottom-large:20px;--awb-spacing-left-large:1.92%;--awb-width-medium:100%;--awb-order-medium:0;--awb-spacing-right-medium:1.92%;--awb-spacing-left-medium:1.92%;--awb-width-small:100%;--awb-order-small:0;--awb-spacing-right-small:1.92%;--awb-spacing-left-small:1.92%;\"><div class=\"fusion-column-wrapper fusion-column-has-shadow fusion-flex-justify-content-flex-start fusion-content-layout-column\"><div class=\"fusion-text fusion-text-1\"><p><strong>Investigadores de CONICET desarrollan un proyecto orientado a aplicar t\u00e9cnicas de verificaci\u00f3n formal de software, destinadas a sistemas cr\u00edticos en el campo de la producci\u00f3n de reactores nucleares de INVAP. El equipo est\u00e1 integrado por Carlos L\u00f3pez Pombo (CITECCA, UNRN), Juan Pablo Galeotti (ICC UBA\/CONICET) y Germ\u00e1n Regis (Departamento de Computaci\u00f3n, UNRC).<\/strong><\/p>\n<p>INVAP es una empresa estatal argentina que desarrolla y comercializa productos tecnol\u00f3gicos de avanzada. Est\u00e1 dedicada al dise\u00f1o, integraci\u00f3n y construcci\u00f3n de plantas, equipamientos y dispositivos en \u00e1reas de alta complejidad como energ\u00eda nuclear, tecnolog\u00eda aeroespacial, tecnolog\u00eda industrial, sistemas m\u00e9dicos y defensa, seguridad y ambiente. Se fund\u00f3 en 1976 y, a ra\u00edz de su importante crecimiento, se constituy\u00f3 en un caso paradigm\u00e1tico de desarrollo al conectar la investigaci\u00f3n b\u00e1sica con la industria y alcanzar as\u00ed la vanguardia en estas \u00e1reas.<\/p>\n<p>A partir del contacto con la Gerencia de Tecnolog\u00eda de INVAP, por parte de un investigador especializado en software de la Universidad Nacional de R\u00edo Negro, se busc\u00f3 encontrar problemas comunes de inter\u00e9s entre ambas partes y as\u00ed surgi\u00f3 la posibilidad de la colaboraci\u00f3n acad\u00e9mica para la verificaci\u00f3n formal de software de sistemas cr\u00edticos, en este caso reactores nucleares. Todo ello teniendo en cuenta que -debido a las t\u00e9cnicas y metodolog\u00edas muy espec\u00edficas requeridas en las soluciones- el proyecto necesitaba de la intervenci\u00f3n de cient\u00edficos del \u00e1mbito acad\u00e9mico.<\/p>\n<p>La finalidad del proyecto es realizar un diagn\u00f3stico 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\u00e1lisis formal a fin de certificar el cumplimiento de ciertas propiedades de inter\u00e9s. Tal es as\u00ed que encarar este problema supone la creaci\u00f3n de herramientas que permitan verificar los programas, previamente a su utilizaci\u00f3n, para garantizar la calidad de los mismos, detectar errores de manera temprana y poder corregirlos antes de que sean utilizados directamente en la planta.<\/p>\n<p>El equipo que realiza la verificaci\u00f3n formal del software est\u00e1 conformado por <strong>Juan Pablo Galeotti<\/strong> (Investigador del Instituto de Ciencias de la Computaci\u00f3n UBA-CONICET, Profesor y Director del Departamento de Computaci\u00f3n, Exactas-UBA), <strong>Germ\u00e1n Regis<\/strong> (Profesor e Investigador del Departamento de Computaci\u00f3n de la Universidad Nacional de R\u00edo Cuarto) y <strong>Carlos L\u00f3pez Pombo<\/strong> (Investigador de CONICET en el Centro Interdisciplinario de Telecomunicaciones, Electr\u00f3nica, Computaci\u00f3n y Ciencia Aplicada, CITECCA, de la Sede Andina de la Universidad Nacional de R\u00edo Negro y actualmente de licencia como Profesor del DC-Exactas-UBA), quien coordina el proyecto desde San Carlos de Bariloche.<\/p>\n<p>En una <a href=\"https:\/\/admin.radionacional.com.ar\/crean-herramientas-para-verificar-sistemas-para-reactores-nucleares\/\" target=\"_blank\" rel=\"noopener noreferrer\">reciente entrevista con un medio local<\/a>, L\u00f3pez Pombo destaca: \u201c<em>En este proyecto ofrecemos t\u00e9cnicas y metodolog\u00edas capaces de asegurar la calidad de los elementos de software involucrados en la operaci\u00f3n del reactor nuclear, teniendo en cuenta que para un artefacto con la complejidad de esta naturaleza se necesita no s\u00f3lo de seguridad sino de calidad operativa con altos niveles de certificaci\u00f3n, especialmente a la hora de evaluar potenciales problemas<\/em>\u201d. Y complementa que gran parte de su carrera en investigaci\u00f3n la dedic\u00f3 a problem\u00e1ticas de verificaci\u00f3n de software, incluyendo diversos proyectos de vinculaci\u00f3n tecnol\u00f3gica. \u201c<em>En este caso cuando uno tiene sistemas cr\u00edticos, es decir sistemas cuyos fallos pueden generar graves consecuencias, tanto humanas como materiales, es necesario aplicar t\u00e9cnicas que provean mayores niveles de certeza acerca del comportamiento de esos sistemas<\/em>\u201d, concluye. En otras palabras, el trabajo de los investigadores resultar\u00e1 clave para generar un est\u00e1ndar de calidad de estos artefactos de energ\u00eda nuclear y, al mismo tiempo, ofrecer garant\u00edas de comportamiento sobre el producto del que forman parte.<\/p>\n<p>Actualmente el proyecto cuenta con el apoyo y financiamiento de la Fundaci\u00f3n Sadosky, instituci\u00f3n p\u00fablico-privada cuyo objetivo es favorecer la articulaci\u00f3n entre el sistema cient\u00edfico-tecnol\u00f3gico y la estructura productiva en todo lo referido a la tem\u00e1tica de las Tecnolog\u00edas de la Informaci\u00f3n y la Comunicaci\u00f3n.<\/p>\n<p>En este video, elaborado por la Fundaci\u00f3n Sadosky, se puede conocer m\u00e1s acerca de la iniciativa:<\/p>\n<p><iframe title=\"YouTube video player\" src=\"https:\/\/www.youtube.com\/embed\/ZH7YDlMriK8\" width=\"560\" height=\"315\" frameborder=\"0\" allowfullscreen=\"allowfullscreen\"><\/iframe><\/p>\n<\/div><\/div><\/div><\/div><\/div>\n","protected":false},"excerpt":{"rendered":"<p>Investigadores de CONICET desarrollan un proyecto orientado a aplicar t\u00e9cnicas de verificaci\u00f3n formal de software, destinadas a sistemas cr\u00edticos en el campo de la producci\u00f3n de reactores nucleares de INVAP. El equipo est\u00e1 integrado por Carlos L\u00f3pez Pombo (CITECCA, UNRN), Juan Pablo Galeotti (ICC UBA\/CONICET) y Germ\u00e1n Regis (Departamento de Computaci\u00f3n, UNRC).<\/p>\n","protected":false},"author":9,"featured_media":2488,"comment_status":"open","ping_status":"open","sticky":false,"template":"","format":"standard","meta":{"footnotes":""},"categories":[69],"tags":[],"class_list":["post-2486","post","type-post","status-publish","format-standard","has-post-thumbnail","hentry","category-vinculacion"],"_links":{"self":[{"href":"https:\/\/icc.fcen.uba.ar\/en\/wp-json\/wp\/v2\/posts\/2486","targetHints":{"allow":["GET"]}}],"collection":[{"href":"https:\/\/icc.fcen.uba.ar\/en\/wp-json\/wp\/v2\/posts"}],"about":[{"href":"https:\/\/icc.fcen.uba.ar\/en\/wp-json\/wp\/v2\/types\/post"}],"author":[{"embeddable":true,"href":"https:\/\/icc.fcen.uba.ar\/en\/wp-json\/wp\/v2\/users\/9"}],"replies":[{"embeddable":true,"href":"https:\/\/icc.fcen.uba.ar\/en\/wp-json\/wp\/v2\/comments?post=2486"}],"version-history":[{"count":2,"href":"https:\/\/icc.fcen.uba.ar\/en\/wp-json\/wp\/v2\/posts\/2486\/revisions"}],"predecessor-version":[{"id":2489,"href":"https:\/\/icc.fcen.uba.ar\/en\/wp-json\/wp\/v2\/posts\/2486\/revisions\/2489"}],"wp:featuredmedia":[{"embeddable":true,"href":"https:\/\/icc.fcen.uba.ar\/en\/wp-json\/wp\/v2\/media\/2488"}],"wp:attachment":[{"href":"https:\/\/icc.fcen.uba.ar\/en\/wp-json\/wp\/v2\/media?parent=2486"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/icc.fcen.uba.ar\/en\/wp-json\/wp\/v2\/categories?post=2486"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/icc.fcen.uba.ar\/en\/wp-json\/wp\/v2\/tags?post=2486"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}