支持需求追踪的语义模型

（1）个体变元：表示抽象或泛指的软件制品或制品属性，如：1 ，2 ， ⋯ ，1 ，2 ；（2）二元谓词符号：用于描述个体变元间的关系，如：₁²，₂²， ⋯ ，²；

（3）联接词符号：；

（4）括号与逗号：(、，、)

若定义集合

：描述制品标识符的有限集合；集合：描述制品属性的有限集合；集合：描述有限二元谓词集合；集合：由一元否定联接符构成的集合；集合：括号与逗号的集合，则形式语言Σ的字母集 = { ∪ ∪ ∪ ∪ }

中的公式由字母集及一系列公式生成规则产生

定义

3.2

语言Σ中合式公式ω的生成规则：

（1）ω = ²(，) ∈ Σ，其中(，∈ ∪ )且²∈

（2）ω = ¬²(，) ∈ Σ，其中(，∈ ∪ )且²∈

（3）公式ω只能通过规则（1）、（2）产生。

字母集合={ ²∈ ;，∈ ∪ ; , ()∈E ; ∈K}

公式生成规则：公式ω只能通过规则（1）、（2）产生。

符号化的公式并没有实际的含义，需要结合一个具体的语义模型对公式中的变元符号或谓词符号进行解释。

对于一个给定的项目，定义集合′：表示项目中可唯一标识的有限制品集合，如需求、设

计元素等；定义集合′：表示有限的制品属性集合，如制品的关键度等级、抽象层次等；定义集合：表示实际项目中有限的关系集合，如制品间的关联关系，制品与其抽象层次的对应关系等。则的语义模型由如下几个部分组成：

。

{S,C,P,K,E}具体化后S代表制品，C代表制品的属性，P代表变元之间的关系R。