• Introduction
• Features
• Screenshots
• Download
• Documentation
• About

TAPAAL tool provides

• a graphical GUI for drawing extended timed-arc Petri nets,
• a simulator,
• an efficient verifier, and
• a translation module using the UPPAAL engine at the back end.

The standard model of timed-arc Petri nets is extended with

• component-based design,
• age invariants,
• transport arcs, and
• inhibitor arcs.

This extended model offers more expressive power than the standard timed-arc Petri net model [1,2,8] and such extensions are very convenient for modelling purposes. Invariants allow to model correctly hard-deadlines and transport arcs are suitable for describing for example workflow processes as with this extension a precise tracking of age of a token is possible throughout the computation of the net. The user is allowed to verify even unbounded nets. In this case the tool provides a suitable underapproximation technique as well as an automatic check whether a designed net is bounded or not for a given number of tokens that can at most appear in the net during any computation.

To the best of our knowledge, TAPAAL is the first publicly available  and maintained tool for verification of timed-arc Petri nets. Other tools for untimed Petri nets and timed Petri nets where time features are added e.g. to transitions can be found for example here.

Implementation details:

The GUI of TAPAAL is based on an open source project called PIPE and extends PIPE version 2.5 with the extra features for modelling of timed-arc Petri nets. It is implemented in Java and JRE 6.0 is required in order to run the GUI. It is released under the Open Software Licence 3.0.

The translation from Petri nets to UPPAAL timed automata is also implemented in Java and all data structures and algorithms for the translation were developed in the TAPAAL project under the BSD License.

TAPAAL's verification engine is now a part of the TAPAAL distribution package and it is licensed under GLP v2 license: http://www.gnu.org/licenses/gpl-2.0.txt.

The verification engine UPPAAL is not a part of the project and it is available under a different license (for details visit uppaal.com) but all together the TAPAAL tool including the verification part is FREE for non-commercial applications in academia and for private persons. For commercial use the company has to first obtain a valid commercial license for UPPAAL, but the editor and simulatior are free to use.

Literature:

The TAPN model was first used in

[1] T. Bolognesi and F. Lucidi and S. Trigila: From Timed Petri Nets to Timed LOTOS published in Proceedings of the IFIP WG 6.1 Tenth International Symposium on Protocol Specification, Testing and Verification in 1990 by North-Holland, Amsterdam, pages 1-14,

and

[2] H.M. Hanisch: Analysis of Place/Transition Nets with Timed-Arcs and its Application to Batch Process Control published in Proceedings of the 14th International Conference on Application and Theory of Petri Nets (ICATPN'93) in 1993, LNCS volume 691, pages 282-299, 1993.

A recent overview of different timed extensions of Petri nets and automata is available in

[3] J. Srba: Comparing the Expressiveness of Timed Automata and Timed Extensions of Petri Nets published in Proceedings of 6th International Conference on Formal Modelling and Analysis of Timed Systems (FORMATS'08), pages 15-32, volume 5215 of LNCS, Springer-Verlag, 2008.

A translation from 1-safe TAPN to networks of timed automata was suggested in

[4] J. Srba: Timed-Arc Petri Nets vs. Networks of Timed Automata  published in Proceedings of 26th International Conference on Application and Theory of Petri Nets (ICATPN'05), pages 385-402, volume 3536 of LNCS, Springer-Verlag, 2005

and it was later extended to bounded nets in

[5] P. Bouyer, S. Haddad and P.-A. Reynier: Timed Petri nets and timed automata: On the discriminating power of zeno sequences published in Information and Computation, volume 206:1, 2008, pages 73-107.

Both [4] and [5] suggest the use of read/test-arcs because it adds a descriptive power to the nets. In TAPAAL tool even more general transport arcs are implemented and they allow to model read/test-arcs in a straightforward manner.

Finally, we list papers related to the TAPAAL tool.

[6] J. Byg, K.Y. Joergensen and J. Srba: TAPAAL: Editor, Simulator and Verifier of Timed-Arc Petri Nets, Proceedings of the 7th International Symposium on Automated Technology for Verification and Analysis (ATVA'09), volume 5799 of LNCS, pages 84-89, Springer-Verlag. [PDF]

[7] J. Byg, K.Y. Joergensen and J. Srba: An Efficient Translation of Timed-Arc Petri Nets to Networks of Timed-Automata, Proceedings of the 11th International Conference on Formal Engineering Methods (ICFEM'09), LNCS 5885, pages 698--716, Springer-Verlag. [PDF]

[8]  L. Jacobsen, M. Jacobsen and M.H. Møller: Undecidability of Coverability and Boundedness for Timed-Arc Petri Nets with Invariatnts, MEMICS'09. [PDF]

[9]  L. Jacobsen, M. Jacobsen, M.H. Møller and J. Srba: A Framework for Relating Timed Transition Systems and Preserving TCTL Model, EPEW'10. [PDF]

[10]   L. Jacobsen, M. Jacobsen and M.H. Møller: Modelling and Verification of Timed-Arc Petri Nets, Master Thesis, Aalborg University, Department of Computer Science, 2010. [PDF]

[11] L. Jacobsen, M. Jacobsen, M.H. Møller and J. Srba: Verification of Timed-Arc Petri Nets, Invited presentation at SOFSEM'11. [PDF]

 

An overview of several case studies (MPEG-2 encoding algorithm, brain memory modelling, TPAL specifications) modelled in the TAPN model is available in [3].