# Product Model Derivation from Feature Model and Formal Specification
## 3 Product Derivation Based on Feature Model and Specification Approach
### Product Model Derivation Approach
#### 3.3.2 Behavior Preserving Integration
\begin{table}
\begin{tabular}{c c c c} \hline \hline
**No.** & **Types** & **Conditions** & **Actions** \\ \hline
1 & Map & s1 = {a1\(\rightarrow\)b1, a2\(\rightarrow\)b2,..., an\(\rightarrow\)bn} s2 = {b1, b2,..., bn} & rng(s1) = s2 \\
2 & Map & s1 = {a1\(\rightarrow\)b1, a2\(\rightarrow\)b2,..., an\(\rightarrow\)bn} s2 = {a1, a2,..., an} & dom(s1) = s2 \\
3 & Map & s1 inter s2 not empty & comp(s) = union(s1, s2) \\
4 & Set & s1 inter s2 not empty & set s = s1 union s2 \\
5 & Sequence & s1 concatenated s2 & sequence s = conc(s1, s2), \\
6 & Composite & s1 inter s2 not empty & comp(s) = s1 union s2 \\ \hline \hline \end{tabular}
\end{table} 
Table 1: Rules for declaration integration based on composite type expressions. \[\exists_{p_{i},\cdots,p_{j}\in P_{m}}\cdot(\exists_{m\in[i,j-1]}\cdot \
exists_{IPort(p_{m})\cup T\times L\to O\mathit{Port}(p_{j})\cup T}) \tag{2}\] \[\forall_{oPort_{j}\in O\mathit{Port}(p_{j})iPort_{i}\in IPort(p_{i+1 })}\cdot oPort_{j}\cup iPort_{i}\
eq\emptyset \tag{3}\]  
The first condition means that there is no process in the path whose output is an input to \(p_{i}\), and the second condition implies no process whose input is from \(p_{j}\). The third condition indicates that each process should be connected to other processes with their input or output ports in the path. All paths connect processes \(P_{ij}\) and \(P_{mm}\), which are denoted by \(Path(p_{ij},p_{mm})\). The process \(P_{mm}\) is obtained from the input of the \(nth\) port of a process \(p\) in the module to the output of the \(mth\) port. A path can have one or more subpaths in the module. Definition 5: Given two paths, \(Path(i,j)\) and \(Path(m,n)\), where \(Path(i,j)\) is a subpath of \(Path(m,n)\), denoted as \(Path(p_{i},p_{j})\subseteq Path(p_{m},p_{n})\), iff  
\[\exists_{x\in[m,n]}\cdot\exists_{O\mathit{Port}(p_{x})\cup T\times L \to IPort(p_{i})\cup T} \tag{4}\] \[\exists_{y\in[m,n]}\cdot\exists_{Iport(p_{j})\cup T\times L\to O \mathit{Port}(p_{y})\cup T} \tag{5}\]  
Each module corresponds to a set of functional scenario paths. All functional scenarios of a process \(p\), denoted as \(Fs_{p}\), have a functional scenario path, which is defined as follows:  
Definition 6: A functional scenario path is a sequence \([fs_{1},\cdots,fs_{n}]\) in the module \(m\), iff  
\[\exists_{[p_{1},\cdots,p_{n}]\in\mathrm{Path}_{m}(p_{1},p_{n})}\cdot\exists_{ p_{1},p_{n}\in P_{m}}\cdot\forall_{i\in[1,n]}\cdot\mathrm{fs}_{i}\in\mathrm{Fs}_{p_{ i}} \tag{6}\]  
The functional scenario path, denoted as \(\mathrm{FsPath}\big{(}p_{ij},p_{mm}\big{)}\), reflects the behavior of module \(m_{f}\). The \(m_{f}\) performs different functional scenario paths when receiving different data inputs. For simplicity, we only consider the postcondition in deriving functional scenarios discussed in this paper. All possible functional scenarios \(fs_{i}(i\in\{1,2,\cdots,n\})\) are derived from the formal specification of pairs based on the data dependency among operations \(C_{i}\wedge D_{i}\), and a set of functional scenarios \(\{\mathrm{fs}_{1},\mathrm{fs}_{2},\cdots,\mathrm{fs}_{n}\}\) are obtained, where \(fs_{i}\) is the related functional scenario of \(p\). we use sequence \(\{IV(\mathrm{fs}_{1})\}[\mathrm{fs}_{1}]\{OV(\mathrm{fs}_{1})\}\to\{IV( \mathrm{fs}_{2})\}[\mathrm{fs}_{2}]\{OV(\mathrm{fs}_{2})\}\to\cdots\to\{IV( \mathrm{fs}_{n})\}[\mathrm{fs}_{n}]\{OV(\mathrm{fs}_{n})\}\) for the scenario path. Each \(\{IV(\mathrm{fs}_{n})\}[\mathrm{fs}_{n}]\{OV(\mathrm{fs}_{n})\}\) is a functional scenario. The input \(IV(fs_{1})\) of \(fs_{1}\) comes from the objects outside the module \(m\) and the set \(OV(fs_{1})\) is the outputs of \(fs_{1}\). The process \(P_{ij}\) in the scenario path receives the input data item \(IV(fs_{i})\) and produces a data item \(OV(fs_{i})\), where one or more variables in \(IV(fs_{i})\) are contained in the guard condition, and the variables in \(OV(fs_{i})\) are contained in a defining condition. The functional scenario path of each process \(p\) within \(m_{f}\) will be generated based on the functional scenarios.