Model Transformation as Conservative Theory-Transformation

By Achim D. Brucker, Frééric Tuong, and Burkhart Wolff.

Model transformations play a central role in model-driven software development. Hence, logical unsafe model transformation can result in erroneous systems. Still, most model transformations are written in languages that do not provide built-in safeness guarantees.

We present a new technique to construct tool support for domain-specific languages (DSLs) inside the interactive theorem prover environment Isabelle. Our approach is based on modeling the DSL formally in higher-order logic (HOL), modeling the API of Isabelle inside it, and defining the transformation between these two. Reflection via the powerful code generators yields code that can be integrated as extension into Isabelle and its user interface. Moreover, we use code generation to produce tactic code which is bound to appropriate command-level syntax.

Our approach ensures the logical safeness (conservativity) of the theorem prover extension and, thus, provides a certified tool for the DSL in all aspects: the deductive capacities of theorem prover, code generation, and IDE support. We demonstrate our approach by extending Isabelle/HOL with support for UML/OCL and, more generally, providing support for a formal object-oriented modeling method.

Keywords:
Model Transformation, Conservativity, UML, OCL, Isabelle/HOL

Please cite this work as follows:
A. D. Brucker, F. Tuong, and B. Wolff, “Model transformation as conservative theory-transformation,” J. Object Technol., 2020. Author copy: https://logicalhacking.com/publications/brucker.ea-model-2020/

BibTeX
@Article{ brucker.ea:model:2020,
  author   = {Achim D. Brucker and Fr{\'e}{\'e}ric Tuong and Burkhart Wolff},
  title    = {Model Transformation as Conservative Theory-Transformation},
  journal  = {J. Object Technol.},
  year     = {2020},
  areas    = {formal methods, software},
  abstract = {Model transformations play a central role in model-driven
              software development. Hence, logical unsafe model
              transformation can result in erroneous systems. Still, most
              model transformations are written in languages that do not
              provide built-in safeness guarantees.
              
              We present a new technique to construct tool support for
              domain-specific languages (DSLs) inside the interactive
              theorem prover environment Isabelle. Our approach is based on
              modeling the DSL formally in higher-order logic (HOL),
              modeling the API of Isabelle inside it, and defining the
              transformation between these two. Reflection via the powerful
              code generators yields code that can be integrated as
              extension into Isabelle and its user interface. Moreover, we
              use code generation to produce tactic code which is bound to
              appropriate command-level syntax.
              
              Our approach ensures the logical safeness (conservativity) of
              the theorem prover extension and, thus, provides a certified
              tool for the DSL in all aspects: the deductive capacities of
              theorem prover, code generation, and IDE support. We
              demonstrate our approach by extending Isabelle/HOL with
              support for UML/OCL and, more generally, providing support for
              a formal object-oriented modeling method.},
  keywords = {Model Transformation, Conservativity, UML, OCL,
              Isabelle/HOL},
  note     = {Author copy: \url{https://logicalhacking.com/publications/brucker.ea-model-2020/}},
  pdf      = {https://logicalhacking.com/publications/brucker.ea-model-2020/brucker.ea-model-2020.pdf},
}