Decentralized Asynchronous Crash-resilient Runtime Verification
Decentralized Asynchronous Crash-resilient Runtime Verification
复制标题
去中心化异步抗崩溃运行时验证
DOI：
10.1145/3550483
复制
发表时间：
2022
影响因子：
2.5
通讯作者：
Travers, Corentin
中科院分区：
文献类型：
--
作者：
Bonakdarpour, Borzoo;Fraigniaud, Pierre;Rajsbaum, Sergio;Rosenblueth, David;Travers, Corentin
验证是一种轻量级的方法，用于在系统执行期间监视系统的形式规格说明。最近的研究表明，一个给定的状态谓词可以被一组容易崩溃的分布式监视器一致地监视，只有当每个监视器可以发出从一个足够大的有限集合中得出的判决。我们重新审视这一不可能的结果在具体的线性时间逻辑（ltl）语义的运行时验证，也就是说，当系统的正确性是指定的anltlformula在其执行轨迹。首先，我们表明，监视器合成的基础上的4值语义的fltl（rv-ltl）可能会导致不一致的分布式监测，即使是一些simpleltlformulas。更一般地说，给定一个公式φ，我们将监控器持续监控φ所需的不同判决数与φ的一个特定结构特征（称为它的突变数）联系起来。具体地说，我们表明，对于每个k ≥ 0，有一个ltlformula φ的交替数k，不能在运行时由分布式监视器发出的判决，从一组基数较小的感谢+ 1验证。在积极的一面，我们定义了一族逻辑，称为distributedltl（简称为dltl），参数为k ≥ 0，它通过增加2k + 4个真值来改进rv-ltl。我们的主要贡献是证明，对于每个k ≥ 0，每个具有交替数k的公式φ都可以被分布式监视器一致地监视，每个监视器运行一个基于dltl族中的（2 k/2 +4）值逻辑的自动机。
Runtime verificationis 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 asynchronousdistributedmonitors observing the system, only if each monitor can emit verdicts taken from alarge enoughfinite set. We revisit this impossibility result in the concrete context of linear-time logic (ltl) semantics for runtime verification, that is, when the correctness of the system is specified by anltlformula on its execution traces. First, we show that monitors synthesized based on the 4-valued semantics ofltl(rv-ltl) may result in inconsistent distributed monitoring, even for some simpleltlformulas. More generally, given anyltlformula φ, we relate the number of different verdicts required by the monitors for consistently monitoring φ, with a specific structural characteristic of φ called itsalternation number. Specifically, we show that, for everyk ≥ 0, there is anltlformula φ with alternation numberkthat cannot be verified at runtime by distributed monitors emitting verdicts from a set of cardinality smaller thank+ 1. On the positive side, we define a family of logics, calleddistributedltl(abbreviated asdltl), parameterized byk≥ 0, which refinesrv-ltlby incorporating2k+ 4 truth values. Our main contribution is to show that, for everyk≥ 0, everyltlformula φ with alternation numberkcan be consistently monitored by distributed monitors, each running an automaton based on a (2 ⌈k/2 ⌉ +4)-valued logic taken from thedltlfamily.
登录
查看更多内容
影响因子：
0.8
作者：
A. Bauer;Yliès Falcone
通讯作者：
A. Bauer;Yliès Falcone
DOI：
10.1007/978-3-540-75142-7_32
发表时间：
2007-09
期刊：
--
影响因子：
--
作者：
V. Ogale;V. Garg
通讯作者：
V. Ogale;V. Garg
分布式系统中 LTL 规范的去中心化运行时验证
DOI：
10.1109/ipdps.2015.95
发表时间：
2015
期刊：
2015 IEEE International Parallel and Distributed Processing Symposium
影响因子：
--
作者：
Menna Mostafa;Borzoo Bonakdarpour
通讯作者：
Borzoo Bonakdarpour
影响因子：
0.8
作者：
C. Colombo;Yliès Falcone
通讯作者：
C. Colombo;Yliès Falcone
DOI：
10.1109/srds.2013.19
发表时间：
2013-04
期刊：
2013 IEEE 32nd International Symposium on Reliable Distributed Systems
影响因子：
--
作者：
Himanshu Chauhan;V. Garg;Aravind Natarajan;N. Mittal
通讯作者：
Himanshu Chauhan;V. Garg;Aravind Natarajan;N. Mittal