Towards Model Transformation Validation from Model Validation

点击翻译按钮获取中文摘要

In this research, we succeeded in designing a static verification algorithm for validating transformations in UnQL(UnCAL), a known graph(model) querying language. Our new approach to the verification problem is based on the two important characteristics of UnCAL, bisimulation-equivalence of graphs and structured recursion, and we show that a graph transformation in the Core UnCAL can be automatically checked with the MONA system against a schema specified in the powerful monadic second order logic(MSO). Moreover, we show that ranges of transformations can be statically computed, which can be used to exclude invalid updates on the resulting graph of a transformation.