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

TPNS webpage




Case Studies

Related Publications

TPNS Prototype


Timed Petri Nets can be used to model real time systems. Reachability analysis can be used to verify safety properties. Reachability analysis comes in two flavours: backward and forward. This package implements the forward approach. For full details about the theory, please refer to [1], [2] and [3].

The model we adopt is that of timed petri nets which are extension of petri nets with timing constraints. The prototype checks timed petri nets models against safety property.

Petri Nets


TPNS is free and open source. You can download the source code for free from below. Distribution is under the GNU General Public License (GPL). PFS runs on Linux and requires g++ 3.2.3.tpns.tar.gz


After extracting the archive, read the file "README.txt". In order to build the package, simply type:

This will generate several executables, two of them being of interest:

Example of usage: "./analyse < fischer"

There is no installation procedure, just run all files from any location you like.

Case studies

The "fischer" is an example showing how to analyse a timed Petri net modeling Fischer's protocol for mutual exclusion. Other examples are also provided:

Related Publications

Main papers:

Techincal report: [3]Forward Reachability Analysis of Timed Petri Nets. Parosh Aziz Abdulla, Johann Deneux, Pritha Mahata and Aletta NylÚn. IT database 2003. Link.

Valid XHTML 1.0 Transitional Valid CSS!
Contact us

This prototype was developed by Johann Deneux who finished his doctoral studies in 2006. The prototype is no longer maintained.

Here is a link to Johann's thesis