Synchronous and asynchronous stream runtime verification

Abstract

We revisit the topic of Stream Runtime Verification (SRV) both for synchronous and asynchronous systems. Stream Runtime Verification is a formalism to express monitors using streams, which results in a simple and expressive specification language. This language is not restricted to describe correctness/failure assertions, but can also collect richer information (including statistical measures) for system profiling and coverage analysis. The monitors generated in SRV are useful for testing, under actual deployment, and to analyze logs. The steps in many algorithms proposed in runtime verification are based on temporal logics and similar formalisms, which generate Boolean verdicts. The key idea of Stream Runtime Verification is that these algorithms can be generalized to compute richer information if a different data domain is used. Hence, the keystone of SRV is to separate the temporal dependencies in the monitoring algorithm from the concrete operations performed at each step. Early SRV languages, pioneered by Lola, considered that the observations arrive in a periodic fashion, so the model of time is synchronous sequences like in linear temporal logic. Newer systems, like TeSSLa, RTLola and Striver, have adapted SRV to real-time event streams, where input and output streams can contain events of data at any point. We will revisit the notions of SRV for synchronous and asynchronous systems. Then, we will justify that synchronous SRV can be modeled by real-time SRV and finally present conditions under which synchronous SRV can simulate real-time SRV.