TAPAAL is a tool for modelling,

simulation A simulation is an imitative representation of a process or system that could exist in the real world. In this broad sense, simulation can often be used interchangeably with model. Sometimes a clear distinction between the two terms is made, in ...

and verification of Timed-Arc Petri nets developed at Department of Computer Science at

Aalborg University Aalborg University (AAU) is an international public university with campuses in Aalborg, Esbjerg, and Copenhagen, Denmark. Founded in 1974, the university awards bachelor's degrees, master's degrees, and PhD degrees in a wide variety of subje ...

in Denmark and it is available for Linux, Windows and Mac OS X platforms. Timed-Arc Petri Net (TAPN) is a time extension of the classical

Petri net A Petri net, also known as a place/transition net (PT net), is one of several mathematical modeling languages for the description of distributed systems. It is a class of discrete event dynamic system. A Petri net is a directed bipartite graph t ...

model (a commonly used graphical model of distributed computations introduced by

Carl Adam Petri Carl Adam Petri (12 July 1926 in Leipzig – 2 July 2010 in Siegburg) was a German mathematician and computer scientist. Life and work Petri created his major scientific contribution, the concept of the Petri net, in 1939 at the age of 13, for ...

in his dissertation in 1962). The time extension considered in TAPN 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 further extension of this model with age invariants with transport arcs (which are more expressive than for example previously considered read-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 (essentially EF, EG, AF, AG formulae without nesting). 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 (one for continuous time and one for discrete time ). Optionally, the user can automatically translate TAPAAL models into UPPAAL and rely on the UPPAAL verification engine. TAPAAL 2

External links

TAPAAL website, downloadDES unit, Deptment of Computer Science, Aalborg University, DenmarkTAPAAL: Editor, Simulator and Verifier of Timed-Arc Petri Nets by J. Byg, K.Y. Jørgensen and J. Srba, ATVA'09, SpringerAn Efficient Translation of Timed-Arc Petri Nets to Networks of Timed Automata by J. Byg, K.Y. Jørgensen and J. Srba, ICFEM'09, SpringerA Framework for Relating Timed Transition Systems and Preserving TCTL Model Checking by L. Jacobsen, M. Jacobsen, M.H. Møller and J. Srba, EPEW'10, SpringerVerification of Timed-Arc Petri Nets by L. Jacobsen, M. Jacobsen, M.H. Møller and J. Srba, SOFSEM'11, Springer

References

Model checkers {{formalmethods-stub