Mining Parametric Specifications

Chen, Feng; Lee, Choonghwan; Rosu, Grigore

Permalink

https://hdl.handle.net/2142/15109 Copy

Description

Title

Mining Parametric Specifications

Author(s)

• Chen, Feng
• Lee, Choonghwan
• Rosu, Grigore

Issue Date

2010-03-05

Keyword(s)

specification mining

Date of Ingest

2010-03-05T22:16:57Z

Abstract

"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."

Type of Resource

text

Genre of Resource

Technical Report

Language

en

Permalink

http://hdl.handle.net/2142/15109

Owning Collections