Runtime Verification of Interactions Using Automata

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.