Runtime Verification Tools
Daut
Daut is an internal shallow DSL, effectively a library, in the Scala programming language for programming monitors. A specific monitor is defined as a subclass of a library Monitor class. Given an object a monitor, one can submit events to it. Events can be any Scala data object respecting the parametric event type of the monitor. The body of the monitor is written in a combination of rule-based programming and state machines, with the additional feature that event sequences can be specified without having to name intermediate states. The DSL relies heavily on the use of Scala's elegant pattern matching to match against events. The internals of Daut are fundamentally a rule-based paradigm, where the state of a monitor at any time is a set of active facts, where a fact is an object parameterized with data. However, a fact has transitions leading to new facts. For each event submitted to a monitor, the relevant active states are applied to the event, causing facts to be removed and/or added. Due to the existence of transitions in facts, they can also be perceived as states in a state machine, but where states carry data in contrast to classical state machines, leading to a more powerful paradigm. Monitors can be chained together such that one monitor can deliver events to other monitors. Since Daut is an internal DSL, rules/state machines can be combined with code, allowing to generate data in addition to just Boolean verdicts.
JunitRV
jUnitRV is a runtime verification framework that integrates seamlessly with the JUnit testing infrastructure for Java, enabling property-based monitoring during unit test execution. It allows developers to specify temporal properties in a high-level specification language, especially LTL, and automatically generates monitors that check these properties at runtime. jUnitRV is particularly useful for augmenting traditional testing with formal temporal specification checking. In other words, it offers checking temporal assertions rather than only assertions alone. By embedding monitors into test cases, it supports identifying bugs related to sequences of method calls, object states, or temporal constraints. Its integration with JUnit makes it accessible in standard Java testing workflows.
PyContract
PyDejaVu
R2U2
TeSSLa
TeSSLa (Temporal Stream-based Specification Language) is a runtime verification framework designed for specifying and monitoring properties of real-time and cyber-physical systems. It operates on time-stamped event streams, allowing users to define formal specifications that capture both logical and temporal aspects of system behavior. TeSSLa excels in handling sparse and asynchronous streams, and it provides native support for timing constructs such as delays, timestamps, and temporal relations. Its language includes features like stream merging, recursion, and time-based operators. TeSSLa specifications are compiled into efficient monitors for deployment in resource-constrained environments. While hLola and hStriver embed their specification languages in Haskell, TeSSLa uses its own syntax and semantics. Notably, hStriver introduces real-time as a first-class concept, similar in spirit to TeSSLa, but within a functional programming context. In contrast, hLola treats time as a data value, offering more flexibility but less direct support for real-time constraints.
hLola
HLola is a Stream Runtime Verification (SRV) tool that builds on LOLA, the pioneering approach in SRV, and extends it by incorporating features from the functional programming language Haskell. This design cleanly separates data computation from temporal aspects, enabling a flexible and extensible language for runtime monitoring. Stream Runtime Verification views runtime verification as stream transformation, where streams of events generated during system execution are processed into output streams to evaluate compliance with specified properties. HLola offers a domain-specific language (DSL) embedded in Haskell, allowing for seamless integration with host language constructs. As a result, it benefits from Haskell's expressive type system for event data and verdicts, functional abstraction for parameterization, access to rich libraries, support for higher-order specification transformations, and familiar syntactic elements like 'let'/'where' clauses, 'do' notation, and type annotations. It is also backed by a robust compiler targeting multiple platforms.
hStriver
hStriver is a Stream Runtime Verification (SRV) tool that builds on LOLA, the pioneering approach in SRV, and extends it by incorporating features from the functional programming language Haskell. This design cleanly separates data computation from temporal aspects, enabling a flexible and extensible language for runtime monitoring. hStriver offers a domain-specific language (DSL) embedded in Haskell, allowing for seamless integration with host language constructs. As a result, it benefits from Haskell's expressive type system for event data and verdicts, functional abstraction for parameterization, access to rich libraries, support for higher-order specification transformations, and familiar syntactic elements like let/where clauses, do notation, and type annotations. It is also backed by a robust compiler targeting multiple platforms. The main difference between hLola and hStriver is that hStriver supports real-time as a first-class citizen, whereas in hLola, time may only appear as a data value.
nfer
The nfer tool implements the eponymous language in C, with programmer interfaces in C, Python, and R. Visualization is provided via the Python interface. Nfer rules are written in an external DSL. The nfer language is somewhat unique in that it is a rule-based language for describing the state relationships of events with data. Nfer operates on labeled, temporal intervals with data where an event is considered an interval with zero duration. Rules describe the temporal and data relationships between existing intervals and produce new intervals when their conditions are met. Operations on numeric data are arbitrary, but the string operations are limited to equality matching. Nfer evaluation is undecidable in the general case, but there are known, useful fragments with evaluation complexity in PTime. The tool supports constructing C-language monitors with static memory allocation designed for embedded systems. The Python and R implementations use the C interpreter as a back-end.
rtLola
RTLola (Real-Time Lola) is an extension of the original LOLA stream-based runtime verification framework, designed specifically to support real-time monitoring. Like LOLA, RTLola uses stream-based specifications to define monitors over sequences of events, but it enhances the model by introducing explicit real-time semantics. RTLola allows users to define input, output, and parameterized streams, with powerful features such as sliding windows, aggregation over time intervals, and real-time constraints. These features enable the specification of complex temporal properties, including frequency-based or time-bounded conditions, which are common in embedded and cyber-physical systems. Compared to tools like hLola and TeSSLa, RTLola provides a clean separation between logical time and real time, allowing precise control over how temporal conditions are evaluated. While hLola focuses on leveraging Haskell's functional features and treats time as a data value, and TeSSLa integrates time deeply into its stream model with support for sparse streams and delays, RTLola strikes a balance by supporting high-level real-time constructs in a dedicated DSL with formal semantics and analyzable resource usage.