Runtime Verification over Out-of-order Streams

DOI10.1145/3355609MaRDI QIDQ4972169zbMATH OpenOpenAlexWikidataFDO

Authors Felix Klaedtke, Eugen Zălinescu, David Basin

Publication date 22 November 2019

Published in ACM Transactions on Computational Logic (Search for Journal in Brave)

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

zbMATH Keywords

distributed systemsKleene logicruntime verificationstream processingtemporal logic

Mathematics Subject Classification ID

Temporal logic (03B44) Modes of computation (nondeterministic, parallel, interactive, probabilistic, etc.) (68Q10) Specification and verification (program logics, model checking, etc.) (68Q60) Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85)

Abstract: We present an approach for verifying systems at runtime. Our approach targets distributed systems whose components communicate with monitors over unreliable channels, where messages can be delayed, reordered, or even lost. Furthermore, our approach handles an expressive specification language that extends the real-time logic MTL with freeze quantifiers for reasoning about data values. The logic's main novelty is a new three-valued semantics that is well suited for runtime verification as it accounts for partial knowledge about a system's behavior. Based on this semantics, we present online algorithms that reason soundly and completely about streams where events can occur out of order. We also evaluate our algorithms experimentally. Depending on the specification, our prototype implementation scales to out-of-order streams with hundreds to thousands of events per second.

Recommendations

• Runtime verification of temporal properties over out-of-order data streams
• Foundations of Boolean stream runtime verification
• Formal verification of out-of-order execution with incremental flushing
• Declarative stream runtime verification (hLola)
• The ins and outs of first-order runtime verification
• Runtime verification through forward chaining

Cited in

(11)

• Formal verification of out-of-order execution with incremental flushing
• Runtime verification of temporal properties over out-of-order data streams
• Foundations of Boolean stream runtime verification
• A normalized form for FIFO protocols traces, application to the replay of mode-based protocols
• Failure-aware runtime verification of distributed systems
• Runtime enforcement with reordering, healing, and suppression
• Decentralized runtime verification of message sequences in message-based systems
• Interaction-based offline runtime verification of distributed systems
• Decentralized deadlock-free enforcement of message orderings in message-based systems
• Runtime verification of partially-synchronous distributed system
• Runtime enforcement with event reordering

This page was built for publication: Runtime Verification over Out-of-order Streams

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