A method for matching models in UML-B

UML-B is a graphical front-end formal modelling language of the formal method Event-B. UML-B models semantics are given by the corresponding generated Event-B. Identifying similarities between models has several benefits such as model comparison, integration and evolution. Several matching and comparison methods have been done in the context of model driven software engineering. However, matching models via a systematic method is not supported yet in UML-B. In this work, we propose a matching method for UML-B elements based on their semantics. This method includes variable-based matching, event-based matching and state-machine matching. The variable-based matching provides rules for matching UML-B classes, attributes, states and variables. The event-based matching provides rules and cases for matching UML-B transitions and class-events. The state-machine matching provides rules for matching UML-B state-machines based on the state and transition matching rules. The matching rules are formalized by means of the generated corresponding Event-B specifications. The correctness of the rules is justified via preserving the compatibility of the matched state-variables and corresponding modifying events including their matched guards and actions. These rules are illustrated via a communication-based case study to show their applicability.