Constructing optimized constraint-preserving application conditions for model transformation rules

Constructing optimized constraint-preserving application conditions for model transformation rules
复制标题

构建模型转换规则的优化约束保留应用条件

DOI:
10.1016/j.jlamp.2020.100564
复制
发表时间:
2020
期刊:
J. Log. Algebraic Methods Program.
影响因子:
--
通讯作者:
Gabriele Taentzer
Gabriele Taentzer
中科院分区:
--
文献类型:
--
作者:
Nebras Nassar;Jens Kosiol;Thorsten Arendt;Gabriele Taentzer

文献摘要

参考文献

被引文献

相似文献

有一个模型转换,以确保有效的结果模型wrt一个给定的约束的需求越来越大。例如,在模型重构中,每次执行重构都应该再次产生一个有效的模型。给定一个约束,如果模型转换规则总是产生有效的输出,则称为约束保证;如果仅应用于已经有效的模型,则称为约束保持。在文献中,有一个正式的结构模型转换系统,使他们的约束保证。这是通过将应用程序条件添加到其转换规则中来确保的。然而,这些条件可能变得相当大。由于有一些有趣的应用案例,其中转换只需要保持约束(例如模型重构),因此应用条件的构造也适用于这种情况。虽然逻辑上较弱,但直接的构造可以导致更大的应用条件。在这项工作中,我们开发了简化的约束保证条件,通过省略这些条件的某些部分,即检查先行有效性的部分。我们证明了由此产生的应用条件是约束保持和表征其逻辑强度。我们的理论是为M-粘合剂类别,其中包括各种图形的模型结构。此外,在Eclipse插件OCL 2AC中实现了约束保证应用条件的计算及其简化。评估表明,所构造的简化条件的复杂性平均降低了7倍。此外,这种优化产生了约2.5倍的规则应用的加速。
There is an increasing need for model transformations ensuring valid result models wrt a given constraint. In model refactoring, for example, each performed refactoring should yield a valid model again. Given a constraint, if a model transformation rule always produces valid output, it is called constraint-guaranteeing; if only when applied to an already valid model, it is called constraint-preserving. In the literature, there is a formal construction for model transformation systems making them constraint-guaranteeing. This is ensured by adding application conditions to their transformation rules. These conditions can become quite large, though. As there are interesting application cases where transformations just need to be constraint-preserving (such as model refactoring), the construction of application conditions was also adapted to this case. Although logically weaker, the straightforward construction can lead to even larger application conditions. In this work, we develop simplifications of constraint-guaranteeing conditions by omitting certain parts of these conditions, namely of parts that check for antecedent validity. We prove that the resulting application conditions are constraint-preserving and characterize their logical strength. Our theory is developed for M-adhesive categories which encompass various graph-like model structures. In addition, the computation of constraint-guaranteeing application conditions and their simplifications was implemented in the Eclipse plug-in OCL2AC. Evaluations show that the complexity of the constructed simplified conditions is reduced by factor 7 on average. Moreover, this optimization yields a speedup of rule application by approximately 2.5 times.
随机重写系统的换向器:Z3 中的理论与实现
DOI: --
发表时间: 2020
期刊: GCM@STAF
影响因子: --
作者:
Nicolas Behr;Maryam Ghaffari Saadat;R. Heckel
通讯作者: R. Heckel
模型版本控制中保持一致性的编辑脚本
DOI: --
发表时间: 2013
期刊: International Conference on Automated Software Engineering
影响因子: --
作者:
Timo Kehrer;U. Kelter;G. Taentzer
通讯作者: G. Taentzer
DOI: --
发表时间: 2014
影响因子: 0.5
作者:
H. Ehrig;Ulrike Golas;A. Habel;Leen Lambers;F. Orejas
通讯作者: F. Orejas
Sesqui-Pushout 重写
DOI: --
发表时间: 2006
期刊: International Conference on Graph Transformation
影响因子: --
作者:
A. Corradini;T. Heindel;F. Hermann;B. König
通讯作者: B. König
DOI: --
发表时间: 2005
期刊: ACM/IEEE International Conference on Model Driven Engineering Languages and Systems
影响因子: --
作者:
M. Giese;Daniel Larsson
通讯作者: Daniel Larsson