Static Type Checking of Model Transformation Programs

摘要

Model transformations, utilized for various tasks, such as formal model analysis or code generation are key elements of model-driven development processes. As the complexity of developed model transformations grows, ensuring the correctness of transformation programs becomes increasingly difficult. Nonetheless, error detection is critical as errors can propagate into the target application. Various analysis methods are being researched for the validation of model transformations. Theorem proving based approaches, such as [5] show the possibility to prove statement validity over graph-based models.