POLIMON: Checking Temporal Properties over Out-of-order Streams at Runtime
arxiv(2024)
摘要
This paper presents the monitoring tool POLIMON for checking system behavior
at runtime against specifications expressed as formulas in the real-time logic
MTL or its extension with the freeze quantifier. The tool's distinguishing
feature is that POLIMON can receive messages describing the system events out
of order. Furthermore, since POLIMON processes received messages immediately,
it outputs verdicts promptly when a message's described system event leads to a
violation of the specification. This makes the tool well suited, e.g., for
verifying the behavior of distributed systems with unreliable channels at
runtime.
更多查看译文
AI 理解论文
溯源树
样例
生成溯源树,研究论文发展脉络
Chat Paper
正在生成论文摘要