up: Publications |
Abstract |
We present a prototype for executing and verifying graph transformations.
The transformations are written in a simple imperative programming language,
and pre- and post-conditions as well as loop invariants are specified in the
Description Logic ALC (whence the name of the tool). The
programming language has a precisely defined operational semantics and a sound
Hoare-style calculus. The tool consists of the following sub-components: a
compiler to Java for executing the transformations; a verification condition
generator; and a tableau prover for an extension of ALC capable of deciding
the generated verification conditions. A description of these components and
their interaction is the main purpose of this paper.
Online Copy |
BibTeX Entry |
@inproceedings{baklanova15:_provab_correc_graph_trans_small, author = {Nadezhda Baklanova and Jon Ha{\"{e}}l Brenas and Rachid Echahed and Christian Percebois and Martin Strecker and Hanh Nhi Tran}, title = {Provably Correct Graph Transformations with Small-tALC}, booktitle = {Proceedings of the 11th International Conference on {ICT} in Education, Research and Industrial Applications: Integration, Harmonization and Knowledge Transfer, Lviv, Ukraine, May 14-16, 2015.}, pages = {78--93}, year = 2015, url = {https://www.irit.fr/~Martin.Strecker/Publications/icteri2015.html} }
Last modified: Mon Jun 8 19:56:45 CEST 2015 |