| 摘要 | 第1-5页 |
| Abstract | 第5-6页 |
| 目录 | 第6-8页 |
| 第一章 绪论 | 第8-12页 |
| ·研究背景 | 第8-9页 |
| ·研究现状 | 第9-10页 |
| ·论文的研究内容及主要工作 | 第10-11页 |
| ·论文组织结构 | 第11-12页 |
| 第二章 相关技术 | 第12-26页 |
| ·面向方面技术 | 第12-21页 |
| ·面向方面编程 | 第12-13页 |
| ·面向方面的软件开发 | 第13-14页 |
| ·面向方面需求工程方法 | 第14-18页 |
| ·基于场景面向方面需求工程方法 | 第18-21页 |
| ·形式化方法 | 第21-26页 |
| ·形式化方法概述 | 第21-22页 |
| ·形式化方法的研究内容 | 第22页 |
| ·形式化方法的优点和存在的问题 | 第22-24页 |
| ·形式化方法的发展方向 | 第24页 |
| ·B 方法介绍 | 第24-26页 |
| 第三章 NFR-SMA 方法 | 第26-30页 |
| ·方法概述 | 第26页 |
| ·方法的主要步骤 | 第26-30页 |
| ·确定功能性需求和非功能需求 | 第26-27页 |
| ·在用例图的中关联非功能软目标 | 第27页 |
| ·精化用例图并识别功能性横切关注点 | 第27-28页 |
| ·分解非功能软目标 | 第28页 |
| ·精化用例图中连接点处的子软目标并识别非功能性横切关注点 | 第28-30页 |
| 第四章 UML 状态图到 B 方法的转换 | 第30-40页 |
| ·UML 状态图 | 第30-31页 |
| ·状态图各模型元素的 B 方法表示 | 第31-34页 |
| ·状态的表示 | 第31-32页 |
| ·转移的表示 | 第32-33页 |
| ·动作的表示 | 第33页 |
| ·事件的表示 | 第33-34页 |
| ·事件的建模 | 第34-37页 |
| ·聚合同一 B 抽象机中的事件和数据 | 第34-35页 |
| ·实现事件的 B 操作 | 第35-37页 |
| ·建模状态图中的异步通信 | 第37-38页 |
| ·状态图中的通信 | 第37页 |
| ·发送信号 | 第37-38页 |
| ·状态图到形式化 B 方法 | 第38-39页 |
| ·数据的形式化 | 第38页 |
| ·操作的形式化 | 第38页 |
| ·生成 B 规范的体系结构 | 第38-39页 |
| ·小结 | 第39-40页 |
| 第五章 实例应用 | 第40-54页 |
| ·识别方面 | 第40-44页 |
| ·识别功能性需求和非功能需求 | 第40-41页 |
| ·在用例图的非功能需求连接点处关联非功能软目标 | 第41页 |
| ·精化用例图并识别功能性横切关注点 | 第41-43页 |
| ·分解非功能软目标 | 第43-44页 |
| ·精化用例图中连接点处的子软目标并识别非功能性横切关注点 | 第44页 |
| ·识别方面场景与非方面场景 | 第44-46页 |
| ·UML 顺序图到 UML 状态图的转换 | 第46-48页 |
| ·UML 状态图的合成 | 第48-49页 |
| ·UML 状态图到 B 方法的转换 | 第49-53页 |
| ·系统形式规约的模型检测 | 第53-54页 |
| 第六章 总结与展望 | 第54-55页 |
| ·总结 | 第54页 |
| ·展望 | 第54-55页 |
| 参考文献 | 第55-58页 |
| 致谢 | 第58页 |