TAPAAL

Overview

Entry last updated: 2009/9/23
Entry last validated: 2009/9/23

Tool homepage: http://www.tapaal.net

Tool availability: Free of charge

Tool Features

Petri Nets Supported (see also help on terminology)

Place/Transition Nets
Petri Nets with Time

Components (see also help on terminology)

Graphical Editor
Token Game Animation
Advanced Performance Analysis
Interchange File Format

Environments

Sun, SunOS
HP, HP-UX
Silicon Graphics, IRIX
PC, Linux
PC, MS DOS
PC, OS/2
PC, MS Windows 95
PC, MS Windows 98
PC, MS Windows NT
PC, MS Windows 2000
PC, MS Windows XP
Macintosh, Mac OS
Macintosh, Mac OS X
Java

Tool Description

TAPAAL is a tool for modelling, simulation and verification of Timed-Arc Petri nets developed at Department of Computer Science at AALborg University in Denmark and available for Linux, Windows and Mac OS X platforms.

Timed-Arc Petri Net (TAPN) is a time extension of the classical Petri net model where tokens in the net carry their own age and arcs from places to transitions are labelled by time intervals that restrict the age of tokens that can be used in order to fire the respective transition.

The TAPAAL tool offers a graphical editor for drawing TAPN models, simulator for experimenting with the designed nets and a verification environment that automatically answers logical queries. The verification algorithm translates the TAPAAL queries into UPPAAL ones and relies on the UPPAAL verification engine.

Contact Information

Jiri Srba
Department of Computer Science, Aalborg University
Selma Lagerlofs Vej 300
9220 Aalborg
Denmark

Phone:  +45 99 40 98 51 
Fax:    +45 99 40 97 98 
E-mail: tapaal@cs.aau.dk

Other Remarks

The verification module uses the UPPAAL engine and can run on Win/Linux/MAC OS X platforms. UPPAAL is free for academic use but not for commercial use.

The maintainers of this page