Distributed runtime verification of metric temporal properties

Distributed Systems are often composed of geographically separated components, where the clocks may not perfectly synchronized. As such verifying the correctness of such system properties are a major challenge and of utmost importance. In this paper, we describe a centralized runtime monitoring technique for distributed system. First, we propose a generalized runtime verification technique for verifying partially synchronous distributed computations for the metric temporal logic (MTL) by exploiting bounded-skew clock synchronization. Second, we introduce a progression-based formula rewriting scheme for monitoring MTL specifications which employs SMT solving techniques and report experimental results. Third, we also quantify each event according the possible time of occurrence and calculate the probabilistic guarantee for generating the verification verdict. Lastly, we have implemented the entire procedure and report on extensive synthetic experimental results UPPAAL, a set of cross-chain transactions implemented on Ethereum and an Industrial Control System of a treatment plant.

Automated summary

This paper presents a centralized runtime monitoring technique for distributed systems, which verifies the correctness of distributed computations by exploiting bounded-skew clock synchronization. By introducing a progression-based formula rewriting scheme and utilizing SMT solving techniques, the metric temporal logic can be monitored and the probabilistic guarantee for verification results can be calculated. Experimental results demonstrate the effectiveness of this technique in different application scenarios.