期刊
JOURNAL OF PARALLEL AND DISTRIBUTED COMPUTING
卷 185, 期 -, 页码 -出版社
ACADEMIC PRESS INC ELSEVIER SCIENCE
DOI: 10.1016/j.jpdc.2023.104801
关键词
Metric temporal logic; Partial synchrony; Distributed systems; Runtime verification; Cross-chain protocols
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.
作者
我是这篇论文的作者
点击您的名字以认领此论文并将其添加到您的个人资料中。
推荐
暂无数据