## 2 State of the Art
### Synchronisation Methodologies  
Different approaches exist to assert consistency between heterogeneous models. The model federation [2] approach uses a database to store all data from a system's models. Within that database, the user can assert consistency and traceability between the models. Proof theory is used by [3] in their inconsistency management approach. This methodology interprets models as first-order logics, identifying inconsistencies through a computer-aided proof tool. The lack of expressivity of proof theory limits this approach, making the interpretation and proofs difficult.  
A third approach to heterogeneous models consistency is model synchronisation [4]. The synchronization consists of a three-step process, which is illustrated in Figure 1:  
* Abstraction: The models are translated to a common formalism.
* Comparison: The comparison is operated in the abstracted models. Writing the compared models in a common formalism makes the comparison easier than with heterogeneous models.
* Concretization: The comparison results are carried back to the original models. Concretization can be achieved by correcting the models, annotations, or other means.  
The model synchronization approach is the base for different methodologies. In this work, we intend to interpret them in a mathematical framework.  
Regarding the SmartSync synchronization framework [20], the authors of the methodology provide a methodology and tools for the synchronization of the MBSE and MBSA models [21]. The comparison is operated on abstracted models written with the S2 ML language [22]. The S2 ML comparison models used in SmartSync are described with a set-theoretical point of view as a quintuple \(<P,C,B,\alpha,r\)[5], where:  
* P and B are sets of symbols called ports and blocks, respectively;
* C is a multiset of subsets of P called connections;
* \(\alpha\) is a subset of \(B\times(P\cup C\cup B)\) such as any element of \((P\cup C\cup B)\) that is associated with, at most, a unique element of B called its parent, and there exists a unique block \(r\in B\) with no parent. SmartSync relies on the user to manually align model elements, as described in Section 4.2.1.  
The directed graph methodology from [23] is also a synchronization methodology. It does rely on the abstraction of the models towards graphs. In the graphs, vertices represent parts and ports from SysML and blocks and classes from AltaRica; edges represent connectors from SysML and assertions from AltaRica. This framework allows for the use of graph search algorithms to traverse the graphs, and the use of concepts such as graph and sub-graph isomorphisms to compare the models.  
Figure 1: Model synchronisation approach.  
The consistency links methodology [24] is another synchronization approach that creates links between MBSE and MBSA models. This methodology mainly focuses on the functional aspect of the system.  
The three latest methodologies provide a structural comparison between system engineering and safety models. They rely on comparison models that follow the block, ports, and connection structure described in Section 2.1.3, with different ways to represent them. Category theory offers a point of view that allows us to use both the strengths of the graph and set theories, along with other topological tools, which is why we use it to provide a mathematical framework for synchronization methodologies. We do not find a clear formalisation of the consistency notion that seems to be widely accepted by the community. We provide a mathematical framework within which we define an axiomatic for the representation of models and propose a formal definition of a consistency relation.