up: Publications

Verifying Graph Transformation Systems with Description Logics

Jon Haël Brenas, Rachid Echahed, Martin Strecker



 
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