HStriver: A Very Functional Extensible Tool for the Runtime Verification of Real-Time Event Streams

Abstract

We present HStriver, an extensible stream runtime verification tool for event streams. The tool consists of a runtime verification engine for (1) real-time events streams where individual observations and verdicts can occur at arbitrary times, and (2) rich data in the observations and verdicts. This rich setting allows, for example, encoding as HStriver specifications quantitative semantics of logics like STL, including different notions of robustness. The keystone of stream runtime verification (SRV) is the clean separation between temporal dependencies and data computations. To encode the data values and computations involved in the monitoring process we borrow (almost) arbitrary data-types from Haskell. These types are transparently lifted to the specification language and incorporated in the engine, so they can be used as the types of the inputs (observations), outputs (verdicts), and intermediate streams. The resulting extensible language is then embedded, alongside the temporal evaluation engine (which is agnostic to the types) into Haskell as an embedded Domain Specific Langauge (eDSL). Morever, the availability of functional features in the specification language enables the direct implementation of desirable features in HStriver like parametrization (using functions that return stream specifications), etc. The resulting tool is a flexible and extensible stream runtime verification engine for real-time streams. We illustrate the use of the tool on many sophisticated real-time specifications, including realistic signal temporal logic (STL) properties of existing designs.