up: Publications |
Abstract |
We address the problem of verification of graph transformations
featuring actions such as node merging and cloning,
addition and deletion of nodes and edges, node or edge
labeling and edge redirection. We introduce the
considered graph rewrite systems following an algorithmic approach and
then tackle their formal verification by proposing a Hoare-like
weakest precondition calculus. Specifications are defined as triples
of the form {Pre} (R, strategy) {Post}
where Pre and Post are conditions specified in a
given Description Logic (DL), R is a graph rewrite system and
strategy is an expression stating in which order the rules in
R are to be performed. We prove that the proposed calculus
is sound and characterize which DL logics are suited or not for the
targeted verification tasks, according to their expressive power.
Online Copy |
BibTeX Entry |
@inproceedings{brenas18:_verif_graph_trans_system_descr_logic, author = {Jon Ha{\"{e}}l Brenas and Rachid Echahed and Martin Strecker}, title = {Verifying Graph Transformation Systems with Description Logics}, booktitle = {Graph Transformation - 11th International Conference, {ICGT} 2018, Held as Part of {STAF} 2018, Toulouse, France, June 25-26, 2018, Proceedings}, pages = {155--170}, year = 2018, doi = {10.1007/978-3-319-92991-0_10}, editor = {Leen Lambers and Jens H. Weber}, volume = 10887, publisher = {Springer} , url = {http://www.irit.fr/~Martin.Strecker/Publications/icgt2018.html} }
Last modified: Wed Oct 17 01:04:34 CEST 2018 |