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

^*Korrespondierende/r Autor/-in für diese Arbeit

Institut für Softwaretechnik und Programmiersprachen

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.

Originalsprache	Englisch
Titel	SBMF 2018: Formal Methods: Foundations and Applications
Redakteure/-innen	Tiago Massoni, Mohammad Reza Mousavi
Seitenumfang	19
Band	11254 LNCS
Herausgeber (Verlag)	Springer, Cham
Erscheinungsdatum	24.10.2018
Seiten	144-162
ISBN (Print)	978-3-030-03043-8
ISBN (elektronisch)	978-3-030-03044-5
DOIs	https://doi.org/10.1007/978-3-030-03044-5_10
Publikationsstatus	Veröffentlicht - 24.10.2018
Veranstaltung	21st Brazilian Symposium on Formal Methods - Salvador, Brasilien Dauer: 26.11.2018 → 30.11.2018 Konferenznummer: 221099

UN SDGs

Dieser Output leistet einen Beitrag zu folgendem(n) Ziel(en) für nachhaltige Entwicklung

Zugriff auf Dokument

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

Andere Dateien und Links

www.scopus.com

Zitieren

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 (Hrsg.), SBMF 2018: Formal Methods: Foundations and Applications (Band 11254 LNCS, S. 144-162). (Lecture Notes in Computer Science ; Band 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 (Hrsg.), SBMF 2018: Formal Methods: Foundations and Applications. Bd. 11254 LNCS, Lecture Notes in Computer Science , Bd. 11254 LNCS, Springer, Cham, S. 144-162, 21st Brazilian Symposium on Formal Methods, Salvador, Brasilien, 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. Hrsg. / Tiago Massoni; Mohammad Reza Mousavi. Band 11254 LNCS Springer, Cham, 2018. S. 144-162 (Lecture Notes in Computer Science ; Band 11254 LNCS).

Publikation: Kapitel in Büchern/Berichten/Konferenzbänden › Konferenzbeitrag › Begutachtung

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

Zugriff auf Dokument

Andere Dateien und Links

Fingerprint

Zitieren