Show simple item record

dc.contributor.authorHasabelnaby, Mennatallah 18:00:27 (GMT) 18:00:27 (GMT)
dc.description.abstractRuntime verification is a lightweight automated formal method for specification-based run- time 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 work, 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 set of iOS devices running a distributed program 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.en
dc.publisherUniversity of Waterlooen
dc.subjectDistributed systemsen
dc.subjectruntime verificationen
dc.subjectmonitoring of distributed systemsen
dc.titleDecentralized Runtime Verification of LTL Specifications in Distributed Systemsen
dc.typeMaster Thesisen
dc.pendingfalse R. Cheriton School of Computer Scienceen Scienceen of Waterlooen
uws-etd.degreeMaster of Mathematicsen
uws.contributor.advisorBonakdarpour, Borzoo
uws.contributor.affiliation1Faculty of Mathematicsen

Files in this item


This item appears in the following Collection(s)

Show simple item record


University of Waterloo Library
200 University Avenue West
Waterloo, Ontario, Canada N2L 3G1
519 888 4883

All items in UWSpace are protected by copyright, with all rights reserved.

DSpace software

Service outages