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 instatiate 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 deployment layer to allocate the different components to host machines. This will refine the code generation functionality of the framework, which can generate Java or C++ code for the whole system. Read more »

Theta Configurable Abstraction Refinement-Based Verification Framework

The Theta Configurable Abstraction Refinement-Based Verification Framework is a modeling and verification framework to support designers and programmers in verifying behavioral properties. With the wide range of available high-level language frontends (including C programs and statecharts), users can describe their problems easily without deep knowledge in formal methods. These models are automatically transformed to lower-level formalisms with mathematically precise semantics. The underlying analysis backend can be fine-tuned by multiple configuration parameters to obtain automated tools, with recommended settings for different problem domains. Verification results are mapped back to the high-level formalisms and counderexample traces can be simulated to give a meaningful feedback to the user. Multiple intermediate formalisms serve the extensibility of the framework with new language frontends, and a low-level library provides built-in functionalities for developing new algorithms. Read more »