TAPAAL Model Checker
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 it is available for Linux, Windows and Mac OS X platforms.
Timed-Arc Petri Net is a time extension of the classical Petri net model. The time extension considered in TAPN allows for explicit treatment of real-time, which is associated with the tokens in the net 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 further extension of this model with age invariants with transport arcs and with inhibitor arcs is implemented.
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 formulated in a subset of CTL logic. It also allows the user to check whether a given net is k-bounded for a given number k. TAPAAL is equipped with its own verification engines distributed together with TAPAAL. Optionally, the user can automatically translate TAPAAL models
into UPPAAL and rely on the UPPAAL verification engine.