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.