# Product Model Derivation from Feature Model and Formal Specification
## 3 Product Derivation Based on Feature Model and Specification Approach
### Sofl  
SOFL, standing for Structured Object-Oriented Formal Language, is a formal engineering method. A SOFL specification is usually composed of modules that are associated with CDFDs (Condition Data Flow Diagrams). CDFDs are designed in a hierarchy to describe the architecture of the system under design, while the components are used in each CDFD, such as data flows, data stores, and processes. Each process is described in preconditions and postconditions, where the preconditions can be used to describe constraints on input, and postconditions can be used to describe functions on output data. Different processes are linked to each other by data [40]. Figure 2 shows the basic structure of the formal specification to reflect the relationship between module, CDFD, and process. For example, module A1 consists of A11 and A12, CDFD A1 represents the behavior of module A1, and module A1 encapsulates the data in CDFD A1 (const; type; class; var; inv;) and process (A11, A12), which together form the specification of SOFL. A process in SOFL is the most basic unit that constitutes a module, and a module is formed by integrating a group of processes. Each process is responsible for performing an action, task, or operation, it accepts input and produces output, and different processes are connected through data. Figure 3 is the basic structure diagram of a \(Check\_Pass\) process and the corresponding formal specification. To explain the basic concepts involved in our discussion, we have simplified the original version of the process specification to the extent that we believe ensures a good understandability. A process consists of five parts: name, input ports, output ports, preconditions, and postconditions. In the middle of the box is the name of the process. The input port on the left side of the graphical representation receives three input data flow \(sel\) (customer selection), \(pass\_no\) (the password provided by the customer to access his account), \(id\) (the account number provided by the customer), while the three on the right output ports are used to connect different output data flow, allowing users to enter the next stage to perform different operations. For example, the \(Check\_Pass\) process is intended to verify the customer's account and password through the database for further operations, and the output data flows of different ports cannot be valid at the same time. Different outputs are obtained according to different conditions. Details of the conditions are given in the formal specification of the process. The reader who wishes to understand more details of SOFL can refer to [40] for extensive reading. The formal definitions of the key elements in SOFL are given. Figure 2: The framework of a SOFL specification. **Definition 1**. : _A SOFL process \(p\) is a 4-tuple \((1 Port,OPort,preP,postP)\), where \(1 Port=\{iPort_{1},...iPort_{m}\}\) is the set of input ports of \(p\), where each \(iPort_{i}=\{iv_{i1},...,iv_{il}\}\) is a set of input variables, \(OPort=\{oPort_{1}...oPort_{n}\}\)is the set of output ports of \(p\) where each \(oPort_{j}=\{o_{\gamma_{1}},...,o_{\gamma_{k}}\}\)is a set of output variables. The preP is a constraint on the input, and postP is the relationship between input and output. Each preP and postP exists as a union of multiple predicate expressions._  
A process \(P=(1 Port,OPort,preP,postP)\) as \(P=\{P_{ij}|1\leq i\leq m,1\leq j\leq n\}\), \(P_{ij}=(iPort_{i},oPort_{j},preP_{ij},postP_{ij})\), where \(preP_{ij}=preP,postP_{ij}=postP\). The execution of the process consumes all the input data flows \(iv_{11},...,iv_{il}\) connected to the available input port \(iPort_{i}\) for activating the execution, and makes exactly one of the output ports \(postP_{ij}\) available. Therefore, all the output data flows \(ov_{1j},...,ov_{jk}\) connected to \(oPort_{j}\) become available. This part will become clearer as the discussion on the functional scenario path of a feature and its specification progresses. **Definition 2**.