Tesis:
Theory and Practice of Stream Runtime Verification for Sequences and Real-Time Event Based Systems
- Autor: GOROSTIAGA, Felipe
- Título: Theory and Practice of Stream Runtime Verification for Sequences and Real-Time Event Based Systems
- Fecha: 2022
- Materia: Sin materia definida
- Escuela: E.T.S DE INGENIEROS INFORMÁTICOS
- Departamentos: LENGUAJES Y SISTEMAS INFORMATICOS E INGENIERIA DE SOFTWARE
- Acceso electrónico: https://oa.upm.es/70504/
- Director/a 1º: SÁNCHEZ SÁNCHEZ, César
- Resumen: Software verification is the employment of formal methods to ensure the absence of errors in a program, but whose application is susceptible to become impractical for large and complex systems. Runtime verification is a technique for software assurance that consists of generating, from a formal specification, a monitor that analyses an execution trace online or offline and detects violations of the specification, which makes this technique more scalable than static verification. Stream Runtime Verification (SRV) defines specifications declaratively in terms of input and output streams of events that carry data of rich types. One of the main concerns of SRV languages is the clean separation of temporal and data aspects of a specification. Most early SRV formalisms, such as the pioneer language Lola, are based on synchronous streams, where data observed at the same index in different streams are considered to have occurred simultaneously. The first contribution of this Thesis is Striver, a novel SRV language inspired in Lola that handles non-synchronized timestamped event streams. We compare Striver with similar pre-existing formalisms and also exhibit the conditions under which Striver is equally expressive to Lola. We show an algorithm to translate to one another and we study the performance of the translated specifications both theoretically and empirically. The second contribution of this Thesis is the implementation of Lola and Striver using “lift-deep embedding”, a novel technique lets us effectively fulfill the promise of a straightforward addition and usage of arbitrary data types in the languages, which we demonstrate empirically employing the tools over a wide range of application domains. We also present new extensions to both languages that amplify their expressive power and give rise to a new class of specifications. ----------RESUMEN---------- 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. 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. 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. Comparamos Striver con formalismos preexistentes similares y mostramos las condiciones bajo las cuales Striver y Lola son igualmente expresivos. También presentamos un algoritmo para traducir especificaciones entre uno y otro lenguaje y estudiamos 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 nos permite cumplir con la promesa de poder añadir y utilizar tipos de datos arbitrarios en los lenguajes de manera sencilla, capacidad que demostramos empíricamente usando las herramientas implementadas en diversos dominios de aplicación. También presentamos nuevas extensiones a los lenguajes que amplifican sus capacidades y dan origen a una nueva clase de especificaciones.