PetriDotNet
PetriDotNet is a framework for the editing, simulation and analysis of Petri nets. The framework is developed by the Fault Tolerant Systems Research Group at the Budapest University of Technology and Economics.
Our aim is an easy to use and extendable tool to support Petri net based modelling and verification.
We have implemented and made available many advanced algorithms for the verification of Petri nets.
We are dealing with the following researches:
- 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.
Case study
We used our tool for the verification of an industrial embedde safety-critical system. Further details can be found here.
Download
The tool and the algorithms are under development, but the following versions can be dowloaded (we send other versions and the model checking moduls upon request):
- PetriDotNet -- For the education of Formal Methods (hungarian) (1.3.4836)
- PetriDotNet -- for the edition of ordinary and Colured Petri nets (without analysis) (1.3.4804)
- User manual (hungarian)
- Examples: examples.zip
The program requires .Net 4.0 runtime environment.
Contact persons:
Publications
Some of our main publications:
- 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 Entreprises (MITIP 2012), pp. 472-485, Budapest, Hungary, 10/2012.
- "Parallel Saturation Based Model Checking", The 10th International Symposium on Parallel and Distributed Computing (ISPDC 2011), Cluj Napoca, IEEE Computer Society, 07/2011.
- András Vörös, Dániel Darvas, Tamás Bartha: Bounded Saturation Based CTL Model Checking. The 12th Symposium on Programming Languages and Software Tools, SPLST11, pages 149-160, Tallinn, Estonia, 2011. Tallinn University of Technology, Institute of Cybernetics.
- Full list of publications
