Symbolic mining of temporal specifications

Program specifications are important in many phases of the software development process, but they are often omitted or incomplete. An important class of specifications takes the form of temporal properties that prescribe proper usage of components of a software system. Recent work has focused on the automated inference of temporal specifications from the static or runtime behavior of programs. Many techniques match a specification pattern (represented by a finite state automaton) to all possible combinations of program components and enumerate the possible matches. Such approaches suffer from high space complexity and have not scaled beyond simple, two-letter alternating patterns (e.g. (ab) ). In this paper, we precisely define this form of specification mining and show that its general form is NP-complete. We observe a great deal of regularity in the representation and tracking of all possible combinations of system components. This motivates us to introduce a symbolic algorithm, bas...

• Type: Conference
• Year: 2008
• Where: ICSE
• Authors: Mark Gabel, Zhendong Su
• Keywords: ICSE 2008, NSF CAREER Grant, NSF CCF Grant, NSF CyberTrust Grant, Software Engineering