IDEALS Home University of Illinois at Urbana-Champaign logo The Alma Mater The Main Quad

Mining Parametric Specifications

Show full item record

Bookmark or cite this item: http://hdl.handle.net/2142/15109

Files in this item

File Description Format
PDF chen-lee-rosu-2010-issta-techreport.pdf (919KB) (no description provided) PDF
Title: Mining Parametric Specifications
Author(s): Chen, Feng; Lee, Choonghwan; Rosu, Grigore
Subject(s): specification mining
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.
Issue Date: 2010-03-05
Genre: Technical Report
Type: Text
Language: English
URI: http://hdl.handle.net/2142/15109
Publication Status: unpublished
Peer Reviewed: not peer reviewed
Date Available in IDEALS: 2010-03-05
 

This item appears in the following Collection(s)

Show full item record

Item Statistics

  • Total Downloads: 125
  • Downloads this Month: 2
  • Downloads Today: 0

Browse

My Account

Information

Access Key