PetriDotNet

PetriDotNet is a framework for the editing, simulation and analysis of Petri nets. Our aim is an easy to use and extendable tool to support Petri net based modelling and verification. It provides a convenient graphical editor for creating (ordinary or coloured) Petri nets. It is extended with analysis of structural and dynamic properties of Petri nets, simulation, reachability and model checking capabilities. Furthermore, PetriDotNet is a simple, generic and extensible platform for new, Petri net-based algorithms that provides wide access to the Petri net data structures and the graphical user interface.

The framework is developed by the Fault Tolerant Systems Research Group at the Budapest University of Technology and Economics.

We are dealing with the following research directions:

• Saturation-based symbolic state space exploration and CTL model checking,
• LTL model checking based on saturation,
• Verification of infinite state systems: CEGAR-based Petri net reachability checking,
• Markovian stochastic analysis.

Case study

We used our tool for the verification of an industrial embedde safety-critical system. Further details can be found here.

Measurements

A large number of measurements and comparisons were done in our paper at TACAS 2015, these measurements are available here.

The synthetic models used in the paper presented at Petri nets 2015 are available here.

Models for the measurements of the stochastic analysis are available here.

Download

The latest version of the tool and the algorithms can be downloaded:

• PetriDotNet -- complete tool with analysis (1.5-beta2) | User manual (in English)
• Example models: examples.zip (also included in the release)

The program requires Microsoft .NET 4.0 runtime environment.

Contact persons:

• András Vörös
• István Majzik
• Tamás Bartha

Technical support: <the name of the tool> at inf.mit.bme.hu

Publications

Full list of publications

Main publications

• Ákos Hajdu, András Vörös, and Tamás Bartha. New search strategies for the Petri net CEGAR approach.
  In Raymond Devillers and Antti Valmari, editors, Application and Theory of Petri Nets and Concurrency, volume 9115 of Lecture Notes in Computer Science, pp. 309-328. Springer, 2015. Presented at the 36th International Conference on Application and Theory of Petri Nets and Concurrency.
• Vince Molnár, Dániel Darvas, András Vörös, and Tamás Bartha. Saturation-based incremental LTL model checking with inductive proofs. In C. Baier and C. Tinelli, editors, Tools and Algorithms for the Construction and Analysis of Systems, volume 9035 of Lecture Notes in Computer Science, pp. 643-657. Springer, 2015.
• Ákos Hajdu, András Vörös, Tamás Bartha, Zoltán Mártonka: Extensions to the CEGAR Approach on Petri Nets.
  Acta Cybernetica, 21(3):401-417, 2014. DOI: 
• András Vörös, Dániel Darvas, Attila Jámbor, Tamás Bartha: Advanced Saturation-based Model Checking of Well-formed Coloured Petri Nets. Periodica Polytechnica, Electrical Engineering and Computer Science, 58(1):3-13, 2014.
• András Vörös, Dániel Darvas, Tamás Bartha: Bounded saturation-based CTL model checking. Proceedings of the Estonian Academy of Sciences, 62(1):59-70, 2013.
• Tamás Bartha, András Vörös, Attila Jámbor, Dániel Darvas: Verification of an Industrial Safety Function Using Coloured Petri Nets and Model Checking. In: 14th International Conference on Modern Information Technology in the Innovation Processes of the Industrial Enterprises (MITIP 2012), pp. 472-485, 2012.
• András Vörös, Tamás Bartha, Dániel Darvas, Tamás Szabó, Attila Jámbor, Ákos Horváth: Parallel Saturation Based Model Checking. In: The 10th International Symposium on Parallel and Distributed Computing (ISPDC 2011), IEEE Computer Society, 2011.