In KAOS, every concept used in a definition in the goal model has to be defined in the object model. It means that when the goal model is complete, all predicates used in the formal definition of goals and in particular requirements have been defined in the object model \cite{Lamsweerde2009,Landtsheer2007a}. It seems thus interesting to translate in a way or another the object model to Event-B, so concepts manipulated in formulas have an equivalent in the Event-B model.

As Event-B uses the set theory to define and manipulate data, the KAOS object model could be quite easily transformed into an ERA model. Tools like DB-Main \cite{REVERv9.0.1} can automatically transform such model into a relational model compliant with relational databases. The relational nature of the diagram allows getting an Event-B model from it with a simple syntactic transformation. Moreover, as relational databases are the most used database management systems, the relational diagram could be used to generate SQL data definition code. This method implies more than one transformation. Another negative point is that the generated data definition in the Event-B Context and Machine may be more difficult to manipulate.

Snook et al. define in \cite{Snook2006,Said2009a} a method to transform a UML Class diagram into a classical B machine. This method may be adapted to transform the KAOS Object model which corresponds to a simplified UML Class diagram to an Event-B Machine and its associated Context.

From now we will take the following conventions: the name of the KAOS model elements will be those defined in the KAOS meta-model \cite{Lamsweerde2009}; the first letter of those meta-concepts will be in capital.

\subsection{Object types and Attributes}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

A set \texttt{OBJECT\_SET} of all possible objects belonging to a certain Object type is defined in the Context for each Object type. The set \texttt{OBJECTS} of all the existing instances of a certain Object type is defined in the Machine that will see the Context and belongs to the powerset of \texttt{OBJECT\_SET}. 

The domains of the Attributes have to be defined in the Context. In particular, non standard types or enumerated domains have to be specified in comprehension or in extension. Attributes are represented in the Machine by a partial or total function according to the Multiplicity of the Attribute, from an element of the \texttt{OBJECT} set to an element of the domain of the attribute. The table \ref{tab_transformation_rules_KAOS_attributes} gives the transformation rules for the different Multiplicities of an attribute of Object type \texttt{T}.

\begin{table}[h]
\centering
\caption{Transformation rules for KAOS Attributes}
\begin{tabularx}{\textwidth}{|p{2,3cm}|p{5,5cm}|X|}
\hline 
\textbf{KAOS attribute} & \textbf{Corresponding function} & \textbf{Event-B Invariant} \tabularnewline
\hline 
a : type [1..1] & 
Total function to \texttt{TYPE} &
$ a \in T \tfun TYPE $ \tabularnewline
\hline 
a : type [0..1] & 
Partial function to \texttt{TYPE} &
$ a \in T \pfun TYPE $ \tabularnewline
\hline 
a : type [1..n] & 
Total function to non-empty subset of \texttt{TYPE} &
$ a \in T \tfun \pown (TYPE) $ \tabularnewline
\hline 
a : type [0..n] & 
Total function to subsets of \texttt{TYPE} &
$ a \in T \tfun \pow (TYPE) $\tabularnewline 
\hline
\end{tabularx}
\label{tab_transformation_rules_KAOS_attributes}
\end{table}

\FloatBarrier
\subsection{Associations and Specializations}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

Associations may be directed or not and will be represented in the Machine by functions. Table \ref{tab_transformation_rules_KAOS_Associations} gives the transformation rules for the different kinds of directed associations. An undirected association corresponds to two opposite directed associations and can be manage as two directed associations with an additional invariant saying that if on exists, then the other exists too. For an association linking A to B with multiplicities [a1..a2] and [b1..b2] 

\begin{center}
A ---a1..a2------------------------------b1..b2---B \\
\end{center}

\begin{flushleft}
The result in Event-B will be :
\end{flushleft}

\begin{center}
A set AtoB according to the rules in table \ref{tab_transformation_rules_KAOS_Associations} \\
A set BtoA according to the rules in table \ref{tab_transformation_rules_KAOS_Associations} \\
An additional invariant: \\ 
$ \forall x,y \qdot (x \in A \wedge y \in B) \Leftrightarrow ( AtoB(x) = y \Leftrightarrow BtoA(y) = x ) $
\end{center}

\begin{figure}[h]
\centering
\includegraphics[width=0.75\textwidth]{images/ObjectModel2EventB_naryAssociation} 
\includegraphics[width=0.75\textwidth]{images/ObjectModel2EventB_naryAssociation_toClass} 
\caption{N-Ary Association are seen as an Entity with N directed Associations}
\label{fig_ObjectModel2EventB_naryAssociation}
\end{figure}

As show in figure \ref{fig_ObjectModel2EventB_naryAssociation}, an N-Ary Association will be seen as an Entity with N directed Associations to the different Objects of the N-Ary Association. 

In case of Specialization, usually instances belong to one and only one sub-Object type and sub-Objects instances are disjoints. As stated by Snook and Butler \cite{Snook2006}, when translating from KAOS to Event-B, the instances of the sub-Objects will be declared as a subset of super-Object's current instances. Three Object types, one Parent and two sons Son1 and Son2 specializing Parent will become in Event-B :

\begin{center}
$ PARENT \in \pow(PARENT\_SET)$ \\
$ SON1 \in \pow(PARENT)$ \\
$ SON2 \in \pow(PARENT)$ \\
$ SON1 \binter SON2 = \emptyset $
\end{center}

The Specialization may be more precise like in ERA, \eg if all the instances must be one of a sub-Object type then the sub-Objects instances sets cover the set of super-Object instances :

\begin{center}
$ SON1 \bunion SON2 = PARENT $
\end{center}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\begin{table}[h]
\centering
\caption{Transformation rules for KAOS directed Associations}
\begin{tabularx}{\textwidth}{|p{2cm}|p{5,5cm}|X|}

\hline 
\multicolumn{3}{|p{0.95\textwidth}|}{
The two Object types are A and B and $ a1..a2 \rightarrow b1..b2$ in the table represents the multiplicities for an association :
} \tabularnewline
\multicolumn{3}{|c|}{
A ----a1..a2--------------------b1..b2----> B 
} \tabularnewline
\multicolumn{3}{|p{0.95\textwidth}|}{
According to our convention, the Objects sets in Event-B will be called \texttt{A} and \texttt{B}.
} \tabularnewline 
\hline

\multicolumn{3}{|p{0.95\textwidth}|}{
The $disjoint$ macro in the table is defined as:
} \tabularnewline
\multicolumn{3}{|p{0.95\textwidth}|}{
\centering$ ( \forall a1,a2 \qdot (a1 \in dom ( AtoB ) \wedge a2 \in dom ( AtoB ) \wedge a1 \ne a2 \limp AtoB ( a1 )  \binter AtoB ( a2 ) = \emptyset ) ) $
} \tabularnewline \hline \hline

\textbf{KAOS association multiplicity} & \textbf{Corresponding function} & \textbf{Event-B Invariant} \tabularnewline
\hline
\hline
 
 $ 0..* \rightarrow 0..1 $  & 
Partial function to \texttt{B} &
$ AtoB \in A \pfun B $ \tabularnewline
\hline 

 $ 0..* \rightarrow 1..1 $  & 
Total function to \texttt{B} &
$ AtoB \in A \tfun B $ \tabularnewline
\hline 

 $ 0..* \rightarrow 0..* $  & 
Total function to subset of \texttt{B} &
$ AtoB \in A \tfun \pow (B) $ \tabularnewline
\hline 

 $ 0..* \rightarrow 1..* $  & 
Total function to non-empty subset of \texttt{B} &
$ AtoB \in A \tfun \pown (B) $ \tabularnewline
\hline 
\hline 

 $ 0..1 \rightarrow 0..1 $  & 
Partial injection to \texttt{B} &
$ AtoB \in A \pinj B $ \tabularnewline
\hline 

 $ 0..1 \rightarrow 1..1 $  & 
Total injection to \texttt{B} &
$ AtoB \in A \tinj B $ \tabularnewline
\hline 

 $ 0..1 \rightarrow 0..* $  & 
Total function to subsets of \texttt{B} which don't intersect &
$ AtoB \in A \tfun \pow (B) 
\wedge disjoint $ \tabularnewline
\hline 

 $ 0..1 \rightarrow 1..* $  & 
Total function to non-empty subsets of \texttt{B} which don't intersect &
$ AtoB \in A \tfun \pown (B) 
\wedge disjoint $ \tabularnewline
\hline 
\hline 

 $ 1..* \rightarrow 0..1 $  & 
Partial surjection to \texttt{B} &
$ AtoB \in A \psur B $ \tabularnewline
\hline 

 $ 1..* \rightarrow 1..1 $  & 
Total surjection to \texttt{B} &
$ AtoB \in A \tsur B $ \tabularnewline
\hline 

 $ 1..* \rightarrow 0..* $  & 
Total function to subsets of \texttt{B} which cover \texttt{B} &
$ AtoB \in A \tfun \pow (B) \wedge \union( \ran (AtoB))=B $ \tabularnewline
\hline 

 $ 1..* \rightarrow 1..* $  & 
Total function to non-empty subsets of \texttt{B} which cover \texttt{B} &
$ AtoB \in A \tfun \pown (B) \wedge \union( \ran (AtoB))=B $ \tabularnewline
\hline 
\hline 

 $ 1..1 \rightarrow 0..1 $  & 
Partial bijection to \texttt{B} (partial injection defined for all the elements of \texttt{B}) &
$ AtoB \in A \pinj B \wedge \forall b \qdot (b \in B \limp ( \exists a \qdot (a \in A \wedge (a \mapsto b) \in AtoB) ))  $ \tabularnewline
\hline 

 $ 1..1 \rightarrow 1..1 $  & 
Total bijection to \texttt{B} &
$ AtoB \in A \tbij B $ \tabularnewline
\hline 

 $ 1..1 \rightarrow 0..* $  & 
Total function to subsets of \texttt{B} which cover \texttt{B} without intersecting &
$ AtoB \in A \tfun \pow (B) \wedge \union( \ran (AtoB))=B \wedge disjoint $ \tabularnewline
\hline 

 $ 1..1 \rightarrow 0..* $  & 
Total function to non-empty subsets of \texttt{B} which cover \texttt{B} without intersecting &
$ AtoB \in A \tfun \pown (B) \wedge \union( \ran (AtoB))=B \wedge disjoint $ \tabularnewline
\hline 

\end{tabularx}
\label{tab_transformation_rules_KAOS_Associations}
\end{table}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
