ABSTRACT. Runtime Verification (RV) is a semi-formal verification technique that involves augmenting a system with runtime monitors that continuously check for deviations from the system’s expected behavior. This ensures that the current run of the system is error-free. State-of-the-art RV frameworks synthesize runtime monitors from formal specifications of system properties. As a result, these monitors are tailored for single-property verification, necessitating resynthesis for different properties. In this work, we propose a RV framework that includes a domain-specific architecture and its associated compiler that takes as input properties specified in Linear Temporal Logic (LTL) and flags deviations from the expected behavior of a system. Our proposed framework requires only recompilation (instead of resynthesis) as properties change, thereby enabling an ASIC implementation of the runtime monitors. This allows for high-speed, low-overhead as well as flexible monitoring of a wide range of system properties. This level of flexibility is essential for ensuring the reliability and robustness of complex systems. We evaluate our framework using 53 LTL properties from several prior works.

ABSTRACT. We propose an efficient offline monitoring algorithm for properties written in DMTL (Dynamic Metric Temporal Logic), a temporal formalism that combines MTL (Metric Temporal Logic) with regular expressions. Our algorithm is polynomial in the size of the temporal specification and linear in the length of the input trace. In particular, our monitoring algorithm needs time $O(m^3 \cdot n)$, where $m$ is the size of the DMTL formula and $n$ in the length of the input trace.

ABSTRACT. First-order monitors analyze data-carrying event streams. When event streams are generated by distributed systems, it may be difficult to ensure that events arrive at the monitor in the right order. We develop a new monitoring algorithm for metric first-order temporal logic that can process out-of-order events. We implement our algorithm in the stream processing framework Timely Dataflow, which transparently supports the parallelized execution of our monitor. We demonstrate our monitor's good performance and scalability on synthetic and real-world benchmarks.

ABSTRACT. Stream Runtime Verification (SRV) is gaining traction for monitoring systems with data streams, but it struggles with specifying state-based systems and control flow. While automata models like state charts excel at representing states, functional languages offer solutions like monads (e.g., in Haskell) to elegantly handle state and data streams together. Other approaches exist in Lustre/Esterel or Rust. However, for SRV frameworks like TeSSLa, no such approach exists so far. This paper extends TeSSLa’s syntax by building on a monadic type to simplify for improved control flow specifications.

ABSTRACT. Nfer is a Runtime Verification language for the analysis of event traces that applies rules to create hierarchies of time intervals. This work examines the complexity of the evaluation and satisfiability problems for the data-free fragment of nfer. The evaluation problem asks whether a given interval is generated by applying rules to a known input, while the satisfiability problem asks if an input exists that will generate a given interval.

By excluding data from the language, we achieve PTime complexity for the evaluation problem and satisfiability when only considering inclusive rules, and decidability for the satisfiability problem for cycle-free specifications. Finally, we show that for the full data-free language, satisfiability is undecidable.

ABSTRACT. Runtime monitoring facilitates human oversight of safety-critical systems by collecting and aggregating data from sensors and other system components and by issuing alerts whenever the safety specification is violated. It is critical that the collected data is presented in a way that helps the user to quickly assess the situation. Most monitoring tools have only limited support for data visualization. We present RTLolaMo³Vis, an online runtime monitoring framework that is mobile, modular, and supports the graphical visualization of the monitoring data in real time. RTLolaMo³Vis is highly configurable, from data collection to the final visualization, which makes it applicable to a wide spectrum of applications. The design of RTLolaMo³Vis follows the monitoring-based visualization approach, which minimizes the additional code for visualization by preprocessing the data in the monitor. We demonstrate the modularity and efficiency of RTLolaMo³Vis on simulated drone flights and real-world communication data. On standard mobile phones and tablet computers, RTLolaMo³Vis processes the monitoring output at a frequency of 100Hz without any data loss.