Share and Export
Share and Export
Cheng, Zheng, Monahan, Rosemary and Power, James F. (2016) Verifying SimpleGT Transformations Using an Intermediate Verification Language. In: 4th International Workshop on the Verification Of Model Transformations, Jully 2015, L'Aquila, Italy.
Preview
Available under License Creative Commons Attribution Non-commercial Share Alike.
Download (251kB) | Preview
Abstract
Previously, we have developed the VerMTLr framework that
allows rapid verifier construction for relational model transformation languages. VerMTLr draws on the Boogie intermediate verification language
to systematically design a modular and reusable verifier. It also includes
a modular formalisation of EMFTVM bytecode to ensure verifier soundness. In this work, we will illustrate how to adapt VerMTLr to design
a verifier for the SimpleGT graph transformation language, which allows us to soundly prove the correctness of graph transformations. An
experiment with the Pacman game demonstrates the feasibility of our
approach.
| Item Type: | Conference or Workshop Item (Paper) |
|---|---|
| Keywords: | model transformation verification; graph transformation; SimpleGT; automatic theorem proving; intermediate verification language; Boogie; |
| Academic Unit: | Faculty of Science and Engineering > Computer Science |
| Item ID: | 8220 |
| Depositing User: | Dr. James Power |
| Date Deposited: | 17 May 2017 15:37 |
| Refereed: | Yes |
| Use Licence: | This item is available under a Creative Commons Attribution Non Commercial Share Alike Licence (CC BY-NC-SA). Details of this licence are available here |
Downloads
Downloads per month over past year
Origin of downloads
Repository Staff Only (login required)
- Item control page
