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.


For more information on the VIATRA2 model transformation framework, we kindly refer the reader to the VIATRA portal, the official website, and the Eclipse Wiki.

A thematic list of VIATRA2-related publications is available here. A comprehensive list is available on the portal.


EMF-IncQuery is an Eclipse-based framework that supports high-performance incremental model queries over large instance models. Based on the incremental graph pattern matching engine, core model-driven engineering applications such as on-the-fly well-formedness validation, model synchronization and view maintenance can be easily implemented in an extremely scalable way. More information is available on the official website of the project.

Gamma Statechart Composition Framework

The Gamma Statechart Composition Framework is a toolset to model, verify and generate code for component-based reactive systems. The framework builds on Yakindu, an open source statechart modeling tool and provides an additional modeling layer to instantiate a communicating network of statecharts. Compositionality is hierarchical, which facilitates the creation of reusable component libraries. Individual statecharts, as well as composite statechart networks can be validated and verified by an automated translation to UPPAAL, a model checker for timed automata. Once a complete model is built, designers can use the code generation functionality of the framework, which can generate Java code for the whole system. Read more »

Theta: a Framework for Abstraction Refinement-Based Model Checking

Theta is a generic, modular and configurable model checking framework developed at the Fault Tolerant Systems Research Group of Budapest University of Technology and Economics, aiming to support the design and evaluation of abstraction refinement-based algorithms for the reachability analysis of various formalisms.