TPNS webpage

Introduction

Download

Instruction

Case Studies

Related Publications

TPNS Prototype

Introdution

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.

Download

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

Instructions

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

• ./configure
• make
• make clean

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

• "test" is an interactive program designed to play with dlgs.
• "analyse" performs forward reachability analysis of a timed Petri net.

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:

• fischerext: an extension of Fischer's protocol.
• mutex2: another mutual exclusion protocol, from R. Alur and G. Taubenfeld: Results about fast mutual exclusion. In Proc. 13th IEEE Real-Time Systems Symposium, pages 12-21, 1992.

Related Publications

Main papers:

• [1]Forward Reachability Analysis of Timed Petri Nets. Parosh Aziz Abdulla, Johann Deneux, Pritha Mahata and Aletta Nylén. In Proc. of Formats-FTRTFT '04. PS.
• [2]Timed Petri Nets and BQOs. Parosh Aziz Abdulla and Aletta Nylén. In Proc. of ICATPN'2001, 22nd Int. Conf. on application and theory of Petri nets. PDF.

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.