基于谓词逻辑的需求追踪方法研究

摘要

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

目录

封面

声明

中文摘要

英文摘要

目录

缩略词

第一章 绪论

1.1课题研究背景

1.2国内外研究现状及选题依据

1.3论文组织结构

第二章 基于谓词逻辑的需求追踪方法

2.1可追踪性

2.2谓词逻辑

2.3基于谓词逻辑的需求追踪框架

2.4本章小结

第三章 支持需求追踪的语义模型

3.1基于谓词逻辑的符号系统

3.2需求间追踪关系语义

3.3需求与设计间可满足关系语义

3.4本章小结

第四章 基于语义模型的追踪关系推导及检验

4.1需求关系到公式关系的映射

4.2需求间隐含追踪关系的推导

4.3需求关系的一致性检验

4.4需求与状态图元素间可满足关系的约束规则

4.5本章小结

第五章 需求追踪原型工具的设计与实现

5.1需求追踪工具系统设计

5.2主要模块实现

5.3襟缝翼控制单元案例分析

5.4本章小结

第六章 总结与展望

6.1论文工作总结

6.2未来工作展望

参考文献

致谢

在学期间的研究成果及发表的学术论文