Dataflow languages have, as well as functional languages, immutable semantics, which is often implemented by copying values. A common compiler optimization known from functional languages involves analyzing which data structures can be modified in-place instead of copying them. This paper presents a novel algorithm to this so called Aggregate Update Problem for multi-clocked dataflow languages, i.e. those that allow streams to have events at disjoint timestamps, like e.g. Lucid, Lustre and Signal. Unrestricted multi-clocked languages require a static triggering analysis on how events and hence data values are read, written and replicated. We use TeSSLa as a generic stream transformation language with a small set of operators to develop our ideas. We implemented the solution in a TeSSLa compiler targeting the Java VM via Scala code generation which combines persistent data structures and mutable data structures for those data values which allow in-place editing. Our empirical evaluation shows considerable speedup for use cases where queues, maps or sets are dominant data structures.

Abstract Runtime verification deals with checking correctness properties on the runs of a system under scrutiny. To achieve this, it addresses a variety of sub-problems related to monitoring of systems: These range from the appropriate design of a specification language over efficient monitor generation as hardware and software monitors to solutions for instrumenting the monitored system, preferably in a non-intrusive way. Further aspects play a role for the usability of a runtime verification toolchain, e.g. availability, sufficient documentation and the existence of a developer community. In this paper we present the TeSSLa ecosystem, a runtime verification framework built around the stream runtime verification language TeSSLa: It provides a rich toolchain of mostly freely available compilers for monitor generation on different hardware and software backends, as well as instrumentation mechanisms for various runtime verification requirements. Additionally, we highlight how the online resources and supporting tools of the community-driven project enable the productive usage of stream runtime verification.

Abstract We study the problem of online runtime verification of real-time event streams. Our monitors can observe concurrent systems with a shared clock, but where each component reports observations as signals that arrive to the monitor at different speeds and with different and varying latencies. We start from specifications in a fragment of the TeSSLa specification language, where streams (including inputs and final verdicts) are not restricted to be Booleans but can be data from richer domains, including integers and reals with arithmetic operations and aggregations. Specifications can be used both for checking logical properties and for computing statistics and general numeric temporal metrics (and properties on these richer metrics). We present an online evaluation algorithm for the specification language and a concurrent implementation of the evaluation algorithm. The algorithm can tolerate and exploit the asynchronous arrival of events without synchronizing the inputs. Then, we introduce a theory of asynchronous transducers and show a formal proof of the correctness such that every possible run of the monitor implements the semantics. Finally, we report an empirical evaluation of a highly concurrent Erlang implementation of the monitoring algorithm.

Runtime Verification (RV) studies how to analyze execution traces of a system under observation. Stream Runtime Verification (SRV) applies stream transformations to obtain information from observed traces. Incomplete traces with information missing in gaps pose a common challenge when applying RV and SRV techniques to real-world systems as RV approaches typically require the complete trace without missing parts. This paper presents a solution to perform SRV on incomplete traces based on abstraction. We use TeSSLa as specification language for non-synchronized timed event streams and define abstract event streams representing the set of all possible traces that could have occurred during gaps in the input trace. We show how to translate a TeSSLa specification to its abstract counterpart that can propagate gaps through the transformation of the input streams and thus generate sound outputs even if the input streams contain gaps and events with imprecise values. The solution has been implemented as a set of macros for the original TeSSLa and an empirical evaluation shows the feasibility of the approach.

We present a novel, non-intrusive approach to MC/DC coverage measurement using modern processor-based tracing facilities. Our approach does not require recompilation or instrumentation of the software under test. Instead, we use the Intel Processor Trace (Intel PT) facility present on modern Intel CPUs. Our tooling consists of the following parts: a frontend that detects so-called decisions (Boolean expressions) that are used in conditionals in C source code, a mapping from conditional jumps in the object code back to those decisions, and an analysis that computes satisfaction of the MC/DC coverage relation on those decisions from an execution trace. This analysis takes as input a stream of instruction addresses decoded from Intel PT trace data, which was recorded while running the software under test. We describe our architecture and discuss limitations and future work.

In this tutorial, we present a comprehensive approach to non-intrusive monitoring of multi-core processors. Modern multi-core processors come with trace-ports that provide a highly compressed trace of the instructions executed by the processor. We describe how these compressed traces can be used to reconstruct the actual control flow trace executed by the program running on the processor and to carry out analyses on the control flow trace in real time using FPGAs. We further give an introduction to the temporal stream-based specification language TeSSLa and show how it can be used to specify typical constraints of a cyber-physical system from the railway domain. Finally, we describe how light-weight, hardware-supported instrumentation can be used to enrich the control-flow trace with data values from the application. These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.

This paper studies runtime verification of distributed asynchronous systems and presents a monitor generation procedure for this purpose, which allows three-valued monitoring. The properties used in the monitors are specified in a logic that was newly created for this purpose and is called Distributed Temporal Logic (DTL). DTL combines the three-valued Linear Temporal Logic (LTL3) with the past-time Distributed Temporal Logic (ptDTL), which allows to mark subformulas for remote evaluation. The monitor generation presented in this paper is based on an adopted version of the LTL3monitor generation, which integrates the ptDTL monitor construction. The aim of this new procedure is to increase the amount of monitorable properties compared to the properties monitorable with ptDTL. Runtime verification using this new monitoring has been implemented on LEGO Mindstorms NXT robots communicating via Bluetooth.