Skip to main content
SpringerLink
Log in

PetriDotNet 1.5: Extensible Petri Net Editor and Analyser for Education and Research

  • Conference paper
  • First Online:
Book cover Application and Theory of Petri Nets and Concurrency (PETRI NETS 2016)

Part of the book series: Lecture Notes in Computer Science ((LNTCS,volume 9698))

Abstract

PetriDotNet is an extensible Petri net editor and analysis tool originally developed to support the education of formal methods. The ease of use and simple extensibility fostered more and more algorithmic developments. Thanks to the continuous interest of developers (especially M.Sc. and Ph.D. students who choose PetriDotNet as the framework of their thesis project), by now PetriDotNet became an analysis platform, providing various cutting-edge model checking algorithms and stochastic analysis algorithms. As a result, industrial application of the tool also emerged in recent years. In this paper we overview the main features and the architecture of PetriDotNet, and compare it with other available tools.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution

Institutional subscriptions

Notes

  1. 1.

    http://www.davidrajuh.net/gpensim/.

  2. 2.

    http://www2.informatik.hu-berlin.de/lehrstuehle/automaten/ina/.

  3. 3.

    http://sal.csl.sri.com/.

  4. 4.

    http://projects.laas.fr/tina/.

  5. 5.

    See the complete list of related publications at http://petridotnet.inf.mit.bme.hu/publications/.

  6. 6.

    http://www.futurict.szte.hu/en/home/.

  7. 7.

    http://www.r3-cop.eu/.

  8. 8.

    http://petridotnet.inf.mit.bme.hu/en/.

References

  1. Bartha, T., Vörös, A., Jámbor, A., Darvas, D.: Verification of an industrial safety function using coloured Petri nets and model checking. In: Proceedings of the 14th International Conference on Modern Information Technology in the Innovation Processes of the Industrial Enterprises, pp. 472–485. Hungarian Academy of Sciences (2012)

    Google Scholar 

  2. Cayir, S., Ucer, M.: An algorithm to compute a basis of Petri net invariants. In: 4th ELECO International Conference on Electrical and Electronics Engineering. UCTEA, Bursa, Turkey (2005)

    Google Scholar 

  3. Ciardo, G., Marmorstein, R., Siminiceanu, R.: The saturation algorithm for symbolic state-space exploration. Int. J. Softw. Tools Technol. Transf. 8(1), 4–25 (2006)

    Article  Google Scholar 

  4. Ciardo, G., Yu, A.J.: Saturation-based symbolic reachability analysis using conjunctive and disjunctive partitioning. In: Borrione, D., Paul, W. (eds.) CHARME 2005. LNCS, vol. 3725, pp. 146–161. Springer, Heidelberg (2005)

    Chapter  Google Scholar 

  5. Ciardo, G., Zhao, Y., Jin, X.: Ten years of saturation: a Petri net perspective. In: Jensen, K., Donatelli, S., Kleijn, J. (eds.) Transactions on Petri Nets and Other Models of Concurrency V. LNCS, vol. 6900, pp. 51–95. Springer, Heidelberg (2012)

    Chapter  Google Scholar 

  6. Clarke, E., Grumberg, O., Jha, S., Lu, Y., Veith, H.: Counterexample-guided abstraction refinement. In: Emerson, E.A., Sistla, A.P. (eds.) CAV 2000. LNCS, vol. 1855, pp. 154–169. Springer, Heidelberg (2000)

    Chapter  Google Scholar 

  7. Cseh, A., Tarnai, G., Sághi, B.: Petri net modelling of signalling systems [in Hungarian, original title: Biztosítóberendezések modellezése Petri-hálókkal]. Vezetékek Világa XIX(1), 14–17 (2014)

    Google Scholar 

  8. Darvas, D., Fernández Adiego, B., Blanco Viñuela, E.: Transforming PLC programs into formal models for verification purposes. Internal Note CERN-ACC-NOTE-2013-0040, CERN (2013)

    Google Scholar 

  9. Darvas, D., Vörös, A.: Saturation-based test input generation using coloured Petri nets [in Hungarian, original title: Szaturációalapú tesztbemenet-generálás színezett Petri-hálókkal]. In: Mesterpróba 2013, pp. 48–51 (2013)

    Google Scholar 

  10. Darvas, D., Vörös, A., Bartha, T.: Improving saturation-based bounded model checking. Acta Cybernetica (2014, accepted, in press). http://petridotnet.inf.mit.bme.hu/publications/AC2014_DarvasEtAl.pdf

  11. Duret-Lutz, A., Klai, K., Poitrenaud, D., Thierry-Mieg, Y.: Self-loop aggregation product — a new hybrid approach to on-the-fly LTL model checking. In: Bultan, T., Hsiung, P.-A. (eds.) ATVA 2011. LNCS, vol. 6996, pp. 336–350. Springer, Heidelberg (2011)

    Chapter  Google Scholar 

  12. Hajdu, Á., Vörös, A., Bartha, T.: New search strategies for the Petri net CEGAR approach. In: Devillers, R., Valmari, A. (eds.) PETRI NETS 2015. LNCS, vol. 9115, pp. 309–328. Springer, Heidelberg (2015)

    Chapter  MATH  Google Scholar 

  13. Hajdu, Á., Vörös, A., Bartha, T., Mártonka, Z.: Extensions to the CEGAR approach on Petri nets. Acta Cybernetica 21(3), 401–417 (2014)

    Article  MathSciNet  MATH  Google Scholar 

  14. Heiner, M., Rohr, C., Schwarick, M.: MARCIE – model checking and reachability analysis done efficiently. In: Colom, J.-M., Desel, J. (eds.) PETRI NETS 2013. LNCS, vol. 7927, pp. 389–399. Springer, Heidelberg (2013)

    Chapter  Google Scholar 

  15. ISO/IEC 15909-2 Systems, software engineering - High-level Petri nets - Part 2: Transfer format (2011)

    Google Scholar 

  16. Klenik, A., Marussy, K.: Configurable stochastic analysis framework for asynchronous systems. Scientific students’ associations report, Budapest University of Technology and Economics (2015). http://petridotnet.inf.mit.bme.hu/publications/TDK2015_KlenikMarussy.pdf

  17. Martínez, J., Silva, M.: A simple and fast algorithm to obtain all invariants of a generalised Petri net. In: Girault, C., Reisig, W. (eds.) Application and Theory of Petri Nets, Informatik-Fachberichte, vol. 52, pp. 301–310. Springer, Heidelberg (1982)

    Chapter  Google Scholar 

  18. Milánkovich, A., Ill, G., Lendvai, K., Imre, S., Szabó, S.: Evaluation of energy efficiency of aggregation in WSNs using Petri nets. In: Proceedings of the 3rd International Conference on Sensor Networks, pp. 289–297. Science and Technology Publications (2014)

    Google Scholar 

  19. Molnár, V., Darvas, D., Vörös, A., Bartha, T.: Saturation-based incremental LTL model checking with inductive proofs. In: Baier, C., Tinelli, C. (eds.) TACAS 2015. LNCS, vol. 9035, pp. 643–657. Springer, Heidelberg (2015)

    Chapter  Google Scholar 

  20. Molnár, V., Vörös, A., Darvas, D., Bartha, T., Majzik, I.: Component-wise incremental LTL model checking. Formal Aspects of Computing (2016, in press). doi:10.1007/s00165-015-0347-x

  21. Murata, T.: Petri nets: properties, analysis and applications. Proc. IEEE 77(4), 541–580 (1989)

    Article  Google Scholar 

  22. Szilvási, B.: Development of an education tool for the Formal methods course [in Hungarian, original title: Oktatási segédeszköz fejlesztése Formális módszerek tárgyhoz]. Master’s thesis, Budapest University of Technology and Economics (2008)

    Google Scholar 

  23. Thong, W.J., Ameedeen, M.A.: A survey of Petri net tools. ARPN J. Eng. Appl. Sci. 9(8), 1209–1214 (2014)

    Google Scholar 

  24. Vörös, A., Darvas, D., Bartha, T.: Bounded saturation-based CTL model checking. Proc. Est. Acad. Sci. 62(1), 59–70 (2013)

    Article  Google Scholar 

  25. Vörös, A., Darvas, D., Jámbor, A., Bartha, T.: Advanced saturation-based model checking of well-formed coloured Petri nets. Periodica Polytechnica, Electr. Eng. Comput. Sci. 58(1), 3–13 (2014)

    Article  Google Scholar 

  26. Wimmel, H., Wolf, K.: Applying CEGAR to the Petri net state equation. In: Abdulla, P.A., Leino, K.R.M. (eds.) TACAS 2011. LNCS, vol. 6605, pp. 224–238. Springer, Heidelberg (2011)

    Chapter  MATH  Google Scholar 

  27. Yu, A.J., Ciardo, G., Lüttgen, G.: Decision-diagram-based techniques for bounded reachability checking of asynchronous systems. Int. J. Softw. Tools Technol. Transf. 11(2), 117–131 (2009)

    Article  Google Scholar 

  28. Zhao, Y., Ciardo, G.: Symbolic CTL model checking of asynchronous systems using constrained saturation. In: Liu, Z., Ravn, A.P. (eds.) ATVA 2009. LNCS, vol. 5799, pp. 368–381. Springer, Heidelberg (2009)

    Chapter  Google Scholar 

Download references

Acknowledgement

The authors are grateful for all colleagues, former and present students and external users involved in the development, testing or the usage of the tool. Special thanks to Bertalan Szilvási for developing Petri.NET, the initial version of the presented tool.

This paper is partially supported by the MTA-BME Lendület 2015 Research Group on Cyber-Physical Systems and by the ARTEMIS JU and the Hungarian National Research, Development and Innovation Fund in the frame of the R5-COP and R3-COP projects.

Author information

Authors and Affiliations

  1. Department of Measurement and Information Systems, Budapest University of Technology and Economics, Budapest, Hungary

    András Vörös, Dániel Darvas, Vince Molnár, Attila Klenik, Ákos Hajdu, Attila Jámbor & István Majzik

  2. MTA-BME Lendület Cyber-Physical Systems Research Group, Budapest, Hungary

    András Vörös, Vince Molnár & Ákos Hajdu

  3. Institute for Computer Science and Control, Hungarian Academy of Sciences, Budapest, Hungary

    Tamás Bartha

Authors
  1. András Vörös
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Dániel Darvas
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Vince Molnár
    View author publications

    You can also search for this author in PubMed Google Scholar

  4. Attila Klenik
    View author publications

    You can also search for this author in PubMed Google Scholar

  5. Ákos Hajdu
    View author publications

    You can also search for this author in PubMed Google Scholar

  6. Attila Jámbor
    View author publications

    You can also search for this author in PubMed Google Scholar

  7. Tamás Bartha
    View author publications

    You can also search for this author in PubMed Google Scholar

  8. István Majzik
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to András Vörös .

Editor information

Editors and Affiliations

  1. Université Pierre and Marie Curie, Paris, France

    Fabrice Kordon

  2. Department Informatik, Universität Hamburg Department Informatik, Hamburg, Germany

    Daniel Moldt

Rights and permissions

Reprints and permissions

Copyright information

© 2016 Springer International Publishing Switzerland

About this paper

Cite this paper

Vörös, A. et al. (2016). PetriDotNet 1.5: Extensible Petri Net Editor and Analyser for Education and Research. In: Kordon, F., Moldt, D. (eds) Application and Theory of Petri Nets and Concurrency. PETRI NETS 2016. Lecture Notes in Computer Science(), vol 9698. Springer, Cham. https://doi.org/10.1007/978-3-319-39086-4_9

Download citation

  • DOI: https://doi.org/10.1007/978-3-319-39086-4_9

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-319-39085-7

  • Online ISBN: 978-3-319-39086-4

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation