Unifying the Time-Event Spectrum for Stream Runtime Verification

Abstract

We study the spectra of time-event and of synchronousasynchronous models of computation for runtime verification, in particular in the context of stream runtime verification (SRV). Most runtime verification formalisms do not involve a notion of time, either by having inputs at all instants (like LTL or Lola) or by reacting to external events in an event-driven fashion (like MOP). Other formalisms consider notions of real-time, ranging from the collection and periodic processing of events to complex computations of the times at which events exist or are produced (like TeSSLa or Striver). Also, some monitoring languages assume that all inputs and outputs change values at once (synchronous), while others allow changes independently (asynchronous). In this paper we present a unifying view of the event-time and synchronousasynchronous dimensions in the general setting of SRV. We first prove that the Striver event-based asynchronous language can execute synchronous untimed specifications (written in Lola), and empirically show that this simulation is efficient. We then prove that Lola can simulate real-time Striver monitors under the assumption of the existence of temporal backbones and study two cases: (1) Purely event-driven or when reactions can be precomputed (for example periodic intervals), which results in an efficient simulation but restricted to a fragment. (2) When the time has a minimum quantum: which allows full expressivity but the performance is greatly affected, particularly for sparse input streams.