Thumbnail
Access Restriction
Open

Author Schätz, Bernhard ♦ Boronat, Artur ♦ Heckel, Reiko ♦ Margaria, Tiziana ♦ Padberg, Julia ♦ Taentzer, Gabriele
Source CiteSeerX
Content type Text
File Format PDF
Subject Domain (in DDC) Computer science, information & general works ♦ Data processing & computer science
Subject Keyword Model Transformation ♦ Soundness Condition ♦ Declarative Relational Specification ♦ Automatic Transformation ♦ Graph Transformation ♦ Important Issue ♦ Declarative Relational Style Transformation ♦ Formal Verification ♦ Isabelle Theorem Prover ♦ Connectedness Soundness Condition ♦ Abstract Description Technique ♦ Direct Translation ♦ Relational Style ♦ Refactoring Transformation ♦ Interactive Theorem Prover ♦ Test-based Approach
Abstract Abstract: With the increasing use of automatic transformations of models, the correctness of these transformations becomes an increasingly important issue. Especially for model transformation generally defined using abstract description techniques like graph transformations or declarative relational specifications, however, establishing the soundness of those transformations by test-based approaches is not straight-forward. We show how formal verification of soundness conditions over such declarative relational style transformations can be performed using an interactive theorem prover. The relational style allows a direct translation of transformations as well as associated soundness conditions into corresponding axioms and theorems. Using the Isabelle theorem prover, the approach is demonstrated for a refactoring transformation and a connectedness soundness condition.
Educational Role Student ♦ Teacher
Age Range above 22 year
Educational Use Research
Education Level UG and PG ♦ Career/Technical Study
Learning Resource Type Article