Dies ist ein Archiv des alten Softwaretechnik Lehrstuhls der Universität des Saarlandes. Es ist nicht länger aktuell.


Mining temporal specifications from object usage

Lehrstuhl für Softwaretechnik (Prof. Zeller)
Universität des Saarlandes – Informatik
Informatik Campus des Saarlandes
Campus E9 1 (CISPA)
66123 Saarbrücken
E-mail: zeller @ cs.uni-saarland.de
Telefon: +49 681 302-70970

Deutschsprachige Startseite Page d'acceuil en franšais English home page

Cebit 2010

We have released a web service that allows anyone to check his/her own code against the wisdom of 200 million lines of linux code. Check your code at checkmycode.org.


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.


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.


Contact us

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

Impressum Datenschutzerklärung

<webmaster@st.cs.uni-saarland.de> · http://www.st.cs.uni-saarland.de/models/tikanga/?lang=en · Stand: 2018-04-05 13:41