Runtime Verification over Out-of-order Streams
(From the article abstract)
We present an approach for verifying systems at run-time. 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 specifcation language that extends the real-time logic MTL with freeze quantifers for reasoning about data values. The logic’s main novelty is a new three-valued semantics that is well suited for runtime verifcation 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 specifcation, our prototype implementation scales to out-of-order streams with hundreds to thousands of events per second.
This article is a contribution for ACM Transactions of Computational Logic