2026-07-23T08:16:05Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:5619 2024-03-06T10:36:47Z ddc:004 open_access

Failure-aware Runtime Verification of Distributed Systems Basin, David Klaedtke, Felix Zalinescu, Eugen Runtime verification monitoring algorithm real-time logics multi-valued semantics distributed systems asynchronous communication Prior runtime-verification approaches for distributed systems are limited as they do not account for network failures and they assume that system messages are received in the order they are sent. To overcome these limitations, we present an online algorithm for verifying observed system behavior at runtime with respect to specifications written in the real-time logic MTL that efficiently handles out-of-order message deliveries and operates in the presence of failures. Our algorithm uses a three-valued semantics for MTL, where the third truth value models knowledge gaps, and it resolves knowledge gaps as it propagates Boolean values through the formula structure. We establish the algorithm's soundness and provide completeness guarantees. We also show that it supports distributed system monitoring, where multiple monitors cooperate and exchange their observations and conclusions. Schloss Dagstuhl – Leibniz-Zentrum für Informatik David Basin and Felix Klaedtke and Eugen Zalinescu 2015 Is Part Of LIPIcs, Volume 45, 35th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2015) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.FSTTCS.2015.590 urn:nbn:de:0030-drops-56194 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2015.590 eng https://creativecommons.org/licenses/by/3.0/legalcode