Paper Info
Title
Decentralized Runtime Verification of LTL Specifications in Distributed Systems
Abstract
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.
Year
DOI
Venue
2015
10.1109/IPDPS.2015.95
International Parallel & Distributed Processing Symposium
Keywords
Field
DocType
Runtime monitoring, Asynchronous distributed systems, Formal methods
Replica,Asynchronous communication,Swarm behaviour,Computer science,Slicing,Parallel computing,Automaton,Runtime verification,Formal methods,Semantics,Distributed computing
Conference
ISSN
Citations 
PageRank 
1530-2075
19
0.76
References 
Authors
8
2
Name
Order
Citations
PageRank
Menna Mostafa1190.76
Borzoo Bonakdarpour249045.02