Decentralized Crash-tolerant Runtime Verification of Distributed Systems

Seminar
Thursday, October 15, 2015
11:00 AM to 12:00 PM
POB 3.116
Free and open to the public

Runtime Verification (RV) is a lightweight method for monitoring the formal specification of a system (usually in some form of temporal logics) at execution time. First, I will show that existing logics and RV techniques are not capable of monitoring distributed systems in a consistent fashion, if monitors are prone to crash faults. To tackle this problem, I propose a family of multi-valued logics, LTL_K that has 2K + 4 truth values. In particular, LTL_K coincides with the well-known RV-LTL when K = 0. I will discuss how the truth values of LTL_K can be effectively used as a set of opinions emitted by local monitors in order to reach a consistent verdict for the corresponding global execution of the distributed system under inspection. I will also present an algorithm for local monitor construction as well as global runtime inference based on aggregation of local evaluation verdicts.

Contact Prof. Vijay Garg  at (512) 471-9424 for more information.

Sponsor: 

x x

Speaker

Borzoo Bonakdarpour

Borzoo Bonakdarpour

Assistant Professor
McMaster University

Borzoo Bonakdarpour is currently an assistant professor at the Department of Computing and Software at McMaster University, Canada.  His research interests include runtime monitoring of distributed systems and security/privacy policies, power-aware algorithms, and model synthesis. His work in these areas have received multiple best paper awards and nominations from highly prestigious conferences. He is the main developer of the tool SYCRAFT which is capable of synthesizing  fault-tolerant distributed protocols of size 10^80 reachable states  and beyond. His Ph.D. dissertation, "Automated Revision of Distributed  and Real-Time Programs", was nominated for the 2010 ACM Doctoral Dissertation Award. He has also received two Best Paper Awards from SSS'14 and SIES'10 conferences.