Semantic Merging
Last Updated on Wednesday, 03 August 2011 08:52 Written by Administrator
Current optimistic model versioning systems, which are indispensable to coordinate the collaboration within teams, are able to detect several kinds of conflicts between two concurrently modified versions of one model. These systems support the detection of syntactical problems such as contradicting changes and violations of the underlying metamodel or of OCL constraints, but violations of the semantics remain unreported. We suggest to use redundant information inherent in models to check if the semantics is violated during the merge process. In particular, we exploit the information encoded in state machine diagrams to validate evolving sequence diagrams by the means of the model checker SPIN.
Semantics Aware Merging
Consider the following versioning scenario. The UML state machine diagram below models a coffee machine and the UML sequence diagram a possible behavior thereof.
Two software engineers change the sequence diagram at the same time: one includes the message turnOff(), resulting in S', the other adds the message prepareTea(), resulting in S''. Each change on its own results in a sequence diagram consistent with the state machine. The next step is to merge the changes into a new sequence diagram Ŝ using an automatic versioning tool.
As the messages of a lifeline are represented as ordered list, an Update/Update conflict occurs, because both newly added messages are stored at the same index of this list. A conceivable merging strategy is to consider all possible combinations of the two diagrams. This may result in several syntactically correct diagrams. The lower part of the Sequence Diagram Figure shows two possibilities Ŝ1 and Ŝ2: turnOff() can be placed before or after makeTea(). However, making tea after turning off the machine does not make much sense and a modeler would avoid such a solution in a manual merge process.
At first glance, it might seem necessary to provide additional knowledge, e.g., a specifically tailored ontology, to support an automatic merge process aware of the model’s semantics. However, in modeling languages like the UML, the required knowledge is in fact distributed over different types of diagrams. Each diagram type provides a view on a specific aspect of the described system. Yet, these views overlap in parts, effectively duplicating certain aspects of the system across different diagrams. For our example, we may ascertain, that the first merge option, i.e., turnOff() before makeTea(), turns out inconsistent with respect to the state machine diagram, as preparing tea after turning off the machine is not possible.
We propose to integrate the model checker SPIN to support the merge process. We have implemented the outlined approach based on the Eclipse Modeling Framework (EMF). In particular, the presented language excerpt of UML has been specified as an Ecore-based metamodel. The transformations of state machines into PROMELA automata and sequence diagrams into PROMELA arrays have been implemented as model-to-text transformations using Xpand.
Download
The prototype including the Ecore-based metamodel, the transformation to PROMELA, and examples may be downloaded as Eclipse project. Import the project into the workspace of your Eclipse modeling edition and run as MWE Workflow to execute code generation.