TeSSLa: temporal stream-based specification language

DOI10.1007/978-3-030-03044-5_10MaRDI QIDQ6165893zbMATH OpenOpenAlexFDO

Authors Lukas Convent, Sebastian Hungerecker, Martin Leucker, Torben Scheffel, M. Schmitz, Daniel Thoma

Publication date 2 August 2023

Published in Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL https://arxiv.org/abs/1808.10717

Mathematics Subject Classification ID

Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Formal languages and automata (68Q45) Specification and verification (program logics, model checking, etc.) (68Q60)

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.

Recommendations

• Foundations of Boolean stream runtime verification
• Declarative stream runtime verification (hLola)
• Runtime verification of temporal properties over out-of-order data streams
• Runtime verification logics. A language design perspective
• Time-triggered runtime verification

Cited in

(10)

• Declarative stream runtime verification (hLola)
• Multi-head monitoring of metric temporal logic
• Property-based testing for Spark Streaming
• Temporal stream logic modulo theories
• Symbolic runtime verification for monitoring under uncertainties and assumptions
• Runtime verification of real-time event streams using the tool HStriver
• An Operational Guide to Monitorability
• Verified first-order monitoring with recursive rules
• Uncertainty in runtime verification: a survey
• TeSSLa-ROS-bridge -- runtime verification of robotic systems

This page was built for publication: TeSSLa: temporal stream-based specification language

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q6165893)