| 摘要 | 第1-8页 |
| ABSTRACT | 第8-10页 |
| 目录 | 第10-14页 |
| 图表目录 | 第14-15页 |
| 表格目录 | 第15-16页 |
| 第一章 绪论 | 第16-27页 |
| ·课题来源 | 第16页 |
| ·概述 | 第16-17页 |
| ·软件需求工程概论 | 第17-20页 |
| ·软件需求工程的发展 | 第17页 |
| ·软件需求的定义 | 第17-18页 |
| ·软件需求的分类 | 第18页 |
| ·软件需求开发过程 | 第18-19页 |
| ·软件需求规格说明描述方法 | 第19-20页 |
| ·软件需求分析技术 | 第20-23页 |
| ·面向对象方法 | 第20页 |
| ·形式方法 | 第20-23页 |
| ·半形式化方法与形式方法的比较 | 第23-24页 |
| ·论文的主要研究内容 | 第24-25页 |
| ·论文大纲 | 第25-26页 |
| ·小结 | 第26-27页 |
| 第二章 语言背景 | 第27-35页 |
| ·概述 | 第27页 |
| ·Z语言和Z语言家族 | 第27-30页 |
| ·Z语言简介 | 第27页 |
| ·Object-Z语言特征 | 第27-29页 |
| ·其它面向对象的Z语言扩充 | 第29-30页 |
| ·Object-Z语言的支持工具 | 第30页 |
| ·UML简介 | 第30-34页 |
| ·UML基本概念 | 第31-32页 |
| ·UML的扩展机制 | 第32页 |
| ·UML的工具支持 | 第32-33页 |
| ·OCL语言简介 | 第33页 |
| ·OCL与Object-Z作为模型约束语言的比较 | 第33-34页 |
| ·小结 | 第34-35页 |
| 第三章 相关的研究工作分析比较 | 第35-43页 |
| ·概述 | 第35页 |
| ·关于方法结合的讨论 | 第35-36页 |
| ·IFAD Rose-VDM++ Link | 第36页 |
| ·结合UML与B的研究工作 | 第36-37页 |
| ·结合UML与Z/Object-Z的主要研究工作 | 第37-41页 |
| ·Synthesis方法 | 第37-38页 |
| ·补充面向对象建模语言(AML) | 第38页 |
| ·ROZ工具 | 第38页 |
| ·Noe以及Hartrum对Rational Rose 98的扩展 | 第38-39页 |
| ·RoZeLink | 第39页 |
| ·France等人的研究工作 | 第39-40页 |
| ·Kim的研究工作 | 第40页 |
| ·其他相关研究工作 | 第40-41页 |
| ·现有工作存在的主要问题 | 第41-42页 |
| ·小结 | 第42-43页 |
| 第四章 从UML模型到Object-Z规格说明的转换 | 第43-61页 |
| ·概述 | 第43-44页 |
| ·面向对象模型形式化方法概述 | 第43-44页 |
| ·UML类图的形式化 | 第44-49页 |
| ·UML类图简介 | 第44-45页 |
| ·UML类的形式化 | 第45-46页 |
| ·关系的形式化 | 第46页 |
| ·继承关系的形式化 | 第46-47页 |
| ·关联的形式化 | 第47-48页 |
| ·关联类的形式化 | 第48-49页 |
| ·系统类的形式化 | 第49页 |
| ·UML状态图的形式化 | 第49-51页 |
| ·UML状态图简介 | 第49页 |
| ·从状态图到Object-Z规格说明的转换 | 第49-51页 |
| ·UML用例图的形式化 | 第51-54页 |
| ·用例图简介 | 第51页 |
| ·使用顺序图实现用例图中的各个用例 | 第51-52页 |
| ·形式化顺序图 | 第52-53页 |
| ·用例图的形式化 | 第53页 |
| ·用例图的形式化过程 | 第53-54页 |
| ·UML约束条件的形式化 | 第54-60页 |
| ·预定义的基本类型 | 第54-56页 |
| ·集(Collection)类型 | 第56-58页 |
| ·迭代操作的转换 | 第58-59页 |
| ·从OCL表达式到Object-Z表达式的转换 | 第59-60页 |
| ·小结 | 第60-61页 |
| 第五章 实例研究 | 第61-73页 |
| ·概述 | 第61页 |
| ·问题描述 | 第61-62页 |
| ·UML建模 | 第62-65页 |
| ·UML类图模型 | 第62-63页 |
| ·UML状态图模型 | 第63-64页 |
| ·增加OCL约束条件 | 第64-65页 |
| ·从UML模型到Object-Z规格说明 | 第65-68页 |
| ·Object-Z模型的一般检查验证方法 | 第68-70页 |
| ·类局部定义的一致性 | 第68-69页 |
| ·状态模式一致性检查验证 | 第69页 |
| ·类初始化状态存在性检查验证 | 第69页 |
| ·操作模式的一致性检查验证 | 第69-70页 |
| ·规格说明性质的检查验证 | 第70页 |
| ·电梯模型的检查验证 | 第70-72页 |
| ·状态模式一致性检查验证 | 第70-71页 |
| ·初始状态存在性检查验证 | 第71页 |
| ·操作模式一致性检查验证 | 第71页 |
| ·电梯系统的性质的证明 | 第71-72页 |
| ·小结 | 第72-73页 |
| 第六章 UMLFormalizer的设计与实现 | 第73-83页 |
| ·概述 | 第73页 |
| ·XMI技术简介 | 第73-75页 |
| ·UMLFormalizer的系统结构图 | 第75-77页 |
| ·XMI文件的解析 | 第75-77页 |
| ·XML格式的Object-Z文件存储格式定义 | 第77-81页 |
| ·XML结构的说明 | 第78页 |
| ·相关研究工作介绍 | 第78-79页 |
| ·类 | 第79-80页 |
| ·变量定义 | 第80页 |
| ·操作 | 第80-81页 |
| ·UMLFormalizer功能简介 | 第81-82页 |
| ·小结 | 第82-83页 |
| 第七章 Object-Z动画技术的研究 | 第83-97页 |
| ·介绍 | 第83页 |
| ·规格说明动画的本质 | 第83-84页 |
| ·相关的研究工作 | 第84-85页 |
| ·SICStus Prolog语言简介 | 第85-86页 |
| ·Object-Z类模式的转换 | 第86-89页 |
| ·Object-Z类 | 第86页 |
| ·基本类型实例化 | 第86-87页 |
| ·类常量 | 第87页 |
| ·状态模式 | 第87-89页 |
| ·Object-Z集合理论的Prolog谓词实现 | 第89-92页 |
| ·有限集合以及集合操作 | 第89-90页 |
| ·序偶和关系 | 第90-91页 |
| ·函数 | 第91-92页 |
| ·转换规则的描述 | 第92页 |
| ·OZAnimator-Object-Z动画模拟系统的功能介绍 | 第92-95页 |
| ·实例研究 | 第95-96页 |
| ·小结 | 第96-97页 |
| 第八章 结束语 | 第97-99页 |
| ·本文研究工作的总结 | 第97页 |
| ·本文的主要创新之处 | 第97-98页 |
| ·进一步研究工作展望 | 第98-99页 |
| 参考文献 | 第99-109页 |
| 作者攻读学位期间公开发表的论文及参加的科研工作 | 第109-111页 |
| 致谢 | 第111页 |
