Decentralized and Distributed Stream Runtime Verification
Authors:   , Danielsson Villegas Luis Miguel 
Published: May 2024

There are multiple ways to ensure software quality. In Formal Software Verification we use a formal language to express the desired behavior of a program. Runtime Verification (RV) is the area that studies monitoring as the process of checking whether an execution trace conforms to a given specification expressed in a formal language. In Stream Runtime Verification (SRV) we use a specification expressed using a stream based language to synthesize a monitor. Then the monitor consumes the execution trace of a program, collects information from the trace and outputs verdicts on whether the trace meets the specification or quantitative results.

Most RV works consider only a centralized solution where a single central monitor computes the whole specification. In contrast, in decentralized monitoring the task of computing the specification is shared among the nodes of a network. The first contribution of this Thesis is a decentralized monitoring algorithm based on streams for synchronous networks and then extensions for more realistic network models, concretely timed asynchronous networks and finally a fault-tolerant enhancement that allows the monitors to be resilient against message duplication and message loss. All of the publications in this first contribution provide formal proofs of correctness and the study of the resource usage of the algorithms. We show the necessary conditions that allow the monitors to use only bounded resources. This is specially important in the area of cyber-physical systems where devices often have limited resources available. These techniques are applicable in the areas of smart-buildings and ambient living as shown by our empirical evaluations where we use datasets from those domains, but are not restricted to them.

In the second part of this Thesis we dive into the different conceptions of time for monitoring (synchronous/event-based vs asynchronous/time-based) and if there could be a way of trans- forming a specification from one to the other. The second contribution of this Thesis contains a translation between synchronous and asynchronous SRV languages in the decentralized setting based on existing translations in the centralized setting. In order to do this, we provide a decentralized algorithm for an asynchronous SRV language. We also studied with special emphasis in the associated extra communication needed to provide the appropriate transformations to the input trace so that these different solutions can actually monitor.

RESUMEN

Existen diferentes maneras de asegurar la calidad del Software. En Verificación Formal de Software se utiliza un lenguaje formal para expresar el comportamiento deseado de un programa. La Verificación en Tiempo de Ejecución (Runtime Verification RV) es el área que estudia cómo monitorizar para comprobar si una traza de ejecución satisface una determinada especificación expresada en un lenguaje formal. En Verificación en Tiempo de Ejecución basado en Streams (Stream Runtime Verification SRV) se utiliza un lenguaje basado en streams para sintetizar un monitor a partir de una especificación. Durante la ejecución el monitor va leyendo la traza de un programa, recolectando información y emite un veredicto acerca de si la traza satisface o no la especificación o bien un resultado cuantitativo obtenido a partir de la información almacenada.

Es habitual en RV considerar una solución centralizada en la que un único monitor central se encarga de computar la totalidad de la especificación. Sin embargo, en monitorización descentralizada la tarea de computar la especificación se reparte entre los nodos conectados por red. La primera contribución de esta Tesis es un algoritmo descentralizado basado en streams para redes síncronas y posteriormente extensiones para modelos cada vez más cercanos a redes realistas. En concreto, para redes asíncronas que permiten tener un reloj global de ciertas características y por último una mejora que incorpora tolerancia a fallos que permite a los monitores ser resistentes a la duplicación y pérdida de mensajes. Todas las publicaciones relacionadas con esta primera contribución aportan pruebas formales de corrección, así como un estudio pormenorizado del consumo de recursos de los algoritmos. Asimismo, se muestra las condiciones necesarias para que los monitores únicamente necesiten recursos limitados. Esto es especialmente importante en el área de sistemas ciber-físicos donde habitualmente los dispositivos disponen de recursos limitados. Estas técnicas son aplicables en las áreas de smart-buildings y de ambient living como se muestra en las diferentes evaluaciones empíricas en las que se han utilizado datasets de dichas áreas, pero su ámbito de aplicación no está restringido a estas.

En la segunda parte de esta Tesis ahondamos en las diferentes nociones de tiempo para la monitorización: ya sea síncrono-basado en eventos o asíncrono-basado en tiempo. También estudiamos si existe una forma de transformar una especificación de un paradigma al otro.

La segunda contribución de esta Tesis contiene una traducción entre lenguajes síncrono y asíncrono de SRV para el entorno descentralizado basándose en traducciones que ya existen para el entorno centralizado. Ahora bien, para ser capaces de hacer esto, proponemos un algoritmo descentralizado para un lenguaje asíncrono de SRV. Estudiamos la traducción descentralizada con especial énfasis en la comunicación asociada que se requiere para realizar las transformaciones adecuadas a la traza de entrada para conseguir que estas soluciones puedan realmente monitorizar la especificación.