(about the name)
Perracotta is a dynamic analysis tool for automatically inferring temporal properties of a target program. It takes the program's execution traces as input and outputs a set of temporal properties it likely has. Figure 1 below shows how our approach works. This project has been inspired mainly by Michael Ernst's work on Daikon. Our work focuses on inferring sequencing invariants, whereas Daikon only detects value-based invariants.
There are several key challenges that have to be addressed to make our dynamic analysis effective. The first problem is to develop a set of property templates that capture commonly occurred properties. Our paper in PASTE 2004 proposed a hierarchy of templates.
To evaluate whether these property patterns are useful, we performed two experiments in two kinds of usage scenarios. First we applied Perracotta to help program evolution. Figure 2 shows how this works. The idea is to use Perracotta to infer temporal properties for several versions of a program, then compare the inferred properties across versions. We did experiments on six versions of OpenSSL. We found that our approach is promising in that it led us to discover some known bugs in earlier version and to expose some intended improvements applied to earlier versions. Our paper in ISSRE 2004 presents the detailed results of this experiment.
Our latest progress is to use Perracotta to support program verification. Figure 3 shows how this works. We use Perracotta to infer a set of temporal properties and then use a formal verification tool to check them. We assume our target programs are correct in most execution scenarios but might have bugs on some cold execution paths. As a result, we could assume that few executions of the target program represent its desirable behaviors. Our dynamic analysis computes an abstraction of such executions as the desired properties which are later checked by a verification tool (e.g. a model checker). We did experiments on Daisy, a prototype implementation of a Unix-like file system. It was used as the subject system at the Joint CAV/ISSTA Special Event on Specification, Verification, and Testing of Concurrent Software. We used Perracotta to infer a set of temporal properties and then checked them with Java PathFinder. The results are encouraging in that we were able to find a bug in Daisy and many subtle and undocumented temporal behaviors.
As an intern at Microsoft during summer 2005, Jinlin Yang applied Perracotta to infer temporal rules for the Windows kernel APIs. He improved Perracotta with several very important features: a scalable statistical inference algorithm that can handle imperfect traces, several heuristics for selecting interesting temporal properties, and a chaining method for constructing larger finite state machines out of a group of small ones. Perracotta successfully inferred 56 interesting properties (e.g., locking disciplines or resource allocation/deletion). Jinlin also used ESP to check the inferred properties and found many previously undetected bugs in Windows. In addition to the Windows experiments, we also applied Perracotta to infer a 24-state finite state machine for the transaction management module of the JBoss application server. These results will be published in our ICSE 2006 paper.
Jinlin Yang, Automatic Inference and Effective Application of Temporal Specifications, PhD Thesis, University of Virginia, May 2007.
Jinlin Yang, David Evans, Deepali Bhardwaj, Thirumalesh Bhat, Manuvir Das. Perracotta: Mining Temporal API Rules from Imperfect Traces. To appear in the 28th International Conference on Software Engineering (ICSE 2006). May 20-28, 2006, Shanghai, China. [PDF]
Jinlin Yang and David Evans. Automatically Discovering Temporal Properties for Program Verification. Technical Report, Department of Computer Science, University of Virginia, 2005. [PDF]
Jinlin Yang and David Evans. Automatically Inferring Temporal Properties for Program Evolution. Fifteenth IEEE International Symposium on Software Reliability Engineering (ISSRE 2004). November 2-5, 2004, Saint-Malo, France. [PDF, PS]
Jinlin Yang and David Evans. Dynamically Inferring Temporal Properties. In proceedings of ACM SIGPLAN-SIGSOFT Workshop on Program Analysis for Software Tools and Engineering (PASTE 2004). June 7-8, 2004, Washington DC, USA. [PDF, PS, PPT]
Perracotta: Mining Temporal API Rules from Imperfect Traces. Invited talk at the New Jersey Programming Language Seminar. University of Maryland at College Park. November 18, 2005. (Host: Dr. Michael Hicks and Dr. Jeff Foster)
Perracotta: Mining Temporal API Rules from Imperfect Traces. Invited talk at the CS851: Dependability System Seminar. Department of Computer Science, University of Virginia. September 28, 2005. (Host: Dr. Elisabeth Strunk)
Mining Windows Kernel API Rules. A special presentation about my summer intern project for Amitabh Srivastava, a Corporate Vice President of the Windows Core Operating System Development and a Microsoft Distinguished Engineer. Microsoft, Redmond, WA. August 2005.
Mining Windows Kernel API Rules. This is my end of internship talk. Microsoft Research, Redmond, WA. August 10, 2005. (Host: Dr. Jim Larus)
Automatically Inferring Temporal Properties for Windows Kernel. Invited talk for the Windows Core Developers Talk, a series of talks given to the Windows developers on every Friday. Microsoft Corporation, Redmond, WA. July 29, 2005. (Host: Dr. David Probert)
Dynamically Inferring Temporal Properties for Daisy. At the Joint CAV/ISSTA Special Event on Specification, Verification, and Testing of Concurrent Software. July 14, 2004. (Host: Dr. Shaz Qadeer) [PPT]
Perracotta is currently under active development. We are happy to release it. Please contact Jinlin Yang if you are interested in giving Perracotta a try.