A Sound and Complete Specification Miner
David Lo, (Advisor) Siau-Cheng Khoo
Awarded 2nd position
ACM SIGPLAN PLDI'07, San Diego, 10-13 June 2007
Student Research Competition (Graduate category)
Abstract
Improper management of software evolution, compounded by imprecise, and changing requirements, along with the ``short time to market'' requirement, commonly leads to a lack of up-to-date specifications. This can result in software that is characterized by bugs, anomalies and even security threats. Software specification mining is a new technique to address this concern by inferring specifications automatically from program execution traces.
In this paper, we propose a novel technique to mine a sound, complete and non-redundant set of multi-event rules expressed in linear temporal logic from a set of program execution traces. The extracted temporal rules shed light on the behavior a system exhibits. Also, since the rules are formalized in temporal logic, they can be easily inputted to existing model checkers or other formal analysis toolkits to discover bugs and anomalies. A framework composed of: program instrumentation, trace collection & abstraction, rule mining and rule post-processing is proposed.
Case studies performed on various components of JBoss Application Server show how the mined rules shed light on the protocols that the code obey; hence aiding program comprehension. A controlled experiment performed on a simple CVS application built on top of the Jakarta Commons Net library shows the applicability of the method for verification and bug-detection purpose.