Journal
JOURNAL OF PARALLEL AND DISTRIBUTED COMPUTING
Volume 185, Issue -, Pages -Publisher
ACADEMIC PRESS INC ELSEVIER SCIENCE
DOI: 10.1016/j.jpdc.2023.104801
Keywords
Metric temporal logic; Partial synchrony; Distributed systems; Runtime verification; Cross-chain protocols
Categories
Ask authors/readers for more resources
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.
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.
Authors
I am an author on this paper
Click your name to claim this paper and add it to your profile.
Reviews
Recommended
No Data Available