Index of /~johannd/tpn

      Name                    Last modified       Size  Description


[DIR] Parent Directory        27-Aug-2007 21:28      -  
[TXT] README.txt              02-Sep-2004 14:22     2k  
[DIR] html/                   21-Oct-2002 17:16      -  
[   ] tpns-20030924-patch1..> 02-Sep-2004 14:27   130k  

Forward reachability analysis of timed Petri nets.

0. Summary

This software package is distributed under the GNU GPL. See COPYING for more
details.
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:

Parosh Aziz Abdulla, Johann Deneux, Pritha Mahata and Aletta Nylén.
"Forward Reachability Analysis of Timed Petri Nets".
To appear in Proc. Formats-FTRTFT '04.
(available at: http://user.it.uu.se/~pritha/Papers/tpn.ps.gz)

Parosh Aziz Abdulla and Aletta Nylén.
"Timed Petri Nets and BQOs".
Proc. ICATPN'2001, 22nd Int. Conf. on application and theory of Petri nets
(available at: http://user.it.uu.se/~parosh/publications/tpn.ps)

1. Installation

Requirements: g++ 3.2.3.

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.

2. Running

% ./analyse <fischer

"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

3. Contact information

You can contact the author, Johann Deneux <johann.deneux@it.uu.se> for any
question reguarding this software.