Runtime Verification of Interactions Using Automata

TL;DR

This paper introduces automata-based methods for runtime verification of distributed systems' interactions, effectively checking multitraces against specifications without relying on synchronized clocks.

Contribution

It proposes two automata-theoretic procedures for verifying multitraces against interaction models, including a reusable, more informative approach.

Findings

Two verification procedures implemented and compared

Reusability reduces preprocessing for multiple trace checks

Automata-based approach handles unsynchronized distributed traces

Abstract

Runtime verification consists in observing and collecting the execution traces of a system and checking them against a specification, with the objective of raising an error when a trace does not satisfy the specification. We consider distributed systems consisting of subsystems which communicate by message-passing. Local execution traces consisting of send and receive events are collected on each subsystem. We do not assume that the subsystems have a shared global clock, which would allow a reordering of the local traces. Instead, we manipulate multitraces, which are collections of local traces. We use interaction models as specifications: they describe communication scenarios between multiple components, and thus specify a desired global behaviour. We propose two procedures to decide whether a multitrace satisfies an interaction, based on automata-theoretic techniques. The first procedure is straightforward, while the second provides more information on the type of error and integrates the idea of reusability: because many multitraces are compared against one interaction, some preprocessing can be done once at the beginning. We implement both procedures and compare them.