Formal Verification of QVT Transformations for Code Generation

Kurt Stenzel, Nina Moebius, Wolfgang Reif

We present a formal calculus for operational QVT. The calculus is implemented in the interactive theorem prover KIV and allows to prove properties of QVT transformations for arbitrary meta models. Additionally we present a framework for provably correct Java code generation. The framework uses a meta model for a Java abstract syntax tree as the target of QVT transformations. This meta model is mapped to a formal Java semantics in KIV. This makes it possible to formally prove with the QVT calculus that a transformation always generates a Java model (i.e. a program) that is type correct and has certain semantical properties. The Java model can be used to generate source code by a model-to-text transformation or byte code directly.
published 2011 Proceedings of MODELS 2011 - 14th International Conference on Model Driven Engineering Languages and Systems

Publisher: Springer LNCS 6981