Felipe Gorostiaga, estudiante de doctorado del Instituto IMDEA Software ha defendido de manera satisfactoria su tesis doctoral esta mañana en la Escuela Técnica Superior de Ingeniería Informática (ETSIINF) de la UPM, en el Campus Montegancedo. Algunos de sus compañeros estuvieron presentes para escucharle y mostrar apoyo.
Su tesis, dirigida por César Sánchez, lleva como título: “Theory and Practice of Stream Runtime Verification for Sequences and Real-Time Event Based Systems”.
Felipe ha comenzado la defensa explicando que la utilización de métodos formales para verificación estática de software permite garantizar la ausencia de errores en un programa, pero su aplicación puede volverse poco práctica para sistemas grandes y complejos. En cambio, la verificación en tiempo de ejecución consiste en generar, dada una especificación formal, un monitor que analice una traza de ejecución del programa de manera online u offline y detecte violaciones sobre la especificación, lo que la convierte en una técnica más escalable que la verificación estática.
En Stream Runtime Verification (SRV) las especificaciones se definen declarativamente en términos de streams de eventos que contienen datos de tipos sofisticados. Uno de los pilares fundamentales de SRV es la clara separación entre aspectos temporales y de datos en una especificación. En este sentido, Gorostiaga comentó que la mayoría de los formalismos de SRV, entre ellos, el lenguaje pionero Lola, se basan en streams síncronos, en donde se considera que los datos observados en el mismo índice en dos streams diferentes ocurrieron en simultáneo.
La primera contribución de esta Tesis es Striver, un novedoso lenguaje de SRV inspirado en Lola que manipula streams de eventos que llevan un sello de tiempo. Ha comparado Striver con formalismos preexistentes similares y muestra las condiciones bajo las cuales Striver y Lola son igualmente expresivos.
En su trabajo, presenta un algoritmo para traducir especificaciones entre uno y otro lenguaje y estudia el desempeño de las especificaciones traducidas, tanto teórica como empíricamente.
La segunda contribución de esta Tesis es la implementación de Lola y Striver utilizando la técnica de “lift-deep embedding”, que permite cumplir con la promesa de poder añadir y utilizar tipos de datos arbitrarios en los lenguajes de manera sencilla, capaz que demostrar empíricamente usando las herramientas implementadas en diversos dominios de aplicación.
Por último, muestra cómo en la Tesis se presentan nuevas extensiones a los lenguajes que amplifican sus capacidades y dan origen a una nueva clase de especificaciones.
