Learn more about TeSSLa and its tools.
TeSSLa Introduction
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. Read this short introduction if you want to see some simple example on which properties can be expressed with TeSSLa.
Quick Start Guide: Using The TeSSLa Compiler and Interpreter
The TeSSLa compiler and interpreter takes a TeSSLa specification and an input trace, compiles the TeSSLa specification and generates an output trace by applying the compiled specification to the input trace. Read this guide for a getting started guide with the TeSSLa interpreter using the text based trace format.
TeSSLa Basic Operators
TeSSLa's full expressiveness can be achieved with the five basic operators nil, unit, lift, last and delay. While in practical applications one wants to use all the operators available in the standard library, having a very small language core with a formal semantics is helpful for thorough theoretical analysis of the language. Read this guide if you want to learn more about these five basic operators and how the other operators are derived from them. This guide is a good introduction if you want to dive deeper into the scientific publications related to TeSSLa.
Publications and Presentations
TeSSLa has successfully been used and refined together with multiple academic and industrial partners in national and international scientific research projects. Read the scientific publications on TeSSLa if you want to learn more about its formal semantics and its expressiveness. There is also scientific work on applying TeSSLa to event streams with partial information.
TeSSLa Tutorial
This tutorial will give you an overview over the stream processing language TeSSLa. You will learn everything you need to know in order to write your own TeSSLa specifications. We will start with the basic TeSSLa operators and their usage in potentially recursive equations. Then we will have a look at TeSSLa's macro expansion and type system as well as complex data types and how to use those in TeSSLa.
Runtime Verification With TeSSla
Runtime verification is the research field of how to monitor your application at runtime. In this tutorial you will learn how to use TeSSLa's C code transformation tools to instrument your C code so that you can get events from the running application and how to verify such an event stream with TeSSLa.
Using the TeSSLa Playground
The TeSSLa playground is available online and is intended for an easy and exploratory usage of the TeSSLa compiler and interpreter. You can simply enter and modify a TeSSLa specification and an input trace in the web IDE and you can immediately inspect the processed output trace. The TeSSLa Visualizer helps you to quickly get an overview on the nature of a TeSSLa trace. Read this short guide if you need more information on how to interact with the web IDE and how to use the TeSSLa Visualizer.
TeSSLa Language Specification 2.0
The TeSSLa Language Specification is the official specification of TeSSLa's syntax and semantics. The document is not meant as a tutorial for neither the TeSSLa language nor for supporting tools, but it may be used as reference to build own TeSSLa compilers and tools and verify them w.r.t. language conformance.
The TeSSLa standard library is an extensive library of operators and functions. It is delivered with the TeSSLa bundle and can be used in TeSSLa specifications. You can look up the definitions and usages of the standard library functions in this reference: