Temporal logic specification mining of programs

This paper proposes a dynamic approach of specification mining for Propositional Projection Temporal Logic (PPTL). To this end, a pattern library is built to collect some common temporal relation among events. Further, several algorithms of specification mining for PPTL are designed. With our approach, PPTL specifications are mined from a trace set of a target program by using patterns in the library. In addition, a specification mining tool PPTLMiner supporting this approach is developed. In practice, given a trace set and user selected patterns, PPTLMiner can capture PPTL specifications of target programs.

Authors

• Nan Zhang
• Bin Yu University of California, Berkeley
• Cong Tian Xidian University
• Zhenhua Duan Xidian University
• Xiaoshuai Yuan

Keywords

• Propositional projection temporal logic
• Pattern
• Trace
• Specification mining