Details about TAPAAL
TAPAAL tool provides
- a graphical GUI for drawing P/T nets (with PNML import/export) and extended timed-arc Petri nets,
- a simulator,
- a timed workflow net analyzer,
- stand-alone efficient verifiers, 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,
- urgent transitions,
- 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.
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 or 7.0 is required in order to run the GUI. It is released under the Open Software Licence 3.0.
The TAPN model was first used in
 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,
 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
 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
 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
 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  and  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.
 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]
 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. [PDFUndecidability of Coverability and Boundedness for Timed-Arc Petri Nets with Invariants, MEMICS'09. [PDF A Framework for Relating Timed Transition Systems and Preserving TCTL Model, EPEW'10. [PDFModelling and Verification of Timed-Arc Petri Nets, Master Thesis, Aalborg University, Department of Computer Science, 2010. [PDF Verification of Timed-Arc Petri Nets, Invited presentation at SOFSEM'11. [PDF TAPAAL 2.0: Integrated Development Environment for Timed-Arc Petri Nets, TACAS'12. [PDF]
 C. Bertolini, Zh. Lin and J. Srba: Verification of Timed Healthcare Workflows Using Component Timed-Arc Petri Nets, FHIES'12. [PDFVerification of Liveness Properties on Closed Timed-Arc Petri Nets, MEMICS'12. [PDF]
 A. David, L. Jacobsen, M. Jacobsen and J. Srba: A Forward Reachability Algorithm for Bounded Timed-Arc Petri Nets, SSV'12. [PDFMemory Efficient Data Structures for Explicit Verification of Timed Systems, NFM'14. [PDFSoundness of Timed-Arc Workflow Nets, Petri Nets'14. [PDF]
 S.V. Birch, T.S. Jacobsen, J.J. Jensen, Ch. Moesgaard, N.N. Samuelsen and J. Srba: Interval Abstraction Refinement for Model Checking of Timed-Arc Petri Nets, FORMATS'14. [PDF]
An overview of several case studies (MPEG-2 encoding algorithm, brain memory modelling, TPAL specifications) modelled in the TAPN model is available in .