University of Illinois Urbana-Champaign

Mining Parametric Specifications

Chen, Feng; Lee, Choonghwan; Rosu, Grigore

Content Files
chen-lee-rosu-2010-issta-techreport.pdf

Permalink

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

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

Research and Tech Reports - Computer Science PRIMARY