El investigador Luis Miguel Danielsson, asesorado por el profesor César Sánchez, defendió el pasado 16 de abril, en la Escuela Técnica Superior de Ingeniería Informática de la Universidad Politécnica de Madrid, su tesis, titulada: “Verificación descentralizada y distribuida de flujos en tiempo de ejecución”, rodeado de compañeros y familiares.
Contexto
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ómo manejar los datos y el cálculo en un algoritmo determinado. Pero construir software fiable es una tarea notoriamente difícil. Aún más, en el software concurrente o distribuido, la naturaleza intrínseca del sistema dificulta la programación, al tener que gestionar dos o más cómputos al mismo tiempo y comprender y gestionar sus interconexiones, como la comunicación o la sincronización.
En este escenario resulta fundamental disponer de herramientas para determinar mecánicamente si un programa es correcto o defectuoso. Este es el ámbito de la verificación de software, que se ocupa de garantizar que un programa se comporta como se espera, es decir, cuál es el resultado deseado y cómo queremos que el programa lo calcule.
En este sentido, Luis Miguel Danielsson afirma que: “Verificar sistemas reactivos es aún más difícil cuando el entorno no es de naturaleza computacional, como los sistemas human-in-the-loop, que dependen del entorno físico (como los drones) y los distribuidos (como los edificios inteligentes). En estos sistemas es muy difícil modelar con precisión el entorno. Por esta razón, las técnicas de verificación estática son a menudo limitadas o incluso prácticamente inviables para este tipo de sistemas en la práctica”.
La tesis
El propósito de esta tesis es llevar la Verificación en Tiempo de Ejecución a los Sistemas Descentralizados y Distribuidos -que son, por su naturaleza concurrente, intrínsecamente complejos-, con el fin de mejorar la privacidad, la eficiencia o añadir tolerancia a fallos en la monitorización distribuida para presentar claras ventajas sobre las soluciones centralizadas.
Los objetivos generales de esta tesis son tres: definir el problema de la monitorización de sistemas descentralizados y distribuidos con veredictos ricos; proponer soluciones algorítmicas a la monitorización descentralizada y probar formalmente su corrección; e implementar dichas soluciones y realizar evaluaciones empíricas.
Luis Miguel propone el uso de algoritmos correctos descentralizados y distribuidos basados en Stream Runtime Verification para monitorizar eficaz y eficientemente sistemas descentralizados y distribuidos ayudando en la tarea de mejorar su calidad.
La solución propuesta por el Dr. Danielsson es un enfoque de método formal ligero que tiene su origen en la verificación formal estática. La verificación en tiempo de ejecución intenta aliviar los problemas al evitar modelar el entorno, y los problemas de escalabilidad al restringir el análisis a una sola traza y no a todas las trazas del sistema.
La primera contribución de la Tesis es un algoritmo de monitorización descentralizado basado en streams para redes síncronas. A continuación, Luis Miguel presenta extensiones para modelos de red más realistas, concretamente redes asíncronas temporizadas. Por último, introduce una mejora tolerante a fallos que permite a los monitores ser resistentes frente a la duplicación y pérdida de mensajes.
La segunda aportación de la Tesis es una comparación y traducción entre lenguajes síncronos y asíncronos en el entorno descentralizado. Para ello, el Dr. Danielsson propone un algoritmo asíncrono descentralizado y procede a realizar la misma comparación y traducciones disponibles en un trabajo anterior, sólo que en un entorno descentralizado, descubriendo que son factibles pero implican un coste adicional.
“La verificación en tiempo de ejecución es un punto intermedio entre la verificación formal estática y el testing: disponer de una especificación formal con la precisión y claridad que proporciona en combinación con la ligereza de tener que analizar sólo una traza, como en el testing” determina Luis Miguel. Esto hace que la VR sea adecuada para analizar grandes programas complejos que no suelen manejarse bien ni en verificación estática ni en Testing.
En resumen, a la hora de elegir un algoritmo para monitorizar un sistema descentralizado, hay que considerar no sólo el formalismo de la especificación, sino cómo se recogen y procesan los datos. Cuando el procesamiento de datos se realiza periódicamente, el lenguaje síncrono y el algoritmo de supervisión funcionarán mejor. En cambio, cuando los datos se obtienen esporádicamente o en ráfagas, el lenguaje asíncrono y el algoritmo evitarán cálculos innecesarios y superarán a una solución síncrona.
