Decomposition makes it possible to manage the complexity of models that increases through the refinement process. It may be interesting to have an early decomposition to break an initial machine into smaller pieces pertinent with the KAOS agents. This choice is made because the KAOS meta-model says that an association or an attribute can be controlled by one and only one agent \cite{Lamsweerde2009,Landtsheer2007a,Letier2001}. The idea is thus to have separate machines with the attributes monitored and controlled by the agent. Let us recall that an attribute or association is controlled by an agent if the agent performs one or more operation that modifies the attribute value and that an attribute is monitored by an agent if the attribute is an input of one or more operation performed by the agent.

Ball presents in \cite{Ball2008} a description of the two techniques used to split a machine into smaller pieces. The first one, called Event-Based Decomposition encapsulates the variables in different machines together with the events or parts of events that concern those variables. The events that have been split will need to be synchronized in order to ensure the functionalities of the original machine. The synchronization will take place by an exchange of inputs and outputs between the synchronized machines events \cite{Butler2009}.

The second technique, called State-Based Decomposition splits the variables in different machines with some shared variables. Events are added to components to simulate how the shared variables are used in other components. Shared variables and events must be kept synchronized between the different machines during the refinement. Theoretically the system could be rebuilt into a single machine at the end of the process, but in practice this will never be done since the different machines will lead to different software components.

This State-Based Decomposition, proposed by Abrial in \cite{Abrial2009, Abrial2009a, Metayer2005} seems to fit more for our problem. For a general model, variables and events will be distributed to several sub-machines with some of those variables presents in more than one sub-machine. It is important to notice here that the sub-machines are not refining the general machine, but are decomposing it. In the sub-machines, a distinction is made between the internal variables used only in a particular sub-machine and the shared variables used in more than one sub-machine. So, shared variables can be modified by more than one event in more than one sub-machine. Figure \ref{fig_Decomposition_Event_B} shows an example of decomposition, a sub-machine \texttt{A} has an event \texttt{evtA} that will modify the value of a shared variable and another sub-machine \texttt{B} has an event \texttt{evtB} using the variable's value in its guard. To express the fact that the variable is not a constant in \texttt{B}, an event \texttt{evtExtA} will be added to \texttt{B} corresponding to an abstraction of the event \texttt{evtA} in \texttt{A}. The added event \texttt{evtExtA} will be called an external event, which is just present in \texttt{B} to synchronize the update of the shared variable in the general machine. 

\begin{figure}[h]
\centering
\includegraphics[width=0.75\textwidth]{images/Decomposition_Event_B} %Image sur la largeur du texte
\caption{Decomposition of a general machine into two sub-machines}
\label{fig_Decomposition_Event_B}
\end{figure}

It is clear now that shared variables coming from the abstract machine will be replicated in each sub-machine. The problem is that each sub-machine could normally refine its variables and the same replicated variable could be refined in one way in one refinement and in another way in another refinement. If this happens, the two sub-machines can't communicate any longer as they are not using the same convention on the shared variable. Such a variable has a special status in the sub-machines where they stay saying that this variable has to be always present in the state space of any refinement of the machine. A shared variable can thus not be data-refined or if it is, the variable has to be refined in the same way in each sub-model using the variable, which can be quite heavy.

\subsection{State-Based Decomposition}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

We propose to use the State-Based Decomposition after an initial creation of the Event-B model from the KAOS object model, as presented in section \ref{12_04_KAOS_Object_Model_to_Event_B_Context}, with one sub-machine per agent. The reason of this choice is simple, the KAOS meta-model states that an attribute or association cannot be controlled by more than one agent \cite{Lamsweerde2009,Letier2001,Landtsheer2007a}. So it means that in Event-B, a shared variable will be updated in one and only one sub-machine, while an external event will be placed with each variable coming from the KAOS object model in all other sub-machines. 

The question is: do we have to place each variable coming from the KAOS object model in all sub-machines? On one side, if we place the variables coming from the controlled and monitored attributes and associations of the KAOS object model only in the sub-machines representing the concerned agent, the model in its all will be more readable. 
On the other side, decomposition link is for now informal and not implemented in existing tools \cite{RODINv1.1} and have thus to be done manually. Moreover, the re-composition of all sub-machines in one big machine proposed in \cite{Metayer2005}, which could be used at some moment in the development process as a verification of the consistency of the model, could not be done in RODIN since a machine cannot refine more than one other machine. It could thus be interesting to have a more "concrete" decomposition. 

For recall, an external event representing the update of a certain shared variables has to be an abstraction of the concrete event updating the variable in another sub-machine. Since KAOS meta-model impose to have only one agent controlling the update of an attribute or an association, the update of a variable coming from the KAOS object model will not be performed in more than one sub-machine. The idea is to add to the general machine coming from the KAOS object model very general update operations for each variable, and generate from this machine one refinement per agent. The variables that are not controller by the agent will be marked as shared variables and the events updating those variables will be marked as external events in the sub-machines. Those events and variables cannot be refined one the sub-machine or its refinements. All the events that update the controlled variables of the agent will be refinement of the general update event defined in the general machine. The re-composition of sub-machines will be simply a new machine, declared as a refinement of the initial machine generated from the KAOS object model where each non-external events and internal variables coming from the different sub-machines will be simply copy-pasted. By doing so, we guaranty that each external event is indeed an abstraction of the update of a non-controlled shared variable, because of the refinement link. The cost here is to have each shared variables and each abstract update event of the non-controlled variables repeated in each machine and its refinement, whether the corresponding agent is controlling or monitoring the variable or not. This could be simply overcome in the modelling tools by hiding in a sub-machine the variables and corresponding external update events that are not controlled or monitored by the corresponding agent.

\subsubsection{Example}
%%%%%%%%%%%%%%%%%%%%%%%

Here is a small example inspired by the mine pump model presented in \cite{Aziz2009}. In this model we have a mine that has to be kept safe from flooding and explosion. For this we have a mine pump that start pumping if the water level is too high and if there is no methane detected. 

\begin{figure}[h]
\centering
\includegraphics[width=\textwidth]{images/minePump_goal_model} %Image sur la largeur du texte
\caption{Mine pump goal model}
\label{fig_minePump_goal_model}
\end{figure}

\begin{figure}[h]
\centering
\includegraphics[width=0.90\textwidth]{images/minePump_agent_model} %Image sur la largeur du texte
\caption{Mine pump agent model}
\label{fig_minePump_agent_model}
\end{figure}

Figure \ref{fig_minePump_agent_model} presents the goal model and the different agents responsible for the requirements and expectations. Figure \ref{fig_minePump_agent_model} shows the agent model with controlled and monitored objects: the PumpController controls the pump attribute and monitors the methane and waterLevel attributes, the AlarmController controls the bell attribute and monitors the methane attribute, the WaterLevelSensor controls the waterLevelAttribute, the MethaneSensor controls the methane attribute and the Miner monitors the bell attribute.

\FloatBarrier

By applying the procedure described in section \ref{12_04_KAOS_Object_Model_to_Event_B_Context}, we get an initial Context in listing \ref{lst_EVENT_B_MinePump_Example_InitialContext} and an initial machine in listing \ref{lst_EVENT_B_MinePump_Example_InitialMachine} describing the objects of the KAOS object model. The initial machine includes the attributes and the update methods for all those attributes, note here that in the listing \ref{lst_EVENT_B_MinePump_Example_InitialMachine} only the update method for the pump has been shown. The update methods of the others attributes follows the same pattern. The complete machines of this example can be found in annex \ref{Anx_decompo_according_agents_Mine_pump_example}.


\lstset{
frame=lines,
numbers=none,
captionpos=t, 
caption=Mine pump example: Initial context,
label=lst_EVENT_B_MinePump_Example_InitialContext
}
\begin{lstlisting}[escapechar=\%] 
% \begin{description}
\CONTEXT{MineContext}
\SETS
	\begin{description}
		\Item{ ONOFF, LEVEL, MINE\_SET }
	\end{description}
\CONSTANTS
	\begin{description}
		\Item{ ON, OFF, LOW, MEDIUM, HIGH, M }
	\end{description}
\AXIOMS
	\begin{description}
		\nItemX{ axm1 }{ partition(ONOFF, \{ ON\} , \{ OFF\} ) }
		\nItemX{ axm2 }{ partition(LEVEL, \{ LOW\} , \{ MEDIUM\} , \{ HIGH\} ) }
		\nItemX{ axm3 }{ partition(MINE\_SET, \{ M\} ) }
	\end{description}
\END
\end{description}
% 
\end{lstlisting}


\lstset{
frame=lines,
numbers=none,
captionpos=t,
caption=Mine pump example: Initial machine,
label=lst_EVENT_B_MinePump_Example_InitialMachine
}
\begin{lstlisting}[escapechar=\%] 
% \begin{description}
\MACHINE{MinePump}
\SEES{MineContext}
\VARIABLES
	\begin{description}
		\Item{ MINE, pump, bell, methane, waterLevel }
	\end{description}
\INVARIANTS
	\begin{description}
		\nItemX{ inv1 }{ MINE \in  \pow(MINE\_SET) }
		\nItemX{ inv2 }{ pump \in  MINE \tfun  ONOFF }
		\nItemX{ inv3 }{ bell \in  MINE \tfun  BOOL }
		\nItemX{ inv4 }{ methane \in  MINE \tfun  BOOL }
		\nItemX{ inv5 }{ waterLevel \in  MINE \tfun  LEVEL }
	\end{description}
\EVENTS
	\INITIALISATION
		\begin{description}
		\BeginAct
			\begin{description}
			\nItemX{ act1 }{ MINE, pump, bell, methane, waterLevel  :=  \emptyset , \emptyset , \emptyset , \emptyset ,\emptyset  }
			\end{description}
		\EndAct
		\end{description}
	\EVT {updatePump}
		\begin{description}
		\AnyPrm
			\begin{description}
			\ItemX{ m }
			\ItemX{ status }
			\end{description}
		\WhereGrd
			\begin{description}
			\nItemX{ grd1 }{ m \in  MINE }
			\nItemX{ grd2 }{ status \in  ONOFF }
			\end{description}
		\ThenAct
			\begin{description}
			\nItemX{ act1 }{ pump(m) :=  status }
			\end{description}
		\EndAct
		\end{description}
\END
\end{description} 
% 
\end{lstlisting}

Starting from this, machines will be created by refining the initial machine for each agent of the KAOS model. The listing \ref{lst_EVENT_B_MinePump_Example_PumpCtrlMachine} shows the machine defined for the PumpController. This machine and all the other machines of this example can be found  in annex \ref{Anx_decompo_according_agents_Mine_pump_example}. The re-composed machine can also be found in listing \ref{lst_EVENT_B_MinePump_Example_MinePumpReunificationMachine_ANX} in annex \ref{Anx_decompo_according_agents_Mine_pump_example} where the update methods have been replaced by their refinements in the different sub-machines.

\lstset{
frame=lines,
numbers=none,
captionpos=t,
caption=Mine pump example: PumpController machine,
label=lst_EVENT_B_MinePump_Example_PumpCtrlMachine
}
\begin{lstlisting}[escapechar=\%] 
% \begin{description}
\MACHINE{PumpController}
\REFINES{MinePump}
\SEES{MineContext}
\VARIABLES
	\begin{description}
		\Item{ MINE, pump, bell, methane, waterLevel }
	\end{description}
\EVENTS
	\INITIALISATION
		\\\textit{extended}
		\begin{description}
		\BeginAct
			\begin{description}
			\nItemX{ act1 }{ MINE, pump, bell, methane, waterLevel  :=  \emptyset , \emptyset , \emptyset , \emptyset ,\emptyset  }
			\end{description}
		\EndAct
		\end{description}
	\EVT {high\_water\_detected}
	\cmt{ Internal Event }
	\REF {updatePump}
		\begin{description}
		\AnyPrm
			\begin{description}
			\ItemX{ m }
			\end{description}
		\WhereGrd
			\begin{description}
			\nItemX{ grd2 }{ m \in  MINE }
			\nItemX{ grd1 }{ waterLevel(m) = HIGH }
			\nItemX{ grd3 }{ methane(m) = FALSE }
			\end{description}
		\Witnesses
			\begin{description}
			\nItem{ status }{ status = ON }
			\end{description}
		\ThenAct
			\begin{description}
			\nItemX{ act1 }{ pump(m) :=  ON }
			\end{description}
		\EndAct
		\end{description}
	\EVT {low\_water\_detected}
	\cmt{ Internal Event }
	\REF {updatePump}
		\begin{description}
		\AnyPrm
			\begin{description}
			\ItemX{ m }
			\end{description}
		\WhereGrd
			\begin{description}
			\nItemX{ grd1 }{ m \in  MINE }
			\nItemX{ grd2 }{ waterLevel(m) = LOW }
			\end{description}
		\Witnesses
			\begin{description}
			\nItem{ status }{ status = OFF }
			\end{description}
		\ThenAct
			\begin{description}
			\nItemX{ act1 }{ pump(m) :=  OFF }
			\end{description}
		\EndAct
		\end{description}
	\EVT {updateBell}
	\cmt{ External Event }
	\EXTD {updateBell}
		\begin{description}
		\AnyPrm
			\begin{description}
			\Item{ m }
			\Item{ status }
			\end{description}
		\WhereGrd
			\begin{description}
			\nItem{ grd1 }{ m \in  MINE }
			\nItem{ grd2 }{ status \in  BOOL }
			\end{description}
		\ThenAct
			\begin{description}
			\nItem{ act1 }{ bell(m) :=  status }
			\end{description}
		\EndAct
		\end{description}
	\EVT {updateMethane}
	\cmt{ External Event }
	\EXTD {updateMethane}
		\begin{description}
		\AnyPrm
			\begin{description}
			\Item{ m }
			\Item{ status }
			\end{description}
		\WhereGrd
			\begin{description}
			\nItem{ grd1 }{ m \in  MINE }
			\nItem{ grd2 }{ status \in  BOOL }
			\end{description}
		\ThenAct
			\begin{description}
			\nItem{ act1 }{ methane(m) :=  status }
			\end{description}
		\EndAct
		\end{description}
	\EVT {updateWaterLevel}
	\cmt{ External Event }
	\EXTD {updateWaterLevel}
		\begin{description}
		\AnyPrm
			\begin{description}
			\Item{ m }
			\Item{ level }
			\end{description}
		\WhereGrd
			\begin{description}
			\nItem{ grd1 }{ m \in  MINE }
			\nItem{ grd2 }{ level \in  LEVEL }
			\end{description}
		\ThenAct
			\begin{description}
			\nItem{ act1 }{ waterLevel(m) :=  level }
			\end{description}
		\EndAct
		\end{description}
\END
\end{description} 
% 
\end{lstlisting}


