Abstract
TAPAAL is a new platform independent tool for modelling, simulation and verification of timed-arc Petri nets. TAPAAL provides a stand-alone editor and simulator, while the verification module translates timed-arc Petri net models into networks of timed automata and uses the UPPAAL engine for the automatic analysis.
We report on the status of the first release of TAPAAL (available at www.tapaal.net), on its new modelling features and we demonstrate the efficiency and modelling capabilities of the tool on a few examples.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Abdulla, P.A., Nylén, A.: Timed petri nets and BQOs. In: ICATPN 2001. LNCS, vol. 2075, pp. 53–70. Springer, Heidelberg (2001)
Bartlett, K.A., Scantlebury, R.A., Wilkinson, P.T.: A note on reliable full-duplex transmission over half-duplex links. Commun. ACM 12(5), 260–261 (1969)
Berthomieu, B., Ribet, P.-O., Vernadat, F.: The tool TINA — construction of abstract state spaces for Petri nets and time Petri nets. International Journal of Production Research 42(14), 2741–2756 (2004)
Bolognesi, T., Lucidi, F., Trigila, S.: From timed Petri nets to timed LOTOS. In: Proceedings of the IFIP WG 6.1 Tenth International Symposium on Protocol Specification, Testing and Verification, Ottawa, pp. 1–14 (1990)
Bouyer, P., Haddad, S., Reynier, P.-A.: Timed Petri nets and timed automata: On the discriminating power of Zeno sequences. Information and Computation 206(1), 73–107 (2008)
Gonzalez del Foyo, P.M., Silva, J.R.: Using time Petri nets for modelling and verification of timed constrained workflow systems. In: ABCM Symposium Series in Mechatronics. ABCM, vol. 3, pp. 471–478. ABCM - Brazilian Society of Mechanical Sciences and Engineering (2008)
Hanisch, H.M.: Analysis of place/transition nets with timed-arcs and its application to batch process control. In: Ajmone Marsan, M. (ed.) ICATPN 1993. LNCS, vol. 691, pp. 282–299. Springer, Heidelberg (1993)
Heitmann, F., Moldt, D., Mortensen, K.H., Rölke, H.: Petri nets tools database quick overview, http://www.informatik.uni-hamburg.de/TGI/PetriNets/tools/quick.html
Platform Independent Petri net Editor 2.5, http://pipe2.sourceforge.net
Jensen, K., Kristensen, L., Wells, L.: Coloured Petri nets and CPN tools for modelling and validation of concurrent systems. International Journal on Software Tools for Technology Transfer (STTT) 9(3), 213–254 (2007)
Lamport, L.: A fast mutual exclusion algorithm. ACM Transactions on Computer Systems 5(1), 1–11 (1987)
Petri Net Markup Language, http://www2.informatik.hu-berlin.de/top/pnml
Sifakis, J., Yovine, S.: Compositional specification of timed systems. In: Puech, C., Reischuk, R. (eds.) STACS 1996. LNCS, vol. 1046, pp. 347–359. Springer, Heidelberg (1996)
Srba, J.: Timed-arc Petri nets vs. networks of timed automata. In: Ciardo, G., Darondeau, P. (eds.) ICATPN 2005. LNCS, vol. 3536, pp. 385–402. Springer, Heidelberg (2005)
Srba, J.: Comparing the expressiveness of timed automata and timed extensions of Petri nets. In: Cassez, F., Jard, C. (eds.) FORMATS 2008. LNCS, vol. 5215, pp. 15–32. Springer, Heidelberg (2008)
UPPAAL, http://www.uppaal.com
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2009 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Byg, J., Jørgensen, K.Y., Srba, J. (2009). TAPAAL: Editor, Simulator and Verifier of Timed-Arc Petri Nets. In: Liu, Z., Ravn, A.P. (eds) Automated Technology for Verification and Analysis. ATVA 2009. Lecture Notes in Computer Science, vol 5799. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-04761-9_7
Download citation
DOI: https://doi.org/10.1007/978-3-642-04761-9_7
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-04760-2
Online ISBN: 978-3-642-04761-9
eBook Packages: Computer ScienceComputer Science (R0)