Reasoning about Consistency in Model Merging

Living with Inconsistencies in Software Development 2010.

计算机科学;

Mehrdad Sabetzadeh† Shiva Nejati† Marsha Chechik‡ Steve Easterbrook‡ ; ‡ University of Toronto

Others  :  http://ceur-ws.org/Vol-661/paper6.pdf
PID  :  41915

学科分类：计算机科学（综合）

来源: CEUR

【 摘 要 】

Models undergo a variety of transformations throughout de- velopment. One of the key transformations is merge, used when developers need to combine a set of models with re- spect to the overlaps between them. A major question about model transformations in general, and merge in particular, is what consistency properties are preserved across the trans- formations and what consistency properties may need to be re-checked (and if necessary, re-established) over the result. In previous work [18], we developed a technique based on category-theoretic colimits for merging sets of inter-related models. The use of category theory leads to the preservation of the algebraic structure of the source models in the merge; however, this does not directly provide a characterization of the (in)consistency properties that carry over from the source models to the result, because consistency properties are predominantly expressed as logical formulas. Hence, an investigation of the connections between the “algebraic” and “logical” properties of model merging became necessary. In this paper, we undertake such an investigation and use techniques from finite model theory [9] to show that the use of colimits indeed leads to the preservation of certain logical properties. Our results have implications beyond the merge framework in [18] and are potentially useful for the broad range of techniques in the graph transformation and alge- braic specification literature that use colimits as the basis