Towards a stream-basedmonitoring language for asynchronous systems

Abstract

In this thesis, we study the problem of monitoring rich properties of real-time event streams, and
propose a solution based on Stream Runtime Verification.
Stream Runtime Verification (SRV) is a specification formalism where observations are described
as streams of data computed from input streams of data, which allows us to cleanly separate the
temporal dependencies between events and the concrete operations that are performed during
the monitoring. However, Stream Runtime Verification languages typically assume that all streams
share a global synchronous clock and input events arrive in a synchronousmanner.
In this thesis we generalize the time assumption to cover streams whose events are stamped from
a real-time domain, but keep the essential explicit time dependencies present in previous synchronous
SRV languages. The resulting formalism, which we call Striver, shares with synchronous
SRV the simplicity of the separation between the timing reasoning and the data domain.
We demonstrate how Striver can serve as a general language to express other real-timemonitoring
languages by showing translations from other logics and specification languages for (piece-wise
constant) signals and timed event streams. Finally, we report an empirical evaluation of an implementation
of Striver and present a real case of a system for the monitorization of cloud applications
where this implementation has been sucessfully used.---ABSTRACT---En esta tesis, estudiamos el problema de monitorizar propiedades sobre flujos de eventos en
tiempo real, y proponemos una solución basada en Stream Runtime Verification.
Stream Runtime Verification (SRV) es un formalismo de especificación en donde las observaciones
se describen como flujos de datos computados a partir de flujos de datos de entrada, lo que permite
establecer una separación limpia entre las dependencias temporales de los eventos y las operaciones
concretas que se llevan a cabo durante la monitorización. Sin embargo, los lenguajes de
Stream Runtime Verification típicamente suponen que todos los flujos de entrada comparten un
reloj global sincronizado, y que los eventos se reciben de manera síncrona.
En esta tesis generalizamos las suposiciones sobre el tiempo para considerar flujos de eventos
en donde cada evento viene acompañado por el instante de tiempo real en el cual se produjo,
manteniendo explícitas las dependencias temporales esenciales características de lenguajes de
SRV preexistentes. El formalismo resultante, al cual llamamos Striver, comparte con los lenguajes
de SRV síncronos la simplicidad de la distinción entre los razonamientos temporales y el dominio
de datos
Mostramos que Striver puede utilizarse como un lenguaje general para expresar otros lenguajes de
monitorización de tiempo real, presentando traducciones de otras lógicas y lenguajes de especificación
para señales (definidas por partes) y flujos de eventos temporales. Finalmente, reportamos
una evaluación empírica de una implementación de Striver y presentamos un caso real de un sistema
para la monitorización de aplicaciones en la nube en donde dicha implementación ha sido
utilizada con éxito.