基于UML类图的B形式化规约研究
| 摘要 | 第1-3页 |
| ABSTRACT | 第3-7页 |
| 1 绪论 | 第7-11页 |
| ·研究背景及意义 | 第7-8页 |
| ·国内外研究现状 | 第8-9页 |
| ·论文的研究内容、主要工作和内容组织 | 第9-11页 |
| ·研究内容和主要工作 | 第9-10页 |
| ·内容组织 | 第10-11页 |
| 2 统一建模语言UML | 第11-20页 |
| ·UML 概述 | 第11-12页 |
| ·UML 的体系结构 | 第12-14页 |
| ·UML 的定义 | 第12页 |
| ·UML 的框架 | 第12-13页 |
| ·模型元素 | 第13-14页 |
| ·UML 的建模机制 | 第14-18页 |
| ·UML 的静态建模 | 第14-16页 |
| ·UML 的动态建模 | 第16-18页 |
| ·通用机制 | 第18页 |
| ·OCL | 第18页 |
| ·UML 存在的问题 | 第18-19页 |
| ·UML 形式语义的研究 | 第19页 |
| ·本章小结 | 第19-20页 |
| 3 形式化方法和B 方法 | 第20-36页 |
| ·形式化方法 | 第20-22页 |
| ·形式化方法基本概述 | 第20-21页 |
| ·形式化方法的主要研究内容 | 第21-22页 |
| ·B 方法 | 第22-34页 |
| ·B 方法概述 | 第22-23页 |
| ·B 方法的符号表示法 | 第23-25页 |
| ·抽象机 | 第25-31页 |
| ·精化和实现 | 第31-32页 |
| ·B 方法的优越性 | 第32-34页 |
| ·UML 与B 方法的结合 | 第34页 |
| ·ProB 工具 | 第34-35页 |
| ·本章小结 | 第35-36页 |
| 4 UML 类图到B 方法形式化规约 | 第36-56页 |
| ·类图 | 第36-42页 |
| ·类 | 第36-38页 |
| ·类与类之间的关系 | 第38-41页 |
| ·接口 | 第41-42页 |
| ·类图到B 形式化规约 | 第42-55页 |
| ·类的B 形式化规约 | 第42-47页 |
| ·类与类之间关系的B 形式化规约 | 第47-50页 |
| ·OCL 数据类型到B 形式化规约 | 第50-51页 |
| ·带OCL 约束条件类的B 形式化规约 | 第51-52页 |
| ·类图的B 形式化规约 | 第52-54页 |
| ·类图层次结构的B 形式化规约 | 第54-55页 |
| ·本章小结 | 第55-56页 |
| 5 实例分析 | 第56-69页 |
| ·电梯系统描述 | 第56页 |
| ·电梯系统的UML 模型图 | 第56-58页 |
| ·类图 | 第56-57页 |
| ·状态图 | 第57-58页 |
| ·电梯系统的UML 类图的B 形式化规约 | 第58-64页 |
| ·电梯的B 形式化规约 | 第59-62页 |
| ·电梯门的B 形式化规约 | 第62页 |
| ·电梯按钮和楼层按钮的B 形式化的规约 | 第62-63页 |
| ·电梯系统的B 形式化规约 | 第63-64页 |
| ·电梯系统形式规约的模型检测 | 第64-68页 |
| ·本章小结 | 第68-69页 |
| 6 结论 | 第69-70页 |
| ·总结 | 第69页 |
| ·展望 | 第69-70页 |
| 致谢 | 第70-71页 |
| 参考文献 | 第71-74页 |
| 附录 | 第74页 |
