Perracotta (about the name)

Introduction    People    Publications    Talks    Tool Distribution
 

Introduction

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 are published in our ICSE 2006 paper.

People

Faculty:

    David Evans

Graduate student:

    Jinlin Yang

Undergraduate student:

    Edward Mitchell

Publications

Talks

Tool Distribution

The Perracotta source code is available at: https://github.com/ModelInference/perracotta

Much thanks to Caroline Lemieux for setting up the github repository and updating the code to work with Java 1.8.

David Evans
University of Virginia
Department of Computer Science
 evans@virginia.edu