Expand, Enlarge and Check

Verification Group -- Université Libre de Bruxelles


This web page offers additional material related to the "Expand, Enlarge and Check" approach to decide the coverability problem of WSTS.

Content of the page:

Papers available for download

[Back to top]

Set of examples used in the experiments

Update (August, 18, 2010) ! The kanban example that was formerly present on this page was not the same as the one reported in the CAV 05 paper. The two versions are now present on the page (see bounded and unbounded PNs) The leabasicapproach example was incorrectly classified as Petri net with Transfer arcs. Many thanks to Tim Strazny for pointing this out.

For each example, we mention the size (number of places and number of transitions) and give a short description. The specification files are available for download. They describe the examples under the form of counter machines: a set of integer variables and a set of transitions that modify the value of the counters. The formalism used to describe the examples should be self-explanatory. The property that is verified (i.e. the reachability of a given upward-closed set of values of the counters) is also given in the file.

We study three category of examples:

Bounded Petri nets

Lamport
#Places:11 #Transitions:9 [Download]
The mutual exclusion protocol by Leslie Lamport, with two threads.

newDekker
#Places:16 #Transitions:14 [Download]
The Dekker mutual exclusion protocol, with two threads

newRTP
#Places:9 #Transitions:12 [Download]
A very basic communication protocol

Peterson
#Places:14 #Transitions:12 [Download]
The Peterson mutual exclusion protocol, with two threads

Read-Write
#Places:13 #Transitions:9 [Download]
A simple "reader/writer" mutual exclusion example.

Kanban (bounded version)
#Places:16 #Transitions:16 [Download]
A concurrent production system. This version of the file has been used in the testsuite of the CAV05 paper. [Petri net]

LeaBasicApproach
#Places:16 #Transitions:12 [Download]
An example of counting abstraction of a Java program from Doug Lea, Concurrent Programming in Java (TM): Design, Principles and Patterns, second edition, Adison Wesley, 2000

[Back to top]

Petri nets

basicME
#Places:5 #Transitions:4 [Download]
A basic mutual exclusion protocol, with an unbound number of threads. The Petri net can be found as Fig. 1 of Giorgio Delzanno, Jean-François Raskin an Laurent Van Begin, Attacking Symbolic State Explosion, in Proc. CAV'01, LNCS 2102. [Download this paper]

CSM
#Places:14 #Transitions:13 [Download]
This example describes a concurrent production system. It is taken from Fig. 76 of M. Ajmone Marsan, G. Balbo, G. Conte, S. Donatelli, and G. Franceschinis, Modelling with generalized stochastic Petri nets, John Wiley Series in Parallel Computing - Chichester, 1995. [Petri net]

FMS
#Places:22 #Transitions:20 [Download]
A concurrent production system. [Petri net]

Kanban (unbounded version)
#Places:16 #Transitions:16 [Download]
A concurrent production system. This is not the example that occurs in the testsuite of the CAV05 paper (see bounded version instead). The only difference is in the initial marking. [Petri net]

Mesh2x2
#Places:32 #Transitions:32 [Download]
This example describes a system in which a set of processors share the execution of various processes. It is taken from Fig. 130 of M. Ajmone Marsan, G. Balbo, G. Conte, S. Donatelli, and G. Franceschinis, Modelling with generalized stochastic Petri nets, John Wiley Series in Parallel Computing - Chichester, 1995. [Petri net]

Mesh3x2
#Places:52 #Transitions:54 [Download]
This example is an extension of the former one.

Multipoll
#Places:18 #Transitions:21 [Download]
This example comes from Andrew S. Miner and Gianfranco Ciardo, Efficient Reachability Set Generation and Storage Using Decision Diagrams, in Proc. ICATPN'99, LNCS 1639. It describes a concurrent production system. [Petri net]

PNCSAcover
#Places:31 #Transitions:36 [Download]
This is the PNCSA protocol as described in example 4.7 of Alain Finkel, The minimal coverability graph for Petri nets, Proc. APN'93, LNCS 674

[Back to top]

Petri nets with transfer arcs

CSMBroad
#Places:13 #Transitions:8 [Download]
The Control Server Monitor. A consistency protocol with atomic syncronization actions. [Image]

MOESI
#Places:9 #Transitions:11 [Download]
A cache coherency protocol.

German
#Places:12 #Transitions:8 [Download]
Steve German's cache coherency protocol.

Java
#Places:44 #Transitions:37 [Download]
The counting abstraction of a Consumer/Producer multithread Java program, with two different kinds of consumers and producers. Buggy. [Java source code]

Javasanserreur
#Places:44 #Transitions:38 [Download]
The counting abstraction of a Consumer/Producer multithread Java program. Same as the previous example but without the bug. [Java source code]

ConsProd
#Places:18 #Transitions:14 [Download]
The counting abstraction of a Consumer/Producer multithreaded Java Program, taken from the [Sun tutorial].

ConsProd2
#Places:18 #Transitions:14 [Download]
Same as the former example, with another property.

DelegateBuffer
#Places:50 #Transitions:52 [Download]
An example of counting abstraction of a Java program from Doug Lea, Concurrent Programming in Java (TM): Design, Principles and Patterns, second edition, Adison Wesley, 2000

ExempleLea
#Places:48 #Transitions:42 [Download]
An example of counting abstraction of a Java program from Doug Lea, Concurrent Programming in Java (TM): Design, Principles and Patterns, second edition, Adison Wesley, 2000

QueuedBusyFlag
#Places:80 #Transitions:104 [Download]
An example of counting abstraction of a Java program from Doug Lea, Concurrent Programming in Java (TM): Design, Principles and Patterns, second edition, Adison Wesley, 2000

SimpleJavaExample
#Places:32 #Transitions:28 [Download]
An example of Java program where two threads share an object describing a point in 2-dimensional space, and increment or decrement its coordinates. [Java source code]

TransThesis
#Places:90 #Transitions:117 [Download]
An example of conting abstraction of a Java program from Doug Lea, Concurrent Programming in Java (TM): Design, Principles and Patterns, second edition, Adison Wesley, 2000

EFM
#Places:6 #Transitions:5 [Download]
The Esparza-Finkel-Mayr counter machine. Can be found at Fig. 2 of Javier Esparza, Alain Finkel, Richard Mayr, On the verification of broadcast protocols, in Proc. LICS'99. IEEE Computer Society, 352--359.

[Back to top]

Experimental results

This page reports on the experiments we have carried out in order to assess the pratical usability of Expand, Enlarge and Check.
[Back to top]

Download

The EEC algorithm for Petri nets only has been implemented in the mist tool.

Warning ! Do not run the EEC implementation of the mist2 tool on the examples that are not Petri nets (i.e. Petri nets with transfers or broadcast protocols...), since the tool will not detect that your source file is not adequate, will not produce any warning, and will produce incorrect results !!

[Back to top]

Links

[Back to top]
Mer aoû 18 16:56:34 CEST 2010

Statistics