{"id":239,"date":"2024-04-24T16:22:18","date_gmt":"2024-04-24T16:22:18","guid":{"rendered":"https:\/\/www.madrimasd.org\/blogs\/Tecnologiasdelainformacionparaelmundodelmanana\/?p=239"},"modified":"2024-04-24T16:22:18","modified_gmt":"2024-04-24T16:22:18","slug":"verificacion-descentralizada-y-distribuida-de-flujos-en-tiempo-real-mejora-de-la-supervision-en-sistemas-complejos","status":"publish","type":"post","link":"https:\/\/www.madrimasd.org\/blogs\/Tecnologiasdelainformacionparaelmundodelmanana\/2024\/04\/24\/verificacion-descentralizada-y-distribuida-de-flujos-en-tiempo-real-mejora-de-la-supervision-en-sistemas-complejos\/","title":{"rendered":"Verificaci\u00f3n descentralizada y distribuida de flujos en tiempo real: Mejora de la supervisi\u00f3n en sistemas complejos"},"content":{"rendered":"
Determinar si un programa inform\u00e1tico es correcto o defectuoso, que se comporta como se espera, es de lo que se encarga la <\/span>verificaci\u00f3n de software, la rama de investigaci\u00f3n a la que se dedica Luis Miguel Danielsson.<\/span><\/h5>\n
\"El
El investigador Luis miguel Danielsson, en el Instituto IMDEA Software<\/figcaption><\/figure>\n

Dado que el software se ha convertido en una herramienta importante para resolver una amplia gama de problemas humanos, es necesario gestionar todos los detalles sobre c\u00f3mo manejar los datos y el c\u00e1lculo en un algoritmo determinado. Pero construir software fiable es una tarea notoriamente dif\u00edcil. A\u00fan m\u00e1s, en el software concurrente o distribuido, la naturaleza intr\u00ednseca del sistema dificulta la programaci\u00f3n, al tener que gestionar dos o m\u00e1s c\u00f3mputos al mismo tiempo y comprender y gestionar sus interconexiones, como la comunicaci\u00f3n o la sincronizaci\u00f3n.<\/span><\/p>\n

En este escenario resulta fundamental disponer de herramientas para determinar mec\u00e1nicamente si un programa es correcto o defectuoso<\/strong>. Este es el \u00e1mbito de la <\/span>verificaci\u00f3n de software<\/b>, que se ocupa de garantizar que un programa se comporta como se espera, es decir, cu\u00e1l es el resultado deseado y c\u00f3mo queremos que el programa lo calcule.<\/span><\/p>\n

En este sentido, Luis Miguel Danielsson<\/a>, investigador del Instituto IMDEA Software, afirma que: \u00abVerificar sistemas reactivos es a\u00fan m\u00e1s dif\u00edcil cuando el entorno no es de naturaleza computacional, como los sistemas human-in-the-loop, que dependen del entorno f\u00edsico (como los drones) y los distribuidos (como los edificios inteligentes)<\/strong>. En estos sistemas es muy dif\u00edcil modelar con precisi\u00f3n el entorno. Por esta raz\u00f3n, las t\u00e9cnicas de <\/span>verificaci\u00f3n est\u00e1tica son a menudo limitadas o incluso pr\u00e1cticamente inviables para este tipo de sistemas en la pr\u00e1ctica\u00bb.<\/span><\/p>\n

Luis Miguel ha presentado recientemente su tesis, cuyo prop\u00f3sito es llevar la <\/span>Verificaci\u00f3n en Tiempo de Ejecuci\u00f3n a los Sistemas Descentralizados y Distribuidos<\/b> -que son, por su naturaleza concurrente, intr\u00ednsecamente complejos-, con el fin de mejorar la privacidad, la eficiencia o a\u00f1adir tolerancia a fallos en la monitorizaci\u00f3n distribuida para presentar claras ventajas sobre las soluciones centralizadas.<\/span><\/p>\n

Los objetivos generales de su tesis son tres: definir el problema de la monitorizaci\u00f3n de sistemas descentralizados y distribuidos con veredictos ricos; proponer soluciones algor\u00edtmicas a la monitorizaci\u00f3n descentralizada y probar formalmente su correcci\u00f3n; e implementar dichas soluciones y realizar evaluaciones emp\u00edricas.<\/span><\/p>\n

El Dr. Danielsson propone el uso de algoritmos correctos descentralizados y distribuidos basados en <\/span>Stream Runtime Verification<\/b> para monitorizar eficaz y eficientemente sistemas descentralizados y distribuidos ayudando en la tarea de mejorar su calidad.<\/span><\/p>\n

La soluci\u00f3n propuesta por el investigador es un enfoque de m\u00e9todo formal ligero que tiene su origen en la verificaci\u00f3n formal est\u00e1tica. La verificaci\u00f3n en tiempo de ejecuci\u00f3n intenta aliviar los problemas al evitar modelar el entorno, y los problemas de escalabilidad al restringir el an\u00e1lisis a una sola traza y no a todas las trazas del sistema. <\/span><\/p>\n

La primera contribuci\u00f3n de la Tesis es un <\/span>algoritmo de monitorizaci\u00f3n descentralizado<\/b> basado en streams para redes s\u00edncronas. A continuaci\u00f3n, Luis Miguel presenta <\/span>extensiones para modelos de red m\u00e1s realistas, concretamente <\/span>redes as\u00edncronas temporizadas. Por \u00faltimo, introduce una mejora <\/span>tolerante a fallos que permite a los monitores ser resistentes frente a la duplicaci\u00f3n y p\u00e9rdida de mensajes.<\/span><\/p>\n

La segunda aportaci\u00f3n de la Tesis es una comparaci\u00f3n y traducci\u00f3n entre lenguajes s\u00edncronos y as\u00edncronos en el entorno descentralizado. Para ello, el Dr. Danielsson propone un algoritmo as\u00edncrono descentralizado y procede a realizar la misma comparaci\u00f3n y traducciones disponibles en un trabajo anterior, s\u00f3lo que en un entorno descentralizado, descubriendo que son factibles pero implican un coste adicional.<\/span><\/p>\n

\u00abLa verificaci\u00f3n en tiempo de ejecuci\u00f3n es un punto intermedio entre la verificaci\u00f3n formal est\u00e1tica y el testing: disponer de una especificaci\u00f3n formal con la precisi\u00f3n y claridad que proporciona en combinaci\u00f3n con la ligereza de tener que analizar s\u00f3lo una traza, como en el testing\u00bb determina Luis Miguel. Esto hace que la VR sea adecuada para analizar grandes programas complejos que no suelen manejarse bien ni en verificaci\u00f3n est\u00e1tica ni en Testing.<\/span><\/p>\n

En resumen, a la hora de elegir un algoritmo para monitorizar un sistema descentralizado, hay que considerar no s\u00f3lo el formalismo de la especificaci\u00f3n, sino c\u00f3mo se recogen y procesan los datos<\/strong>. Cuando el procesamiento de datos se realiza peri\u00f3dicamente, el lenguaje s\u00edncrono y el algoritmo de supervisi\u00f3n funcionar\u00e1n mejor. En cambio, cuando los datos se obtienen espor\u00e1dicamente o en r\u00e1fagas, el lenguaje as\u00edncrono y el algoritmo evitar\u00e1n c\u00e1lculos innecesarios y superar\u00e1n a una soluci\u00f3n s\u00edncrona. <\/span><\/p>\n","protected":false},"excerpt":{"rendered":"

Determinar si un programa inform\u00e1tico es correcto o defectuoso, que se comporta como se espera, es de lo que se encarga la verificaci\u00f3n de software, la rama de investigaci\u00f3n a la que se dedica Luis Miguel Danielsson. Dado que el software se ha convertido en una herramienta importante para resolver una amplia gama de problemas humanos, es necesario gestionar todos los detalles sobre c\u00f3mo manejar los datos y el c\u00e1lculo en un algoritmo determinado. Pero construir software fiable es una tarea notoriamente dif\u00edcil. A\u00fan m\u00e1s, en el software concurrente o distribuido, la naturaleza intr\u00ednseca del sistema dificulta la programaci\u00f3n, al tener\u2026<\/p>\n","protected":false},"author":243,"featured_media":0,"comment_status":"open","ping_status":"open","sticky":false,"template":"","format":"standard","meta":{"ngg_post_thumbnail":0},"categories":[7197],"tags":[51836,51832,51837,36010,51803,51838,51839,51831,244,51835,51834],"blocksy_meta":{"styles_descriptor":{"styles":{"desktop":"","tablet":"","mobile":""},"google_fonts":[],"version":4}},"aioseo_notices":[],"_links":{"self":[{"href":"https:\/\/www.madrimasd.org\/blogs\/Tecnologiasdelainformacionparaelmundodelmanana\/wp-json\/wp\/v2\/posts\/239"}],"collection":[{"href":"https:\/\/www.madrimasd.org\/blogs\/Tecnologiasdelainformacionparaelmundodelmanana\/wp-json\/wp\/v2\/posts"}],"about":[{"href":"https:\/\/www.madrimasd.org\/blogs\/Tecnologiasdelainformacionparaelmundodelmanana\/wp-json\/wp\/v2\/types\/post"}],"author":[{"embeddable":true,"href":"https:\/\/www.madrimasd.org\/blogs\/Tecnologiasdelainformacionparaelmundodelmanana\/wp-json\/wp\/v2\/users\/243"}],"replies":[{"embeddable":true,"href":"https:\/\/www.madrimasd.org\/blogs\/Tecnologiasdelainformacionparaelmundodelmanana\/wp-json\/wp\/v2\/comments?post=239"}],"version-history":[{"count":6,"href":"https:\/\/www.madrimasd.org\/blogs\/Tecnologiasdelainformacionparaelmundodelmanana\/wp-json\/wp\/v2\/posts\/239\/revisions"}],"predecessor-version":[{"id":246,"href":"https:\/\/www.madrimasd.org\/blogs\/Tecnologiasdelainformacionparaelmundodelmanana\/wp-json\/wp\/v2\/posts\/239\/revisions\/246"}],"wp:attachment":[{"href":"https:\/\/www.madrimasd.org\/blogs\/Tecnologiasdelainformacionparaelmundodelmanana\/wp-json\/wp\/v2\/media?parent=239"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/www.madrimasd.org\/blogs\/Tecnologiasdelainformacionparaelmundodelmanana\/wp-json\/wp\/v2\/categories?post=239"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/www.madrimasd.org\/blogs\/Tecnologiasdelainformacionparaelmundodelmanana\/wp-json\/wp\/v2\/tags?post=239"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}