嵌入式软件在航空、核能及交通等安全关键领域应用广泛,保障其安全性至关重要。在软件开发过程中维持软件制品间的可追踪性是保障软件安全性面临的一个重要挑战。当前的可追踪性研究主要存在两个问题:一方面,可追踪性研究主要集中在需求与代码、设计与代码间,缺乏需求间、需求与设计间的可追踪性研究;另一方面,主流的追踪关系建立方法如基于信息检索的关系恢复等,所建立的追踪信息精确性和完整性不高,往往无法有效应用于安全关键领域的软件开发。针对上述问题,本文提出一种基于谓词逻辑的、描述需求间以及需求与设计间追踪信息的语义模型。基于该语义模型,可以实现追踪关系的自动推导和检验,保证追踪关系的精确和完整。论文的主要研究内容包括:(1)构造了支持需求追踪的语义模型。首先定义了一个基于谓词逻辑的符号系统描述制品间的追踪信息,并分别给出了需求间依赖、精化、分解和冲突关系的语义,以及需求与状态图间的可满足关系语义。(2)基于语义模型,给出追踪关系的推导和检验方法。通过分析关系语义,给出需求间隐含关系的推导、关系的一致性检验规则,并设计了自动推导和检验算法。此外,给出支持需求与设计间可满足关系推导和检验的约束规则。(3)根据本文所提出的方法,设计并实现了支持需求追踪的原型工具,该工具可建模制品间的追踪信息,实现对追踪关系的分析,并结合一个应用实例说明本文方法的可行性和有效性。