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