| 摘要 | 第1-5页 |
| ABSTRACT | 第5-11页 |
| 第一章 绪论 | 第11-18页 |
| (一) 研究背景 | 第11-12页 |
| (二) 国内外研究现状 | 第12-16页 |
| ·需求分析工具的研究现状和发展趋势 | 第12-14页 |
| ·形式化方法的研究现状 | 第14-16页 |
| ·有限自动机 | 第14-15页 |
| ·状态图 | 第15页 |
| ·Petri网 | 第15-16页 |
| ·Π演算品 | 第16页 |
| (三) 研究内容 | 第16-17页 |
| (四) 论文结构 | 第17页 |
| (五) 本章小节 | 第17-18页 |
| 第二章 基于用户场景的需求引出 | 第18-27页 |
| (一) 研究背景 | 第18-20页 |
| ·场景的基本概念 | 第18页 |
| ·场景的一般分类 | 第18-19页 |
| ·场景的优、缺点描述 | 第19-20页 |
| (二) 用于场景描述的MSC介绍 | 第20-21页 |
| ·MSC的基本概念 | 第20页 |
| ·MSC的主要元素 | 第20-21页 |
| ·MSC的形式化描述 | 第21页 |
| (三) 用于状态转化的PTA介绍 | 第21-22页 |
| ·前缀树识别器(PTA)简介 | 第21-22页 |
| (四) MSC-场景的需求引出概述 | 第22-26页 |
| ·从用户的需求描述生成MSC图 | 第22-23页 |
| ·从MSC生成前缀树识别器 | 第23-26页 |
| ·MSC中状态与消息的属性与关系 | 第23-24页 |
| ·生成前缀树识别器的算法描述 | 第24-26页 |
| (五) 本章小节 | 第26-27页 |
| 第三章 行为建模技术研究 | 第27-52页 |
| (一) 研究背景 | 第27-28页 |
| ·行为建模引出 | 第27页 |
| ·标号迁移系统(LTS)概念 | 第27-28页 |
| (二) 基于用户场景的LTS建模过程描述 | 第28-51页 |
| ·从需求规约到最终代码的合成步骤 | 第28-45页 |
| ·合并PTA状态的算法 | 第29-37页 |
| ·通过合并PTA状态查找隐含场景 | 第37-41页 |
| ·将全局LTS投射到局部组件的算法 | 第41-42页 |
| ·根据局部LTS构造组件的实现 | 第42-45页 |
| ·根据目标系统对原型进行迭代 | 第45-51页 |
| ·原型系统迭代的原理 | 第45页 |
| ·根据目标系统修改原型 | 第45-48页 |
| ·挖掘子状态与进一步探测隐含场景 | 第48-51页 |
| (三) 本章小节 | 第51-52页 |
| 第四章 自动售票(电影票)机系统实例的需求引出及行为建模 | 第52-68页 |
| (一) 自动售票(电影票)机简介 | 第52-53页 |
| (二) 自动售票(电影票)机主要功能描述 | 第53-55页 |
| (三) 自动售票机部分场景的消息序列图描述 | 第55-60页 |
| (四) 从自动售票机部分场景合成的PTA | 第60-61页 |
| (五) 从自动售票机的PTA合成LTS | 第61-63页 |
| (六) 自动售票(电影票)机模型的实施 | 第63-67页 |
| (七) 方案概括 | 第67页 |
| (八) 本章小节 | 第67-68页 |
| 第五章 结束语 | 第68-70页 |
| (一) 主要工作 | 第68页 |
| (二) 未来工作 | 第68-70页 |
| 参考文献 | 第70-72页 |
| 致谢 | 第72-73页 |
| 攻读学位期间发表的论文 | 第73-75页 |