
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/
@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},
}