Skip to main content
Top

2016 | OriginalPaper | Chapter

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

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

Published in: Application and Theory of Petri Nets and Concurrency

Publisher: Springer International Publishing

Activate our intelligent search to find suitable subject content or patents.

search-config
loading …

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.

Dont have a licence yet? Then find out more about our products and how to get one now:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

Mit Springer Professional "Wirtschaft+Technik" erhalten Sie Zugriff auf:

  • über 102.000 Bücher
  • über 537 Zeitschriften

aus folgenden Fachgebieten:

  • Automobil + Motoren
  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Elektrotechnik + Elektronik
  • Energie + Nachhaltigkeit
  • Finance + Banking
  • Management + Führung
  • Marketing + Vertrieb
  • Maschinenbau + Werkstoffe
  • Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

  • über 67.000 Bücher
  • über 390 Zeitschriften

aus folgenden Fachgebieten:

  • Automobil + Motoren
  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Elektrotechnik + Elektronik
  • Energie + Nachhaltigkeit
  • Maschinenbau + Werkstoffe




 

Jetzt Wissensvorsprung sichern!

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

  • über 67.000 Bücher
  • über 340 Zeitschriften

aus folgenden Fachgebieten:

  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Finance + Banking
  • Management + Führung
  • Marketing + Vertrieb
  • Versicherung + Risiko




Jetzt Wissensvorsprung sichern!

Literature
1.
go back to reference 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) 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)
2.
go back to reference 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) 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)
3.
go back to reference 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)CrossRef 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)CrossRef
4.
go back to reference 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)CrossRef 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)CrossRef
5.
go back to reference 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)CrossRef 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)CrossRef
6.
go back to reference 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)CrossRef 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)CrossRef
7.
go back to reference 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) 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)
8.
go back to reference 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) 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)
9.
go back to reference 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) 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)
11.
go back to reference 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)CrossRef 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)CrossRef
12.
go back to reference 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)CrossRefMATH 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)CrossRefMATH
13.
go back to reference 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)MathSciNetCrossRefMATH 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)MathSciNetCrossRefMATH
14.
go back to reference 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)CrossRef 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)CrossRef
15.
go back to reference ISO/IEC 15909-2 Systems, software engineering - High-level Petri nets - Part 2: Transfer format (2011) ISO/IEC 15909-2 Systems, software engineering - High-level Petri nets - Part 2: Transfer format (2011)
17.
go back to reference 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)CrossRef 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)CrossRef
18.
go back to reference 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) 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)
19.
go back to reference 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)CrossRef 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)CrossRef
20.
go back to reference 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 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.
go back to reference Murata, T.: Petri nets: properties, analysis and applications. Proc. IEEE 77(4), 541–580 (1989)CrossRef Murata, T.: Petri nets: properties, analysis and applications. Proc. IEEE 77(4), 541–580 (1989)CrossRef
22.
go back to reference 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) 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)
23.
go back to reference Thong, W.J., Ameedeen, M.A.: A survey of Petri net tools. ARPN J. Eng. Appl. Sci. 9(8), 1209–1214 (2014) Thong, W.J., Ameedeen, M.A.: A survey of Petri net tools. ARPN J. Eng. Appl. Sci. 9(8), 1209–1214 (2014)
24.
go back to reference Vörös, A., Darvas, D., Bartha, T.: Bounded saturation-based CTL model checking. Proc. Est. Acad. Sci. 62(1), 59–70 (2013)CrossRef Vörös, A., Darvas, D., Bartha, T.: Bounded saturation-based CTL model checking. Proc. Est. Acad. Sci. 62(1), 59–70 (2013)CrossRef
25.
go back to reference 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)CrossRef 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)CrossRef
26.
go back to reference 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)CrossRefMATH 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)CrossRefMATH
27.
go back to reference 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)CrossRef 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)CrossRef
28.
go back to reference 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)CrossRef 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)CrossRef
Metadata
Title
PetriDotNet 1.5: Extensible Petri Net Editor and Analyser for Education and Research
Authors
András Vörös
Dániel Darvas
Vince Molnár
Attila Klenik
Ákos Hajdu
Attila Jámbor
Tamás Bartha
István Majzik
Copyright Year
2016
DOI
https://doi.org/10.1007/978-3-319-39086-4_9

Premium Partner