UPPSALA UNIVERSITET : Institutionen för Informationsteknologi : Algorithmic Program Verification Group
Uppsala universitet

UNDIP webpage

Introduction

Download

Instruction

Case Studies

Related Publications

UNDIP Prototype

Introduction

UNDIP stands for Unbounded Distributed Parameterized systems. UNDIP is a prototype for the verification of safety properties on distributed or non-distributed parameterized systems with potentially unbounded data domain. The prototype performs backward reachability on an over-approximation of the induced transition system. Difference bound matrices are used to define and manipulate the constraints on integer variables.

A parameterized system consists of an arbitrary number of identical state machines running in parallel. Each state machine operates on a finite number of unbounded variables, and communicate with each other machine through shared variables or channels. Such systems have therefore two sources of infinity: the number of processes and the domain of the manipulated data.

UNDIP can be regarded as an extension of PFS to the case where the data domain of the manipulated variables is unbounded, and where the atomic global transition can be replaced by refined non-atomic protocols. Many interesting mutual exclusion algorithms fit into this modeling framework.

Download

UNDIP is free and open source. You can download the source code for free from below. Distribution is under the GNU General Public License (GPL). We run UNDIP on Linux fc6(2.6) undip.tar.gz.

Instructions

In a Linux console, extract the file, cd to the directory, type ./configure, then type make. Check the "README" and the examples to get inspired.

Case studies

This is a (non exhaustive) list of the mutual exclusion algorithms we verified with UNDIP. Assuming we start from a set of constraints "B" where all constraints have the same cardinal "Card" (i.e. number of processes constrained by the constraints). We insert new processes to the generated constraints only once we reach a fixpoint within the set of constraints with the same cardinal "Card". The number of iterations corresponds to the sum of the aggregation of the number iterations for each cardinal.
Models Iterations Constraints Time (sec)
Burns alg. 16 40 < 0.05
Szymanski alg. 61 5085 85
Dijkstra alg. 18 89 < 0.05
Java Meta-Lock alg. 22 376 3.2
Illinois cache prot. 10 46 < 0.05
Firefly cache prot. 14 31 0.1
Futurebus cache prot. 10 46 0.1
German cache prot. 34 10492 232
Bakery alg. 11 29 < 0.05
Bakery (buggy(*)) alg. 7 67 < 0.05
Bakery (all interleavings) alg. 13 42 0.1
Distr. Lamport alg. 30 4676 85
Distr. Ricart & Agrawala alg. 32 1205 13
(*) A Bug was introduced on purpose. A counter-example (trace) is returned by the prototype.

Related Publications

Main papers: Parameterized Verification of Infinite-state Processes with Global Conditions. Parosh Aziz Abdulla, Giorgio Delzanno, and Ahmed Rezine. In Proc. CAV 2007, 19th International Conference on Computer Aided Verification.PDF, PS.
Handling Parameterized Systems with Non-Atomic Global Conditions. Parosh Aziz Abdulla, Noomene Ben Henda, Giorgio Delzanno, and Ahmed Rezine. In Proc. VMCAI 2008, Verification, Model Checking and Abstract Interpretation.PDF, PS.

Technical report: Parameterized Verification of Infinite-state Processes with Global Conditions. Parosh Aziz Abdulla, Giorgio Delzanno, and Ahmed Rezine. IT-database 2007 Link .

Valid XHTML 1.0 Transitional Valid CSS!
Contact us
Ahmed Rezine

Email:

rezine.ahmed@it.uu.se

URL:

http://user.it.uu.se/~rahmed