RTLola: Stream-based Real-time Monitoring

RTLola is a real-time monitoring toolkit for cyber-physical systems and networks. RTLola processes, evaluates, and aggregates streams of input data, such as sensor readings, and provides a real-time analysis in the form of comprehensive statistics and logical assessments of the system health. RTLola has been applied successfully in the monitoring of autonomous systems such as unmanned aircraft.

An RTLola monitor is generated from a formal description given in the RTLola specification language. RTLola specifications consist of stream equations that translate input streams into output streams. RTLola specifications are statically analyzed to determine the required memory and are then either directly executed by the RTLola interpreter, or compiled onto an FPGA.

RTLola has several key features that make it well-suited for applications that require a high level of expressiveness and efficiency and where the reliability of the monitor is safety-critical.

  • Formal specifications. The RTLola specification language is a highly expressive specification language with a precise formal semantics.
  • Reliable guarantees. RTLola monitors are guaranteed to never run out of memory, because the memory consumption is determined statically.
  • Maintainability and reusability. RTLola specifications are structured into multiple streams, which can be modified and reused with a high degree of flexibility. Specifications can immediately be evaluated in the RTLola interpreter.
  • Efficiency. The RTLola toolkit also includes a compiler to VHDL, which makes it possible to run highly efficient, parallelized RTLola monitors on FPGAs with very limited resources.

The RTLola Language

RTLola receives incoming data in the form of timed, and possibly asynchronous, input streams. The RTLola specification language uses stream equations to translate input streams into output streams. Stream equations play a similar role as variable assignments in standard programming languages. They filter incoming data, compare values from different streams, or carry out more complex computations. RTLola supports different accesses to streams such as direct accesses of current stream values, offset accesses to access previous values, or aggregations, such as averaging the values from stream over a certain temporal window. The produced output can be periodic, i.e., at predefined points in time, or follow the flow of the incoming data. To recognize safety violations, the specification contains triggers consisting of a boolean expression and an alarm message. Triggers characterize critical situations that require further action.

Overview of RTLola

As a starting point for RTLola, we recommend the tutorial available here. In the tutorial, we describe specifications to monitor an autonomous drone. The example files can be downloaded here.

The RTLola Interpreter and Compiler

The implementation of the RTLola toolkit is organized into the frontend and several backends. The frontend takes a specification file and produces an intermediate representation (IR). This representation contains an abstract syntax tree (AST) of the specification and includes additional information relevant for the backends.

Overview of the RTLola Toolkit

RTLola specifications can be run in the software-based interpreter or compiled into the hardware description language VHDL. The interpreter takes the IR and interprets the specification based on the incoming data of the system. The incoming data can be read from a CSV file or received from the standard input. In any case, the monitor prints trigger messages on the standard output. The VHDL-compilation on the other hand takes the IR and produces VHDL code, describing a monitor for the given specification. The corresponding input wires in the monitor implementation receive the input, and the current stream values are stored on the corresponding output wires. With this setup, the monitor can be integrated into the system itself or as a separate component after implementing the missing communication, i.e., a UDP communication where the monitor analyzes the UDP packages sent by the system. The VHDL description can then be synthesized onto an FPGA.

Availability

The pre-compiled RTLola interpreter is available for Linux, macOS, and Windows.

Older versions of RTLola are available here.
  • streamlab-0.3.1.zip (2020-03-09) sha256: 8ae52c5c9a56facb397f1dd49828aac031d15c818e1d0e99485ba502f9e3bac0
  • streamlab-0.3.0.zip (2020-02-27) sha256: 0aa4c7d524cd02d1979f9904886901dcc3f52ccca75050bddae627ac5a64d58a
  • streamlab-0.2.0.zip (2019-08-23) sha256: 297c60630a4ca6dd38b9db9776491ca72eb5572fb43d19c6e340e6cd73f9a37d
  • streamlab-0.1.0.zip (2019-08-12) sha256: 68a96699840294787d2373829150fc1333411a2582225daf9ad1334e566e8727

Note that the RTLola implementation was previously named “StreamLAB”.

The implementation is also available open-source at github. The separate modules are available under the following links:

License

The binaries of the RTLola toolkit are distributed under the RTLOLA END USER LICENSE. The open source code of the frontend and the interpreter are licensed under the Apache License, Version 2. The code for the VHDL-compiler is licensed under GNU Affero General Public License, Version 3.

If you intend to use RTLola in any form prohibited by the license, please contact us.

Publications

We suggest to cite the following paper as a general reference for RTLola and the implementation:

StreamLAB: Stream-based Monitoring of Cyber-physical Systems

Peter Faymonville, Bernd Finkbeiner, Malte Schledjewski, Maximilian Schwenger, Marvin Stenger, Leander Tentrup, Hazem Torfah.
CAV 2019

The following publications describe the various features and applications of RTLola in more detail.

Verified Rust Monitors for Lola Specifications

Bernd Finkbeiner, Stefan Oswald, Noemi Passing, and Maximilian Schwenger.
RV 2020

Monitoring Cyber-Physical Systems: From Design to Integration

Maximilian Schwenger.
RV 2020

Verified Rust Monitors for Lola Specifications

Jan Baumeister, Bernd Finkbeiner, Matthis Kruse, and Maximilian Schwenger.
RV 2020

RTLola Cleared for Take-Off: Monitoring Autonomous Aircraft

Jan Baumeister, Bernd Finkbeiner, Sebastian Schirmer, Maximilian Schwenger and Christoph Torens.
CAV 2020

Stream-based Monitors for Real-time Properties.

Hazem Torfah.
RV @FM 2019

FPGA Stream-Monitoring of Real-time Properties.

Jan Baumeister, Bernd Finkbeiner, Maximilian Schwenger, Hazem Torfah.
EMSOFT 2019

Towards Intelligent System Health Management using Runtime Monitoring.

Christoph Torens, Florian-Michael Adolf, Peter Faymonville, Sebastian Schirmer.
AIAA Information Systems-AIAA Infotech @ Aerospace. Grapevine, Texas.

A Stream-based Specification Language for Network Monitoring.

Peter Faymonville, Bernd Finkbeiner, Sebastian Schirmer and Hazem Torfah.
RV2016.

LOLA: Runtime Monitoring of Synchronous Systems.

Ben d’Angelo, Sriram Sankaranarayanan, Cesar Sanchez, Will Robinson, Bernd Finkbeiner, Henny B. Sipma, Sandeep Mehrotra, Zohar Manna.
TIME 2005.

Contributors

The toolkit is based on the implementation and research of the following people:

Contact

If you have questions or problems, please contact us.