# Product Model Derivation from Feature Model and Formal Specification
## 4 Supporting Tool and Case Study
### Case Study  
We have conducted case studies with four product family models and the corresponding formal specifications (including the Online Shopping System (OSS), Beverage Vending Machine System (BVMS), Hotel Room Reservation (HRR), and Tourism Management System (TMS)). In these case studies, we import the feature model and feature specification of the selected features and obtain the feature integration order through the support tool. The tool guides us to integrate the feature pair specification in order, and we judge the scenario path with the partial assistance of the tool and analyze whether the integration results are reasonable. If it meets our expectations, we perform the integration of the next feature pair, repeat the above steps, and obtain the formal specification of the specific product. Specifically, as shown in Table 3,  
* The OSS product family has 14 features, the user selects 9 features, and these features contain 12 processes, of which the declaration integration used the rules 4, 5, and 6 in Table 1, and 5 paths are effectively matched. The final product's formal specification was as expected. * The BVMS product family has 11 features, and the user selects 7 features, including 7 processes. Since the function is relatively simple, there is no declaration integration involved, and there are two valid paths matching obtain. The effect of the formalized specification of the product is not obvious. * The HRR product family has 9 features, and the user selects 6 features, of which the rules 4 and 6 about Composite and Set collections in Table 1 are used in declaration integration, and 4 paths are effectively matched. The final product's formal specification is as expected. Figure 8: A snapshot of the tool. * The TMS product family has 11 features. The user selects 5 of them, the declaration integration applies rules 4 and 6, and 4 paths are effectively matched. The final product's formal specification is as expected. We illustrate our approach in detail with a simplified product derivation process of the TMS product family (Figure 1) and its formal specification. The case study aims to illustrate how our approach integrates the feature specifications through a sequence of scenario paths and guides the user to construct a comprehensive description of a specific product. According to the proposed approach, the feature model of the specific product and the formal specification of the product family is used as input. Since our method is applicable to the process from the product family to a specific product, the integration of feature specifications is usually conducted after the product configuration is completed. The selected features are shown in Figure 9.  
Based on the feature model structure and Integration Ordering algorithm, starting from the top root node, all nodes will be traversed to find non-leaf nodes. Then merge all the leaf nodes under the non-leaf nodes until the root node is merged. The resulting order is [ReserveforFlight, ReserveforBus, Login, Register, UpdateProfile]. We need to integrate the types and variables in the declaration first. Some feature specification declarations have great similarities. They do not involve the intersection of data and information, and the fusion results are not particularly obvious. Here, we list the declaration integration of two features, _Login_ and _ReserveforBus_. The type variable that module _Login_ contains has the basic information of the user (_id_, _pass_no_, _status_, _phone_no_, etc. ), module _ReserveforBus_ has type variables (_id_, _pass_no_, _card_name_, etc.). The variable _Customer_ is a composite type in the two modules, including the common variables _user_id_ and _pass_no_. The declaration integration needs to satisfy the composite type integration rules in Table 1, namely \(comp(Customer_{Login\_ReserveforBus})=Customer_{Login\_union\_Customer_{ReserveforBus}}\). Only one is retained after integrating the same variables in the two modules \(ReserveforBus\) and \(Login\).