Skip to main content

Decentralized Runtime Verification of LTL Specifications in Distributed Systems

Publication Type
Year of Publication
Conference/Journal Name
IEEE International Parallel & Distributed Processing Symposium (IPDPS)
Runtime verification is a lightweight automated formal method for specification-based runtime monitoring as well as testing of large real-world systems. While numerous techniques exist for runtime verification of sequential programs, there has been very little work on specification-based monitoring of distributed systems. In this paper, we propose the first sound and complete method for runtime verification of asynchronous distributed programs for the 3-valued semantics of LTL specifications defined over the global state of the program. Our technique for evaluating LTL properties is inspired by distributed computation slicing, an approach for abstracting distributed computations with respect to a given predicate. Our monitoring technique is fully decentralized in that each process in the
distributed program under inspection maintains a replica of the monitor automaton. Each monitor may maintain a set of possible
verification verdicts based upon existence of concurrent events. Our experiments on runtime monitoring of a simulated swarm
of flying drones show that due to the design of our Algorithm, monitoring overhead grows only in the linear order of the number
of processes and events that need to be monitored.