Mining Parametric Specifications

Mining formal specifications from program executions has numerous applications in software analysis, from program understanding and modeling to testing and bug detection. Parametric specifications carry parameters that are bound to concrete values at runtime. They are useful for specifying system behaviors involving multiple components. Runtime monitoring of parametric specifications is relatively well-understood, with several performant runtime monitoring systems available. The main challenge underlying such parametric monitoring systems is to slice parametric execution traces into smaller, non-parametric traces, each relevant for a particular parameter instance; then each of the trace slices is monitored against a non-parametric monitor. This paper presents a novel technique to automatically mine parametric specifications from execution traces, which builds upon the observation that there is an inherent duality between parametric specification monitoring and parametric specification mining: they both rely on an online parametric trace slicing process, followed either by monitoring the resulting trace slices against given specifications in the first case, or by inferring the specifications that best explain the observed trace slices in the second case. A blind use of off-the-shelf parametric trace slicing techniques from monitoring leads to inefficient and "noisy" slicers for mining. The first contribution of this paper is a mining-specific parametric trace slicer, which makes slicing feasible and precise for mining. The obtained trace slices can then be passed to any non-parametric property learner. A blind use of the off-the-shelf Probabilistic Finite State Automata (PFSA) learner may lead to over-generalized specifications. The second contribution of this paper is a refinement of the PFSA learner that results in accurate specification mining. The presented technique was implemented in a tool for Java and applied to a number of real-world programs, including libraries and popular open source packages, with encouraging results: many meaningful specifications were mined; some revealed tricky bugs in open source programs.unpublishednot peer reviewe