TIKANGA
Mining temporal specifications from object usage

Cebit 2010

Introduction

A caller must satisfy the callee's precondition—that is, reach a state in which the callee may be called. Preconditions describe the state that needs to be reached, but not how to reach it.

Our tool, Tikanga (meaning "correct procedure" in Mãori), combines static analysis with model checking to mine Computation Tree Logic (CTL) formulas that describe the operations a parameter goes through. We call these temporal specifications operational preconditions, and Tikanga can both mine them as well as check the program for their violations.

How Tikanga works

The process, by which Tikanga mines operational preconditions and finds their violations consists of four steps:

• Model mining: Tikanga transforms the program into a set of Kripke structures that reflect the way objects in the program are being used. Part of this transformation is performing dataflow analysis to create so-called object usage models, and we use our own tool, JADET for this purpose.
• Extracting CTL specifications: For each Kripke structure, Tikanga generates a set of CTL formulas stemming from user-given templates. These formulas are model checked to determine which ones hold. They describe the way a specific object is used before being passed to a specific method as an argument.
• Creating operational preconditions: Tikanga looks for sets of CTL formulas that are common to many objects passed as actual arguments. Each such set forms an operational precondition of the formal parameter.
• Detecting violations: Tikanga looks through all the objects used as actual arguments and identifies those that violate the operational preconditions found. These violations are reported to the user; violated CTL formulas suggest a potential fix.

For more details on the whole process, consult our publication.

Effectiveness

We have applied Tikanga to six open-source projects and found that it was able to find problems with all of them. Its effectiveness varied from 16% to 80%, depending on the project. In particular, Tikanga managed to find in total 14 defects in the projects we have analyzed. For more details on the results, consult our publication.

Publications

• Andrzej Wasylkowski, Andreas Zeller: Mining temporal specifications from object usage. 24th IEEE/ACM International Conference on Automated Software Engineering, Auckland, New Zealand, November 2009.
• Natalie Gruska, Andrzej Wasylkowski, Andreas Zeller Learning from 6,000 Projects: Lightweight Cross-Project Anomaly Detection, Technical Report, 2010

Contact us

Below you can find links to people working on mining temporal specifications. Please contact us for questions, rants, and raves.

• Andrzej Wasylkowski
• Andreas Zeller

Impressum ● Datenschutzerklärung