2.4.3 BSD License    
Editor and simulator of timed-arc Petri nets






TAPAAL is an utility that provides a standalone editor and simulator of timed-arc Petri nets. For running an automated verification, the user should first install the latest verion of UPPAAL development version.

TAPAAL is a tool for verification of Timed-Arc Petri Nets developed at Department of Computer Science at Aalborg University. It is based on the Petri Net drawing tool PIPE2.

Timed-Arc Petri Net (TAPN) is a time extension of the classical Petri net model (a commonly used graphical model of distributed computations introduced by Carl Adam Petri in his disseration in 1962). The time extension we consider allows for explicit treatment of real-time, which is associated with the tokens in the net (each tokens has its 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. In TAPAAL tool a furter extension of this model with invariants on places and with transport arcs (which are more expressive than for example previously considered read-arcs) is implemented.

The TAPAAL tools offers a graphical editor for drawing TAPN models, simulator for experimenting with the designed nets and a verification environment that allows to answer logical queries in a subset of CTL logic (essentially EF, EG, AF, AG formulae without nesting). It also allows to automatically check whether a given net is k-bounded for a given number k. The verification algorithm translates the TAPAAL queries into UPPAAL and relies on the UPPAAL engine.
Last updated on September 11th, 2013
TAPAAL - The main editor window of TAPAAL.TAPAAL - The improved query designer makes it super easy to create queries without a detailed knowledge of the concrete syntax. Queries can be by expert users edited also manually.TAPAAL - TAPAAL provides a standalone verification engine as well as verification via a translation to UPPAAL timed automata. The integrating within the TAPAAL GUI is seemless the answers are displayed directly in TAPAAL.TAPAAL - Simulation of a net behaviour can be done step by step, and error traces are loaded into the simulator allowing for an easy visualization of counter-examples.

0 User reviews so far.