TeSSLa Introduction

TeSSLa is a general purpose stream-transformation language. TeSSLa is rather a stream-based specification language than a programming language. TeSSLa is well suited for simple system descriptions. TeSSLa provides a different and perhaps more abstract perspective on the system under observation than its actual implementation.

Nevertheless, TeSSLa still feels natural to programmers and is neither too abstract nor requires previous knowledge in mathematical logic. With TeSSLa one can directly describe monitoring algorithms, it is not a mathematical logic describing valid runs of the systems. Aside from making TeSSLa easier to use for the practical software engineer this also allows to use TeSSLa for event filtering and quantitative and statistical analysis as well as live debugging sessions.

The most basic form of a stream is a sequence of events. For example the following stream x contains four events with the data values 3, 1, 4 and 1:

stream x: bubbles
---
1: x = 3
2: x = 1
3: x = 4
4: x = 1

TeSSLa transforms streams by deriving new streams from existing streams in a declarative functional way: One can define new streams by applying operators to the existing streams but all streams are immutable. For example the stream y was derived from the above stream x by adding 5 to every event's data value:

stream y: bubbles
---
1: y = 8
2: y = 6
3: y = 9
4: y = 6

This relation between the input stream x and the output stream y can be described with the following TeSSLa specification:

in x: Events[Int]
def y = x + 5
out y

Time is a first-class citizen in TeSSLa, making the specification of timed properties as simple as possible. This makes it more natural to reason about time constraints. In cyber-physical systems events are often caused by external inputs of the physical system and hence not following regular clock ticks, but are appearing with variable frequency. In order to simplify specifications over such event streams, every event in TeSSLa always carries a time stamp and a data value:

option axis: true
option timeDomain: [0,20]
---
4: y = 8
6: y = 6
12: y = 9
15: y = 6

The next section shows more practical examples of TeSSLa specifications applied to (timed) event streams.

TeSSLa In Action

As an example for a monitoring specification in TeSSLa, consider the following specification which checks whether a measured temperature stays within given boundaries. For every new event (measurement) on the temperature stream, new events on the derived streams low, high and unsafe are computed:

in temperature: Events[Int]

def low := temperature < 3
def high := temperature > 8
def unsafe := low || high

out unsafe

Read and write events occur independently at different frequencies. The derived stream numReads (numWrites) counts the number of events of the input stream read (write). While the read and write streams contain only discrete events, the number of events can be seen as a piece-wise constant signal with the initial value of 0. The difference between the two signals is evaluated every time one of the two signals changes its value using the last known value of both signals. We call this concept signal semantics: TeSSLa handles internally only streams of discrete events, but one can express operators following signal semantics in TeSSla and hence these discrete events can be seen as those points in time where the signal changes its value. In TeSSLa operators are automatically lifted to signal semantics.

in read: Events[Unit]
in write: Events[Unit]

def numReads := count(read)
def numWrites := count(write)
def safe := numWrites - numReads <= 2

out safe

In TeSSLa, every event has a timestamp which can be accessed via the time operator. Since every event has a timestamp which is referring to a global clock and is unique for its stream, accessing the timestamps of events serves two purposes: Accessing the global order of events by comparing timestamps and performing calculations with the timestamps. Consider e.g. the following specification which checks whether the lapse of time between two write events exceeds 5 time units and outputs the overtime if it does:

in write: Events[Unit]

def diff := time(write) - prev(time(write))
def error := filter(diff > 5, diff - 5)

out error

In the example, the stream diff − 5 is filtered by the condition diff > 5. Note that the property violation is only reported when the delayed event happens. To report such errors as soon as possible, TeSSLa has the ability to create events at certain points in time via the delay operator. The following specification checks the same property but raises a unit event on the error stream as soon as we know that there was no write event in time:

in write: Events[Unit]

def timeout := const(5, write)
def error := delay(timeout, write)

out error

The delay function works as a timer, which is set to a timeout value with the first argument and reset with any event on the second argument. In the example, the function const(5, write) maps the values of events to the constant value of 5, which is then used as timeout value. While in all the other examples the derived streams only contain events with timestamps taken from the input streams, in this example events with additional timestamps are generated.

Summary

TeSSLa is a temporal stream-based specification language designed for specifying and analyzing the behavior of cyber-physical systems, where timing is a critical issue. TeSSLa is ideally suited for stream runtime verification (SRV) and comes with tools supporting this goal. TeSSLa supports timestamped events natively and is hence suitable for streams that are both sparse and fine-grained.

Stream Runtime Verification. SRV is a combination of complex event processing (CEP) and traditional runtime verification (RV) approaches: Streams are transformed into streams and there is not only one final verdict but the output is a stream of the property being evaluated at every change of the input stream. TeSSLa supports a declarative programming style, which is perfectly suited for correctness properties and specifications.

Time as First-Class Citizen. TeSSLa doesn’t require all streams to have simultaneous events and hence supports both sparse and high-frequency streams. In TeSSLa, every event has a timestamp which can be accessed via the time operator. Accessing the timestamps of events serves two purposes: Accessing the global order of events by comparing timestamps and performing calculations with the timestamps.

Modular Architecture. TeSSLa relates a set of input streams to a set of output streams via mutually recursive equations, which allows self-references to the past. With this inherent support for recursive equations TeSSLa can maintain a huge expressiveness which is based only on very few primitive operators. TeSSLa has a complex type and macro system which supports domain specific standard libraries.

Efficient Parallel Evaluation. TeSSLa’s design follows two principles to allow efficient evaluation on parallel hardware: Explicit memory usage and local operator composition. If TeSSLa operates only on streams with bounded data-types of constant size, then the operators only need finite memory because every operator only needs to store at most one data value. This allows implementations on systems without random access memory, e.g. FPGAs or embedded systems.