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
Categories: ,
Documents: (full text as PDF file)
Please cite this article as follows:
Achim D. Brucker, Frééric Tuong, and Burkhart Wolff.
Model Transformation as Conservative Theory-Transformation.
In J. Object Technol., 2020.
Keywords: Model Transformation; Conservativity; UML; OCL; Isabelle/HOL
(full text as PDF file) (BibTeX) (Endnote) (RIS) (Word) (
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.}, | |
author | = | {Achim D. Brucker and Fr{\'e}{\'e}ric Tuong and Burkhart Wolff}, | |
journal | = | {J. Object Technol.}, | |
keywords | = | {Model Transformation; Conservativity; UML; OCL; Isabelle/HOL}, | |
= | {https://www.brucker.ch/bibliography/download/2020/brucker.ea-model-2020.pdf}, | ||
title | = | {Model Transformation as Conservative Theory-Transformation}, | |
url | = | {https://www.brucker.ch/bibliography/abstract/brucker.ea-model-2020}, | |
year | = | {2020}, |