Decentralised stream runtime verification

Abstract

Se estudia el problema de monitorización descentralizada de especificaciones de
stream runtime verification (SRV). La monitorización descentralizada consiste en
organizar una actividad de monitorización para que sea realizada por componentes
distribuidos que se comunican utilizando una red síncrona, un escenario común en
algunos sistemas ciber-físicos(CPS) como en automoción. Alternativas previas de
monitorización descentralizada se restringían a LTL y lógicas similares cuyos monitores computan veredictos booleanos. Se presenta un algoritmo que solventa el
problema de la monitorización descentralizada para el caso más general de stream
runtime verification. Adicionalmente, el algoritmo gestiona topologías de red mientras que trabajos previos asumían una red en la que todos los nodos se podían
comunicar directamente. Este algoritmo es capaz de obtener veredictos de forma
eficiente al hacer uso de estrategias de evaluación parcial, simplificadores de expresiones y estrategias avanzadas de comunicación. Finalmente, presentamos los
resultados de una evaluación empírica de una implementación y comparamos la expresividad y la eficiencia con la herramienta de monitorización descentralizada de
vanguardia Themis.---ABSTRACT---We study the problem of decentralized monitoring of stream runtime verification
(SRV) specifications. Decentralized monitoring consists of organizing a monitoring activity to be performed by distributed components that communicated using
a synchronous network, a setting common in some cyber-physical systems like automotive CPSs. Previous approaches to decentralized monitoring were restricted
to LTL and similar logics whose monitors compute Boolean verdicts. We present
here an algorithm that solves the decentralized monitoring problem for the more
general setting of stream runtime verifiation. Additionally, our algorithm handles
network topologies were previous work assumed a network in which all nodes can
communicate directly.
Our algorithm is able to reach verdicts eficiently by exploiting partial evaluation
strategies, expression simplifiers and advanced communication strategies. Finally,
we present the results of an empirical evaluation of an implementation and compare
the expressive power and eficiency against state-of-the-art decentralized monitoring
tools like Themis.