Mining Specifications From System Executions Using Temporal Logic

This talk addresses the following problem: given a finite set of system executions, and a template of expected behavior given as a formula in temporal logic with missing sub-formulas, compute the missing sub-formulas that make the formula true for all executions. This so-called query-checking problem has many applications in the analysis of time-series data, including vulnerability detection in server logs and financial trend discovery, as well as generally in system comprehension and system-specification mining. The presentation will introduce temporal logic and motivate temporal-logic query checking as a tool for investigating system executions to uncover root causes for observed system behavior. It then outlines the techniques developed by UMD researchers to automate the solving of these queries. Preliminary experimental results of a prototype implementation are also given. This work is joint with Sam Huang.