About GROOVE
GROOVE is a project centered around the use of simple graphs for modelling the design-time, compile-time, and run-time structure of object-oriented systems, and graph transformations as a basis for model transformation and operational semantics. This entails a formal foundation for model transformation and dynamic semantics, and the ability to verify model transformation and dynamic semantics through an (automatic) analysis of the resulting graph transformation systems, for instance using model checking.
The GROOVE tool set includes an editor for creating graph production rules, a simulator for visually computing the graph transformations induced by a set of graph production rules, a generator for automatically exploring state spaces, a model checker that supports CTL and LTL formulas and an imaging tool for converting graphs to images.
