Model Quality

From AtlanMod

With the increasing use of model-driven engineering in safety-critical domains (e.g., in automotive industry, medical data processing, aviation, it is crucial to develop techniques and tools that prevent incorrect model transformations from generating faulty models. The effects of such faulty models could be unpredictably propagated into subsequent MDE steps, e.g. code generation.

For this reason, there is a great need of mechanisms to ensure quality and the absence of errors in models and model transformations. Verification is one of the effective techniques that are typically used to achieve this.


Verification of models and model transformations refers to the ability of these elements to satisfy one or more correctness properties. These properties express certain characteristics that the element under analysis must feature in order to be considered correct. It is typical for verification tools to use formal methods to determine whether the model or model transformation under analysis satisfies the correctness properties under scrutiny.


Current research topics

  • Verification of Model Transformations
  • Verification of Static Models


Main publications

  • Zheng Cheng, Massimo Tisi. [ Incremental Deductive Verification for Relational Model Transformations]. In 10th IEEE International Conference on Software Testing, Verification and ValidationTo appear, 2017