A main goal of MDE is the usage of models for early verification. Goal of the Invariant Checker project is the development of techniques for static analysis. Examples are graph based techniques for proving that certain safety critical states are not reached during execution of a software system.
With the advent of MDE not only models but also model transformations became first-class artefacts in the development process. Model transformations manipulate models with different goals such as refinement, code generation, refactoring, etc. In order to ensure correctness of software developed using MDE it is of major importance to be able to verify these model transformations. Therefore, the CorMorant project (see also the research page of the project) aims at presenting methods for the formal verification of correctness of model transformation based on graph transformation.
Moreover, in the context of the QUANTUM project, whose goal is the development of new quantitative models and quantitative analysis techniques for service-oriented real-time systems that provide the required combinations of probabilistic behavior, real-time behavior, and structure dynamics, we introduced the formal model of Probabilistic Timed Graph Transformation Systems (PTGTSs) and outlined a mapping of PTGTS models employing an extended version of the HENSHIN tool to probabilistic timed automata (PTA) such that the PRISM model checker can be used to analyze PTGTS models with respect to PTCTL properties. Also, to enable the analysis of complex large-scale PTGTS models, we developed a simulator for PTGTSs that allows to import real-world topologies, to automatically detect violations of state properties, and to handle the graph pattern matching as well as time and probabilities efficiently.