# 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
If the union of the scenario paths of modules provides multiple valid paths, a complete CDFD graph can be formed. It is called a matchable path. The matching of multiple process scenario paths in the feature can be regarded as the input and output of multiple sets aligned one by one. Therefore, the connection between paths is judged based on the data flow, and path matching is performed to form a complete scenario path operation. Before the integration operation, the validity needs to be checked for each path. For two adjacent functional scenario paths, a post-condition that cannot be mapped to another pre-condition is an invalid path, that is \(\forall_{FSPath_{m_{f1}},FSPath_{m_{fj}}\subseteq\text{FSPath}_{m_{fj}}} \cdot\exists_{\text{post}}\exists_{\text{post}}\exists_{m_{f_{1}}}\omega_{ \text{pre}}\mathbb{P}_{m_{fj}}\). Note that some checks, such as path checks related to data flow, may be conducted automatically by the tool, but having a manual check may reveal subtle defects that the machine cannot find. For example, in the ATM case [42], the user's withdrawal operation changes from _Receive_Command_ to _Withdraw_, thus the data will not flow to the query balance. Such a mistake is hardly recognized by machines, but human beings can find it. In terms of feature behavior, features will interact through both a database information exchange and process scenario path exchange. The database exchange means that the data stream of one operation will be read into the database, and the data stream of another operation will be written to the same database. This kind of information exchange is usually retained in the integrated features, and the module remains formally unchanged. In a simple case, the path matching needs to satisfy whether the connection between different port variables of the process be matched. The conditions are as follows:  
\[\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}\]3  
\[\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}\]4\[ \begin{split}\exists_{F\text{s}Path_{m_{f_{1}}\in F}Path_{m_{f_{1}} \in F}Path_{m_{f_{2}}\in F}Path_{m_{f_{2}}}}\cdot F\text{s}Path_{m_{f_{i}}} \
eq F\text{s}Path_{m_{f_{j}}}\\ \wedge(iPort(P_{m_{f_{i}}})\subseteq oPort(P_{m_{f_{j}}})\lor iPort(P _{m_{f_{j}}})\subseteq oPort(P_{m_{f_{j}}}))\end{split}  \tag{14}\]  
Condition 1 states that, for the functional scenario paths of different features \(f_{1}\) and \(f_{2}\), if a set of inputs and outputs are the same, the scenario paths are matchable. Condition 2 states that if the set of input variables of the functional scenario path of feature \(f_{1}\) is a subset of the output variables of another \(f_{2}\) or vice versa, it is intuitive to assume that they are related and can be matched. Considering that there are multiple ways to connect the scenario, the connection of the complex scenario path can be divided into three cases, as shown in Figure 7. Figure 7 is the sequential path of scenario connections because the conditional process B will only be fired after the scenarios of processes A1, A2,..., An are all satisfied. It can be formally expressed as \((\text{pre}_{A1}\wedge\text{post}_{A1}(v_{1}))\wedge(\text{pre}_{A2}\wedge \text{post}_{A2}(v_{2}))\wedge\cdots\wedge(\text{pre}_{An}\wedge\text{post}_{An }(v_{n}))\Rightarrow\text{pre}_{B}\) where each \(\text{post}_{Ai}(v_{i})(i=1,\cdots,n)\) is a sub-logical expression of the postcondition \(\text{post}_{Ai}\), representing a component of one of the scenarios of process \(A_{i}\).