Automatic Inference and Effective Application of Temporal Specifications

A Dissertation
Presented to
the faculty of the School of Engineering and Applied Science
University of Virginia


In Partial Fullment
of the requirements of the Degree
Doctor of Philosophy
Computer Science

by
Jinlin Yang

May 2007

Approved:

David E. Evans (Advisor)
Manuvir Das, Microsoft
Jack W. Davidson
Joanne B. Dugan
John C. Knight
Mary Lou Soffa (Chair)

Accepted by the School of Engineering and Applied Science:

James H. Aylor (Dean)

May 2007

Abstract

Software specifications are the foundation of many software development activities including maintenance, testing, and verification. However, specifications are rarely available for real systems. This dissertation describes a dynamic analysis technique to automatically infer program specifications. We focus on temporal specifications, an important category of specifications that constrain the order of occurrence of events. Our technique generates execution traces of the program by running a set of test cases and then analyzes the properties satisfied by traces using inference techniques and a set of predefined patterns. Our approach makes three contributions over previous work, focusing on enabling effective dynamic inference on large programs under realistic conditions. First, our inference algorithm scales well to large execution traces that have millions of events and thousands of distinct events. Second, our statistical inference algorithm can successfully infer property specifications from imperfect traces collected from buggy programs or using inadequate instrumentation tools. Third, our heuristics can effectively reduce the large number of properties inferred to a manageable set of mostly interesting properties. We implemented our dynamic analysis technique in a prototype tool called Perracotta. To evaluate the usefulness of dynamically inferred temporal properties, we applied Perracotta to aid program understanding, verification, and differencing. Results include inferring a 24-state finite state machine from the JBoss transaction manager that is consistent with the J2EE specification, inferring interesting API rules for the Windows kernel, and detecting a previously unknown deadlock bug in Windows by checking the inferred properties with the ESP verifier.

Complete Dissertation: PDF (144 pages)
Project: Perracotta


CS 655 David Evans - Publications
University of Virginia
Department of Computer Science
David Evans
evans@cs.virginia.edu