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
- Zheng Cheng, Massimo Tisi. [ Incremental Deductive Verification for Relational Model Transformations]. In 10th IEEE International Conference on Software Testing, Verification and ValidationTo appear, 2017
- Zheng Cheng, Rosemary Monahan, James F. Power. Formalised EMFTVM bytecode language for sound verification of model transformations. In Software & Systems Modeling, 2016
- Zheng Cheng, Rosemary Monahan, James F. Power. A Sound Execution Semantics for ATL via Translation Validation. In 8th International Conference on Model Transformation, L'Aquila, Italy2015
- Fabian Buettner; Marina Egea; Jordi Cabot. On verifying ATL transformations using 'off-the-shelf' SMT solvers. In 15th International Conference on Model Driven Engineering Languages & Systems, Innsbruck, Austria2012
- Fabian Buettner; Jordi Cabot. Lightweight String Reasoning for OCL. In 8th European Conference on Modelling Foundations and Applications, Lyngby, Denmark2012
- Fabian Buettner; Marina Egea; Jordi Cabot; Martin Gogolla. Verification of ATL Transformations Using Transformation Models and Model Finders. In 14th International Conference on Formal Engineering Methods, Kyoto, Japan2012
- Carlos A. González; Fabian Buettner; Robert Clarisó; Jordi Cabot. EMFtoCSP: A Tool for the Lightweight Verification of EMF Models. In Formal Methods in Software Engineering: Rigorous and Agile Approaches, Zurich, Switzerland2011