## 1 Introduction  
Software product line engineering (SPLE) [1; 2; 3; 4] enables the rapid production of software products that satisfy custom needs through the reuse of core software assets. This technique is widely used in industry to achieve a rapid response to market changes. The key issue in software product family engineering is how to manage variability and reuse core software assets on that basis. Software product line variability modeling is the key technology for variability management, and it is an important technique for domain analysis. By examining the commonality and variability of the components in the system, the corresponding product family model is established using abstraction and selection methods. Feature-Oriented Domain Analysis (FODA) [5] is a generic approach to modeling variability in domain analysis. Subsequent studies have investigated the domain analysis method, Feature-Oriented Reuse Method (FORM) [6], based on the FODA method. However, these methods stay at the feature level description and cannot analyze the internal structure of the relevant features. Some approaches try to enhance the understanding of the feature model by describing the function of the features. The functional role of the features in the feature model is observed during the description. Such approaches help to improve the quality of the feature model during the analytical modeling phase of the product. However, these researchers used informal methods in the analysis process, resulting in the inability of using computers to assist in the analysis for efficiency. Feature specifications written using natural language may suffer from contradictions, ambiguities, and incompleteness. Formal methods have been introduced to solve the problems caused by the use of informal methods in the requirements analysis phase of product family feature modeling. Some researchers [7; 8] chose to use Abstract Behavioural Specification (ABS) and UML language to describe the internal structure of the features. The use of formal specification language enables the consistency and completeness of the specification to be checked during the domain analysis phase. Additionally, the formal specification can be transformed into target software according to rules and checked using computer-assisted methods, which reduces problems caused by human factors and improves the quality and reliability of the product family model. However, these works formalized the initial feature model for each feature without considering the connection between the feature model and the feature specification. According to our investigation and practical experience [9; 10], we found that the feature model is likely to undergo the necessary changes during the clarification of the feature. In-depth analysis of features using formal methods often reveals consistency problems with feature models, which suggests that variability analysis and feature requirements clarification processes are related and should not be considered separately. Although there have been studies considering the correlation between the two, there is still a lack of effective methods to obtain product family models taking into consideration the relationship between analytical feature modeling and feature specification. In summary, current software product line engineering faces a number of dilemmas. When extracting specific products from large product line feature models, similarities and functional uncertainties are found between some functional scenarios. For example, the same set of inputs may cause completely different outputs through two functional modules. This is because the analysis of product family feature models is not precise enough, and the acquisition of product family feature models relies on the personal competence of domain experts and lacks the means to improve model quality. There are some researchers who hope to improve the quality of the entire product family feature model by introducing formal methods to describe it.