TeSSLa: Temporal stream-based specification language

Lukas Convent*, Sebastian Hungerecker, Martin Leucker, Torben Scheffel, Malte Schmitz, Daniel Thoma

*Corresponding author for this work


Runtime verification is concerned with monitoring program traces. In particular, stream runtime verification (SRV) takes the program trace as input streams and incrementally derives output streams. SRV can check logical properties and compute temporal metrics and statistics from the trace. We present TeSSLa, a temporal stream-based specification language for SRV. TeSSLa supports timestamped events natively and is hence suitable for streams that are both sparse and fine-grained, which often occur in practice. We prove results on TeSSLa’s expressiveness and compare different TeSSLa fragments to (timed) automata, thereby inheriting various decidability results. Finally, we present a monitor implementation and prove its correctness.

Original languageEnglish
Title of host publicationSBMF 2018: Formal Methods: Foundations and Applications
EditorsTiago Massoni, Mohammad Reza Mousavi
Number of pages19
Volume11254 LNCS
PublisherSpringer, Cham
Publication date24.10.2018
ISBN (Print)978-3-030-03043-8
ISBN (Electronic)978-3-030-03044-5
Publication statusPublished - 24.10.2018
Event21st Brazilian Symposium on Formal Methods - Salvador, Brazil
Duration: 26.11.201830.11.2018
Conference number: 221099


Dive into the research topics of 'TeSSLa: Temporal stream-based specification language'. Together they form a unique fingerprint.

Cite this