Back to overview

Runtime Verification of Temporal Properties over Out-of-order Data Streams

Type of publication Peer-reviewed
Publikationsform Proceedings (peer-reviewed)
Author Basin David, Klaedtke Felix, Zălinescu Eugen,
Project Big Data Monitoring
Show all

Proceedings (peer-reviewed)

Volume (Issue) 10426 LNCS
Page(s) 356 - 376
Title of proceedings Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
DOI 10.1007/978-3-319-63387-9_18


We present a monitoring approach for verifying systems at runtime. Our approach targets systems whose components communicate with the monitors over unreliable channels, where messages can be delayed or lost. In contrast to prior works, whose property specification languages are limited to propositional temporal logics, our approach handles an extension of the real-time logic MTL with freeze quantifiers for reasoning about data values. We present its underlying theory based on a new three-valued semantics that is well suited to soundly and completely reason online about event streams in the presence of message delay or loss. We also evaluate our approach experimentally. Our prototype implementation processes hundreds of events per second in settings where messages are received out of order.