| 中文摘要 | 第1-4页 |
| ABSTRACT | 第4-9页 |
| 第一章 绪论 | 第9-15页 |
| ·研究背景及意义 | 第9-11页 |
| ·国内外研究现状 | 第11-12页 |
| ·本文研究内容 | 第12-14页 |
| ·本文组织结构 | 第14-15页 |
| 第二章 UML 与形式化方法概述 | 第15-32页 |
| ·统一建模语言UML | 第15-21页 |
| ·形式化方法与OBJECT-Z 语言 | 第21-29页 |
| ·面向对象的形式化语言PERFECT | 第29-31页 |
| ·本章小结 | 第31-32页 |
| 第三章 基于UML 需求建模的OBJECT-Z 描述 | 第32-41页 |
| ·UML 类图简介 | 第32-33页 |
| ·UML 类图语法的OBJECT-Z 定义 | 第33-37页 |
| ·类 | 第33-35页 |
| ·关联 | 第35-36页 |
| ·关联类 | 第36-37页 |
| ·泛化 | 第37页 |
| ·类图 | 第37页 |
| ·UML 类图语义的OBJECT-Z 定义 | 第37-39页 |
| ·UML 类图到OBJECT-Z 的转换 | 第39-40页 |
| ·本章小结 | 第40-41页 |
| 第四章 基于PERFECT 的OBJECT-Z 描述的精化 | 第41-48页 |
| ·软件描述的精化及其分类 | 第41-43页 |
| ·OBJECT-Z 描述的精化 | 第43-47页 |
| ·Perfect 精化Object-Z 描述 | 第43-44页 |
| ·Object-Z 到Perfect 的转换规则 | 第44-47页 |
| ·本章小结 | 第47-48页 |
| 第五章 实例系统应用一 | 第48-58页 |
| ·人事系统的需求分析 | 第48页 |
| ·人事系统的UML 用例图 | 第48-49页 |
| ·人事系统的UML 类图 | 第49页 |
| ·人事系统需求模型的描述与精化 | 第49-57页 |
| ·本章小结 | 第57-58页 |
| 第六章 实例系统应用二 | 第58-65页 |
| ·自动检票系统的需求分析 | 第58页 |
| ·自动检票系统的UML 用例图 | 第58-59页 |
| ·自动检票系统的UML 类图 | 第59页 |
| ·自动检票系统需求模型的描述与精化 | 第59-64页 |
| ·本章小结 | 第64-65页 |
| 第七章 总结与展望 | 第65-67页 |
| ·本文工作总结 | 第65-66页 |
| ·进一步展望 | 第66-67页 |
| 参考文献 | 第67-71页 |
| 攻读硕士学位期间发表的论文 | 第71-72页 |
| 致谢 | 第72页 |