pdfreaders.org

Model Transformation as Conservative Theory-Transformation

Achim D. Brucker, Frééric Tuong und Burkhart Wolff

Cover for brucker.ea:model:2020.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.

Schlüsselwörter: Model Transformation; Conservativity; UML; OCL; Isabelle/HOL
Kategorien: ,
Dokumente: (Artikel als PDF Datei)

QR Code for brucker.ea:model:2020.Bitte zitieren sie diesen Artikel wie folgt:
Achim D. Brucker, Frééric Tuong und Burkhart Wolff. Model Transformation as Conservative Theory-Transformation. In J. Object Technol., 2020.
Schlüsselwörter: Model Transformation; Conservativity; UML; OCL; Isabelle/HOL
(Artikel als PDF Datei) (BibTeX) (Endnote) (RIS) (Word) (Share article on LinkedIn. Share article on CiteULike.)

BibTeX
@Article{ brucker.ea:model:2020,
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},
pdf = {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},
}