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 is a lightweight verification approach that aims at checking that a run of a system under observation adheres to a formal specification. A classical approach is to synthesize a monitor from an LTL property. Usually, such a monitor receives the trace of the system under observation incrementally and checks the property with respect to the first position of any trace that extends the received prefix. This comes with the disadvantage that once the monitor detects a violation or satisfaction of the verdict it cannot recover and the erroneous position in the trace is not explicitly disclosed. An alternative monitoring problem, proposed for example for Past LTL evaluation, is to evaluate the LTL property repeatedly at each position in the received trace, which enables recovering and gives more information when the property is breached. In this paper we study this concept of recurrent monitoring in detail, particularly we investigate how the notion of anticipation (yielding future verdicts when they are inevitable) can be extended to recurrent monitoring. Furthermore, we show how two fundamental approaches in Runtime Verification can be applied to recurrent monitoring, namely Uncertainty—which deals with the handling of inaccurate or unavailable information in the input trace—and Assumptions, i.e. the inclusion of additional knowledge about system invariants in the monitoring process.

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.

Modern multi-core Systems-on-Chip (SoC) provide very high computational power. On the downside, they are hard to debug and it is often very difficult to understand what is going on in these chips because of the limited observability inside the SoC. Chip manufacturers try to compensate this difficulty by providing highly compressed trace data from the individual cores. In the past, the common way to deal with this data was storing it for later offline analysis, which severely limits the time span that can be observed. In this contribution, we present an FPGA-based solution that is able to process the trace data in real-time, enabling continuous observation of the state of a core. Moreover, we discuss applications enabled by this technology.

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.