♠ SPADE
Verification of Multithreaded Dynamic and Recursive Programs

• Introduction
• Examples
• Credits
• Download
• References

SPADE ♠ is a software model-checking tool that allows the analysis of boolean programs presenting several complex features such as parallelism, communication between parallel processes (with rendez-vous), dynamic process creation and recursion. SPADE ♠ checks safety properties of these programs by computing (and refining) abstractions of the sets of the program execution paths that violate the property. Such programs are modeled using Synchronous PAD Systems (SPAD). Since property checking is undecidable for programs presenting all the features mentioned above, SPADE ♠ computes abstractions (over-approximations) of execution paths between the initial and bad configurations of the program. If the computed approximation is too coarse, SPADE ♠ can refine it using more precise abstractions. This refinement process may not converge (due to the undecidability of the problem). In case of convergence, it can either find a bug in the program, or certify that the program is correct.

We have applied SPADE ♠ to different case studies. Our results are encouraging and are reported in [GST07]. In particular, we were able to automatically find two bugs in two versions of a Windows NT Bluetooth driver. Earlier verification efforts of these versions were not completely automatic since they necessitate the guess of the number of processes for which the bugs occur. Whereas with SPADE ♠, the verification process was done in a completely automatic manner. Indeed, we don't need to make any guess since the tool handles dynamic creation of processes.

Synchronous PAD Systems (SPAD for short) [Tou05] is a finite set of rules of the form t -a-> t' where a is a synchronisation action, t and t' are terms built up from the idle process ("0"), a finite set of process variables ("X"), sequential composition ("·"), and asynchronous parallel composition ("||"). Each action a has its corresponding co-action ã. Examples of programs modeled using SPAD can be found in [Tou05] and in the distribution of the SPADE ♠ tool.

SPADE ♠ deals with rechability queries for SPAD models. More precisely, given two (possibly infinite) sets of configurations Init and Bad, the problem is to know whether the set of bad configurations Bad can be reached from the initial configurations Init. The approach implemented in SPADE ♠ consists in computing abstractions of the execution path language that leads form Init to Bad and iteratively refining these abstractions (see [Tou05] for the details). The technique is based on:

1. The representation of the sets of configurations with binary tree automata,
2. The use of these automata to compute a set of constraints whose least fixpoint characterizes the set of execution paths of the program, and
3. The resolution of this set of constraints in an abstract domain.

Several examples of programs that were verified using SPADE ♠ are available in the package (input directory). Among these example, we can mention:

• Two versions of the Bluetooth driver program,
• A multithreaded program that uses concurrently methods of the class java.util.Vector from the Java Standard Collection Framework
• A program that handles an arbitrary number of concurrent insertions on a binary search tree.

SPADE ♠ is written, debugged, maintained and improved by Gael Patin, Mihaela Sighireanu and Tayssir Touili.

You can download the SPADE ♠ tool via HTTP.

For installing SPADE ♠ you need:

• Ocaml 3.04 or greater.
• make for recompiling under Unix.
• Timbuk library (Copyright 2000-2003 Thomas Genet), see http://www.irisa.fr/lande/genet/timbuk/.

[GST07] G. Patin, M. Sighireanu and T. Touili. SPADE: Verification of Multithreaded Dynamic and Recursive Programs. Submitted for publication. January 2007.

[Tou05] T. Touili. Dealing with communication for dynamic multithreaded recursive programs. Invited paper. In Proc. of VISSAS'05

Last updated: Fri Feb 2. 15:37:21 CET 2007