Runtime Verification

Computers now control many important aspects of our lives. We depend on them in many safety-critical applications such as health and aviation. While it is important to verify the program before it is operational, it is equally important to verify each execution during the operation. This is especially true for concurrent and distributed programs where interaction with the environment may lead to subtle synchronization bugs. We are developing a theory, associated algorithms and a package that allows efficient runtime verification. Our theory exploits the fact that the set of consistent global states form a distributive lattice. We apply lattice theory extensively to develop efficient algorithms. Some specific accomplishments are as follows.

• Tools and techniques for computation slicing: The concept of computation slicing was introduced by us in 2001 at ICDCS for which it received the best paper nomination. A computation slice with respect to a predicate is a subcomputation that includes all the consistent global states that satisfy the predicate. We have given efficient algorithms for computing the slice when the predicates satisfy certain properties. Our algorithm exploits Birkhoff's theorem for finite distributive lattices. Slicing allows detection of unstable predicates that were not possible to detect using earlier techniques. It also allows efficient detection of temporal logic predicates on a computation. The paper was generalized in a DISC 2001 paper where algorithms to compose slices are provided. (ICDCS 2001, DISC 2001, ICDCS 2003, IPDPS 2004, Distributed Computing 2006)
• Efficient Detection of Temporal Logic Predicates: Current algorithms (in the area of model-checking) work on explicit or symbolic representation of state transition graph for checking temporal logic formulas. The state-transition graph for a single execution can be of size exponential in the number of processes. We have developed polynomial time algorithms for detecting temporal logic predicates under certain conditions. (IPDPS 2002, RV 2003, FATES'2003, OPODIS 2003)