TeSSLa: Temporal stream-based specification language

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

doi:10.1007/978-3-030-03044-5_10

TeSSLa: Temporal stream-based specification language

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

^*Corresponding author for this work

Institute of Software Engineering and Programming Languages

Abstract

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 language	English
Title of host publication	SBMF 2018: Formal Methods: Foundations and Applications
Editors	Tiago Massoni, Mohammad Reza Mousavi
Number of pages	19
Volume	11254 LNCS
Publisher	Springer, Cham
Publication date	24.10.2018
Pages	144-162
ISBN (Print)	978-3-030-03043-8
ISBN (Electronic)	978-3-030-03044-5
DOIs	https://doi.org/10.1007/978-3-030-03044-5_10
Publication status	Published - 24.10.2018
Event	21st Brazilian Symposium on Formal Methods - Salvador, Brazil Duration: 26.11.2018 → 30.11.2018 Conference number: 221099

UN SDGs

This output contributes to the following UN Sustainable Development Goals (SDGs)

Access to Document

10.1007/978-3-030-03044-5_10

Cite this

Convent, L., Hungerecker, S., Leucker, M., Scheffel, T., Schmitz, M., & Thoma, D. (2018). TeSSLa: Temporal stream-based specification language. In T. Massoni, & M. R. Mousavi (Eds.), SBMF 2018: Formal Methods: Foundations and Applications (Vol. 11254 LNCS, pp. 144-162). (Lecture Notes in Computer Science ; Vol. 11254 LNCS). Springer, Cham. https://doi.org/10.1007/978-3-030-03044-5_10

@inproceedings{51712068da3c48fdac2fc9d8aff56996,

title = "TeSSLa: Temporal stream-based specification language",

abstract = "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{\textquoteright}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.",

author = "Lukas Convent and Sebastian Hungerecker and Martin Leucker and Torben Scheffel and Malte Schmitz and Daniel Thoma",

note = "Funding Information: This work is supported in part by the European COST Action ARVI, the BMBF project ARAMiS II with funding ID 01 IS 16025, and the European Horizon 2020 project COEMS under number 732016. Publisher Copyright: {\textcopyright} The Author(s) 2018. Copyright: Copyright 2019 Elsevier B.V., All rights reserved.; 21st Brazilian Symposium on Formal Methods, SBMF 2018 ; Conference date: 26-11-2018 Through 30-11-2018",

year = "2018",

month = oct,

day = "24",

doi = "10.1007/978-3-030-03044-5_10",

language = "English",

isbn = "978-3-030-03043-8",

volume = "11254 LNCS",

series = "Lecture Notes in Computer Science ",

publisher = "Springer, Cham",

pages = "144--162",

editor = "Massoni, {Tiago } and Mousavi, {Mohammad Reza }",

booktitle = "SBMF 2018: Formal Methods: Foundations and Applications",

}

Convent, L, Hungerecker, S, Leucker, M, Scheffel, T, Schmitz, M & Thoma, D 2018, TeSSLa: Temporal stream-based specification language. in T Massoni & MR Mousavi (eds), SBMF 2018: Formal Methods: Foundations and Applications. vol. 11254 LNCS, Lecture Notes in Computer Science , vol. 11254 LNCS, Springer, Cham, pp. 144-162, 21st Brazilian Symposium on Formal Methods, Salvador, Brazil, 26.11.18. https://doi.org/10.1007/978-3-030-03044-5_10

TeSSLa: Temporal stream-based specification language. / Convent, Lukas; Hungerecker, Sebastian; Leucker, Martin et al.
SBMF 2018: Formal Methods: Foundations and Applications. ed. / Tiago Massoni; Mohammad Reza Mousavi. Vol. 11254 LNCS Springer, Cham, 2018. p. 144-162 (Lecture Notes in Computer Science ; Vol. 11254 LNCS).

Research output: Chapters in Books/Reports/Conference Proceedings › Conference contribution › peer-review

TY - GEN

T1 - TeSSLa: Temporal stream-based specification language

AU - Convent, Lukas

AU - Hungerecker, Sebastian

AU - Leucker, Martin

AU - Scheffel, Torben

AU - Schmitz, Malte

AU - Thoma, Daniel

N1 - Conference code: 221099

PY - 2018/10/24

Y1 - 2018/10/24

N2 - 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.

AB - 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.

UR - https://www.scopus.com/record/display.uri?eid=2-s2.0-85057285112&origin=inward&txGid=3e8270bb84eeb0bc3d62d3f880e9a51e

U2 - 10.1007/978-3-030-03044-5_10

DO - 10.1007/978-3-030-03044-5_10

M3 - Conference contribution

SN - 978-3-030-03043-8

VL - 11254 LNCS

T3 - Lecture Notes in Computer Science

SP - 144

EP - 162

BT - SBMF 2018: Formal Methods: Foundations and Applications

A2 - Massoni, Tiago

A2 - Mousavi, Mohammad Reza

PB - Springer, Cham

T2 - 21st Brazilian Symposium on Formal Methods

Y2 - 26 November 2018 through 30 November 2018

ER -

TeSSLa: Temporal stream-based specification language

Abstract

UN SDGs

Access to Document

Other files and links

Fingerprint

Cite this