Matoussi describes in \cite{ Matoussi2009a, Gervais2009, Matoussi2008} a process to transform a KAOS goal model into an Event-B specification. This process takes on input a KAOS goal model that is not operationalized and produces an Event-B model corresponding to a specification that satisfies the requirements described in the input model. 

\begin{figure}[h]
\centering
\includegraphics[width=0.45\textwidth]{images/MilestoneRefinementPattern} 
\includegraphics[width=0.45\textwidth]{images/OrRefinementPattern} 
\caption{Milestone-driven refinement and Or-refinement}
\label{fig_MilestoneRefinementPattern_OrRefinementPattern}
\end{figure}

This process is based on refinement patterns. Each refinement pattern used in the KAOS model will correspond to a refinement step in the Event-B model. Actually the process works with functional "Achieve" goals which are the most commonly used goal type. Those goals have to be formally defined with an assertion of the form $A \Rightarrow \lozenge B $, which says that from a state where $A$ is true, another state where $B$ is true can be reached someday. The supported patterns are the milestone-driven refinement pattern, used when a target condition $B$ can be reached from a current condition $A$ with an intermediate condition $AB$ and the or-refinement pattern, used when a goal can be satisfied in different ways.

\begin{figure}[h]
\centering
\includegraphics[width=0.85\textwidth]{images/Matoussi_Technique} %Image sur la largeur du texte
\caption{Expressing KAOS Goal Models with Event-B: process overview}
\label{fig_Matoussi_Technique}
\end{figure}

The process  in figure \ref{fig_Matoussi_Technique} has two phases: the first one creates an Event-B representation of the goal model. The initial model includes the definition of a context with all the types used for data and the definition of an initial machine. This initial machine represents the root goal of the KAOS model and each refinement in this model has to follow one of the two patterns described here above. Each refinement step in the goal model will correspond to a refinement step of the Event-B machine, so we have a chain of refined machines where each machine will correspond to a "stage" of the goal model. 

The second phase formally derives an Event-B specification that satisfies the requirements expressed in the goal model. To do this, it takes on input the goal model and the Event-B representation of this model created in the first phase. This second phase correspond to the operationalization process that can be performed in KAOS and guaranty that operations preserve all the properties of the goal model. As in the first phase, the initial Event-B model will be defined for the root goal of the model and each refinement in the goal model following one of the two patterns will correspond to a refinement in the Event-B model.

\FloatBarrier
\subsection{First phase}
%%%%%%%%%%%%%%%%%%%%%%%%

Formally speaking, a KAOS goal is seen as a property that the system has to establish:
\begin{center}
Achieve[G] \\
$A \Rightarrow \lozenge B $
\end{center}
This property will be represented as an event in the Event-B model where the premise of the implication is transcribed in the initialization event of the machine and the consequence of the implication is transcribed in the then part of the event \texttt{EvtG} associated to the goal. An execution of this event means that the goal $G$ has been satisfied. The guard of \texttt{EvtG} is set to true to express the fact that at this level the goal could always be achieved. 


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\lstset{
frame=lines,
numbers=none,
captionpos=t, 
caption=KAOS expressed in Event-B: initial machine,
label=lst_Matoussi_initial_machine
}
\begin{lstlisting}[escapechar=\%] 
% \begin{description}
\MACHINE{EventBGoalModel\_level\_0}
\SEES{ModelContext}
\VARIABLES
	\begin{description}
		\Item{ $ Manipulated data $ }
	\end{description}
\INVARIANTS
	\begin{description}
		\nItemX{ inv }{ $ Data types definitions $ }
	\end{description}
\EVENTS
	\INITIALISATION
		\begin{description}
		\BeginAct
			\begin{description}
			\nItemX{ act }{ A  }
			\end{description}
		\EndAct
		\end{description}
	\EVT {EvtG}
		\begin{description}
		\WhereGrd
			\begin{description}
			\nItemX{ grd }{ \True}
			\end{description}
		\ThenAct
			\begin{description}
			\nItemX{ act }{ B }
			\end{description}
		\EndAct
		\end{description}
\END
\end{description} 
% 
\end{lstlisting}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\subsubsection{Milestone-driven refinement}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

When we have a milestone-driven refinement, it means that the parent goal is satisfied when all the sub-goals have been satisfied. The \texttt{EvtG} event of the parent machine is refined into a new event \texttt{EvtG} taking as pre-condition the conjunction of the functional post-conditions of the children. The refinement of goal $G$ following the pattern described in figure \ref{fig_MilestoneRefinementPattern_OrRefinementPattern} will give a machine:

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\lstset{
frame=lines,
numbers=none,
captionpos=t, 
caption=KAOS expressed in Event-B: milestone refinement machine,
label=lst_Matoussi_milestone_ref_machine
}
\begin{lstlisting}[escapechar=\%] 
% \begin{description}
\MACHINE{EventBGoalModel\_level\_1}
\REFINES{EventBGoalModel\_level\_0}
\SEES{ModelContext}
\VARIABLES
	\begin{description}
		\Item{ $ Manipulated data $ }
	\end{description}
\INVARIANTS
	\begin{description}
		\nItemX{ inv }{ $ Data types definitions $ }
	\end{description}
\EVENTS
	\INITIALISATION
		\begin{description}
		\BeginAct
			\begin{description}
			\nItemX{ act }{ A \land AB  }
			\end{description}
		\EndAct
		\end{description}
	\EVT {EvtG1}
		\begin{description}
		\WhereGrd
			\begin{description}
			\nItemX{ grd }{ \True}
			\end{description}
		\ThenAct
			\begin{description}
			\nItemX{ act }{ AB }
			\end{description}
		\EndAct
		\end{description}
	\EVT {EvtG2}
		\begin{description}
		\WhereGrd
			\begin{description}
			\nItemX{ grd }{ \True}
			\end{description}
		\ThenAct
			\begin{description}
			\nItemX{ act }{ B }
			\end{description}
		\EndAct
		\end{description}
	\EVT {EvtG}
	\REF {EvtG}
		\begin{description}
		\WhereGrd
			\begin{description}
			\nItemX{ grd }{ AB \land B }
			\end{description}
		\ThenAct
			\begin{description}
			\nItemX{ act }{ B }
			\end{description}
		\EndAct
		\end{description}
\END
\end{description} 
% 
\end{lstlisting}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\subsubsection{Or-refinement}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

When we have an or-refinement, it means that the parent goal is satisfied when one or more of the sub-goals have been satisfied. The \texttt{EvtG} event of the parent machine is refined into a new event \texttt{EvtG}' taking as pre-condition a formula expressing that one or more of the two sub-goals have been satisfied. It does not seem to be a generic approach here and the knowledge and competence of the analyst will play an important role. For instance in the case described by Matoussi et al. in \cite{Gervais2009 }, the guard of a refined \texttt{EvtG}' event uses the union of two sets, one for each of the sub-goals and compare it to the set of all the elements:
\begin{center}
\dots $ \wedge  LocalisedElements = (LocalisedByGPSElements \bunion LocalisedByWIFIElements)  \wedge $ \dots
\end{center}

\subsection{Second phase}
%%%%%%%%%%%%%%%%%%%%%%%%%

In the second phase, functional and non-functional goals are treated the same way. The main idea here is to say that an operation can be executed while the associated goal has not been satisfied (considering the non-functional properties too), which is the same as while it's post-condition has not been verified. However, this is not sufficient to ensure that an "Achieve" goal has been reached. A new event called "closing" is added with a guard equals to the post-condition (without the non-functional properties) of the goal to reach. So for the initial machine corresponding to the root goal $G$ we will have an event \texttt{EvtOpG} that can be executed while $G$ has not been reached and an event \texttt{Closing} that can be executed when $G$ is satisfied. This \texttt{Closing} event will finalize the system. As in the first phase, the machine will be refined fallowing the refinement pattern used in the goal model and each level in the goal model will correspond to a machine in the Event-B model.

Note that in their example, Matoussi et al. in \cite{Gervais2009} are working with sets and express the negation of the initial goal post-condition with universal quantifiers. The initial machine for goal $G$ will be:

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\lstset{
frame=lines,
numbers=none,
captionpos=t, 
caption=Operationalization Event-B: initial machine,
label=lst_Matoussi_milestone_ref_machine
}
\begin{lstlisting}[escapechar=\%] 
% \begin{description}
\MACHINE{EventBOperationalSpecification\_level\_0}
\SEES{ModelContext}
\VARIABLES
	\begin{description}
		\Item{ $ Manipulated data $ }
	\end{description}
\INVARIANTS
	\begin{description}
		\nItemX{ inv }{ $ Data types definitions $ }
	\end{description}
\EVENTS
	\INITIALISATION
		\begin{description}
		\BeginAct
			\begin{description}
			\nItemX{ act }{ A}
			\end{description}
		\EndAct
		\end{description}
	\EVT {EvtOpG}
		\begin{description}
		\WhereGrd
			\begin{description}
			\nItemX{ grd }{ \lnot B }
			\end{description}
		\ThenAct
			\begin{description}
			\nItemX{ act }{ $ Do something that makes things going further $ }
			\end{description}
		\EndAct
		\end{description}
	\EVT {Closing}
		\begin{description}
		\WhereGrd
			\begin{description}
			\nItemX{ grd }{ $ B without non-functional properties $ }
			\end{description}
		\ThenAct
			\begin{description}
			\nItemX{ act }{ Exit \bcmeq OK }
			\end{description}
		\EndAct
		\end{description}
\END
\end{description} 
% 
\end{lstlisting}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

As in the first phase, the initial model will be refined according to the refinement patterns used in the goal model. The Closing event is taken as it and the sub-goals will be translated to events like in the machine here over. 

\subsubsection{Milestone-driven refinement}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

When a parent goal $G$ is refined into sub-goals $G_{1},...,G_{n}$ according to the milestone-driven refinement pattern, it means that the goal $G$ can be decomposed into $n$ steps and that $G$ is satisfied if the final step $G_{n}$ is reached. The sub-machine will thus have \texttt{EvtOpG1,...,EvtOpGn} declared events where the pre-condition is the negation of the post-condition of the corresponding \texttt{EvtGi} event in the Event-B model of phase one and the action is something that makes things going further to the step $G_{i+1}$. The realization of the last sub-goal $G_{n}$ implies the realization of the patent goal $G$, so the last event \texttt{EvtOpG3} will refine the \texttt{EvtOpG} event of the parent machine. The refinement of goal $G$ following the pattern described in figure \ref{fig_MilestoneRefinementPattern_OrRefinementPattern} will give a machine:

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\lstset{
frame=lines,
numbers=none,
captionpos=t, 
caption=Operationalization Event-B: initial machine,
label=lst_Matoussi_milestone_ref_machine
}
\begin{lstlisting}[escapechar=\%] 
% \begin{description}
\MACHINE{EventBOperationalSpecification\_level\_1}
\REFINES{EventBOperationalSpecification\_level\_0}
\SEES{ModelContext}
\VARIABLES
	\begin{description}
		\Item{ $ Manipulated data $ }
	\end{description}
\INVARIANTS
	\begin{description}
		\nItemX{ inv }{ $ Data types definitions $ }
	\end{description}
\EVENTS
	\INITIALISATION
		\begin{description}
		\BeginAct
			\begin{description}
			\nItemX{ act }{ A}
			\end{description}
		\EndAct
		\end{description}
	\EVT {EvtOpG1}
		\begin{description}
		\WhereGrd
			\begin{description}
			\nItemX{ grd }{ \lnot AB }
			\end{description}
		\ThenAct
			\begin{description}
			\nItemX{ act }{ $ Do something that makes things going further $ }
			\end{description}
		\EndAct
		\end{description}
	\EVT {EvtOpG2}
	\REF {EvtOpG}
		\begin{description}
		\WhereGrd
			\begin{description}
			\nItemX{ grd }{ \lnot B }
			\end{description}
		\ThenAct
			\begin{description}
			\nItemX{ act }{ $ Do something that makes things going further$ }
			\end{description}
		\EndAct
		\end{description}
	\EVT {Closing}
	\REF {Closing}
		\begin{description}
		\WhereGrd
			\begin{description}
			\nItemX{ grd }{ $ B without non-functional properties $ }
			\end{description}
		\ThenAct
			\begin{description}
			\nItemX{ act }{ Exit \bcmeq OK }
			\end{description}
		\EndAct
		\end{description}
\END
\end{description} 
% 
\end{lstlisting}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\subsubsection{Or-refinement}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

As for phase one, when we have an or-refinement, it means that the parent goal is satisfied when one or more of the sub-goals have been satisfied. The \texttt{EvtOpG} event of the parent machine is refined into a new event \texttt{EvtOpG}' taking as pre-condition the negation of the corresponding event in the Event-B model of phase one, possibly simplified and where possible ambiguities have been removed. 

The two sub-goals are handled as in the general case by having a pre-condition equals to the negation of the post condition of the corresponding event in the model coming from phase one.


