kirancodes.me
To Proof Maintenance & Beyond!
ICSE 2004

Efficient Decentralized Monitoring of Safety in Distributed Systems

Koushik Sen, Abhay Vardhan, Gul Agha, Grigore Rosu

DOI 10.1109/icse.2004.1317464dblp

Abstract

We describe an efficient decentralized monitoring algorithm that monitors a distributed program's execution to check for violations of safety properties. The monitoring is based on formulae written in PT-DTL, a variant of past time linear temporal logic that we define. PT-DTL is suitable for expressing temporal properties of distributed systems. Specifically, the formulae of PT-DTL are relative to a particular process and are interpreted over a projection of the trace of global states that represents what that process is aware of. A formula relative to one process may refer to other processes' local states through remote expressions and remote formulae. In order to correctly evaluate remote expressions, we introduce the notion of Knowledge Vector and provide an algorithm which keeps a process aware of other processes' local states that can affect the validity of a monitored PT-DTL formula. Both the logic and the monitoring algorithm are illustrated through a number of examples. Finally, we describe our implementation of the algorithm in a tool called DIANA.

BibTeX
@inproceedings{Sen-al:ICSE04,
  author    = {Koushik Sen and
               Abhay Vardhan and
               Gul Agha and
               Grigore Rosu},
  title     = {Efficient Decentralized Monitoring of Safety in Distributed Systems},
  booktitle = {ICSE},
  pages     = {418--427},
  publisher = {{IEEE} Computer Society},
  year      = {2004},
}

Related papers