Formal Description and Verification of a Text-based Model Differencing and Merging Method

摘要

Version control is an integral part of teamwork in software development. Differencing and merging key artifacts (i.e. source code) is a key feature in version control systems. The concept of version control can also be applied to model-driven methodologies. The models are usually differenced and merged in their graph-based form. However, if supported, we can also use the textual representation of the models during this process. Text-based model differencing and merging methods have some useful use cases, like supporting the persistence of the model, or having a fallback plan should the differencing algorithm fail. Using the textual notation to display and edit models is relatively rare, as the visual (graph-based) representation of the model is more common. However, many believe that using them both would be the ideal solution. In this paper, we present the formal description of a text-based model differencing and merging method from previous work. We also verify our algorithm based on this formal description. The focus of the verification is the soundness and completeness of the method. The long term goal of our research is to develop a modeling environment-independent algorithm. This could be used in version control systems that support textual representations.