文章基本信息

标题：Decentralized Asynchronous Crash-Resilient Runtime Verification
本地全文：下载
作者：Borzoo Bonakdarpour ; Pierre Fraigniaud ; Sergio Rajsbaum 等
期刊名称：LIPIcs : Leibniz International Proceedings in Informatics
电子版ISSN：1868-8969
出版年度：2016
卷号：59
页码：16:1-16:15
DOI：10.4230/LIPIcs.CONCUR.2016.16
出版社：Schloss Dagstuhl -- Leibniz-Zentrum fuer Informatik
摘要：Runtime Verification (RV) is a lightweight method for monitoring the formal specification of a system during its execution. It has recently been shown that a given state predicate can be monitored consistently by a set of crash-prone asynchronous distributed monitors, only if sufficiently many different verdicts can be emitted by each monitor. We revisit this impossibility result in the context of LTL semantics for RV. We show that employing the four-valued logic Rv-LTL will result in inconsistent distributed monitoring for some formulas. Our first main contribution is a family of logics, called Ltl2k+4, that refines Rv-Ltl incorporating 2k + 4 truth values, for each k >= 0. The truth values of Ltl2k+4 can be effectively used by each monitor to reach a consistent global set of verdicts for each given formula, provided k is sufficiently large. Our second main contribution is an algorithm for monitor construction enabling fault-tolerant distributed monitoring based on the aggregation of the individual verdicts by each monitor.
关键词：Runtime monitoring; Distributed algorithms; Fault-tolerance