Towards a stream-basedmonitoring language for asynchronous systems

Gorostiaga, Felipe (2018). Towards a stream-basedmonitoring language for asynchronous systems. Thesis (Master thesis), E.T.S. de Ingenieros Informáticos (UPM).

Description

Title: Towards a stream-basedmonitoring language for asynchronous systems
Author/s:
  • Gorostiaga, Felipe
Contributor/s:
  • Fredlund, Lars-Åke
  • Sánchez, César
Item Type: Thesis (Master thesis)
Masters title: Software y Sistemas
Date: July 2018
Subjects:
Faculty: E.T.S. de Ingenieros Informáticos (UPM)
Department: Otro
Creative Commons Licenses: Recognition - No derivative works - Non commercial

Full text

[img]
Preview
PDF - Requires a PDF viewer, such as GSview, Xpdf or Adobe Acrobat Reader
Download (425kB) | Preview

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.

More information

Item ID: 51742
DC Identifier: http://oa.upm.es/51742/
OAI Identifier: oai:oa.upm.es:51742
Deposited by: Biblioteca Facultad de Informatica
Deposited on: 26 Jul 2018 07:17
Last Modified: 26 Jul 2018 07:17
  • Logo InvestigaM (UPM)
  • Logo GEOUP4
  • Logo Open Access
  • Open Access
  • Logo Sherpa/Romeo
    Check whether the anglo-saxon journal in which you have published an article allows you to also publish it under open access.
  • Logo Dulcinea
    Check whether the spanish journal in which you have published an article allows you to also publish it under open access.
  • Logo de Recolecta
  • Logo del Observatorio I+D+i UPM
  • Logo de OpenCourseWare UPM