POLIMON: Checking Temporal Properties over Out-of-order Streams at Runtime

TL;DR

POLIMON is a runtime monitoring tool capable of checking temporal properties over out-of-order system event streams, enabling prompt violation detection in distributed systems with unreliable communication.

Contribution

The paper introduces POLIMON, a novel runtime monitoring tool that handles out-of-order messages and provides immediate verdicts for real-time system specifications.

Findings

POLIMON effectively detects violations promptly.

Handles out-of-order message streams.

Suitable for distributed systems with unreliable channels.

Abstract

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.