| 摘要 | 第1-5页 |
| Abstract | 第5-9页 |
| 第1章 绪论 | 第9-15页 |
| ·课题研究背景和意义 | 第9-10页 |
| ·国内外研究现状 | 第10-12页 |
| ·检测工具的研究现状 | 第10-11页 |
| ·模型检测一致性研究现状 | 第11-12页 |
| ·存在的问题 | 第12页 |
| ·论文研究内容及组织结构 | 第12-15页 |
| ·研究内容 | 第12-13页 |
| ·组织结构 | 第13-15页 |
| 第2章 理论背景 | 第15-24页 |
| ·模型检测的相关理论 | 第15-18页 |
| ·模型检测的基本思想和步骤 | 第15-16页 |
| ·分支时序逻辑 CTL | 第16-17页 |
| ·解释系统模型理论 | 第17-18页 |
| ·模型检测工具 MCMAS | 第18-21页 |
| ·MCMAS 的功能模块 | 第19页 |
| ·MCMAS 的运行流程 | 第19-20页 |
| ·MCMAS 的输入语言 ISPL | 第20-21页 |
| ·多主体系统及其建模语言 AUML | 第21-23页 |
| ·本章小结 | 第23-24页 |
| 第3章 基于 AUML 和 MCMAS 的模型检测方法 | 第24-37页 |
| ·基于 AUML 和 MCMAS 的一致性模型检测框架的提出 | 第24-25页 |
| ·改进的多主体系统设计方法 FDMAS | 第25-31页 |
| ·FDMAS的设计流程 | 第25-27页 |
| ·FDMAS 中 AUML 的形式化描述语法语义 | 第27-31页 |
| ·FDMAS 中 AUML 形式化与 DIS 转换规则的实现 | 第31-36页 |
| ·转换的可行性 | 第31-32页 |
| ·主体类模型与 DIS 中相关元素的转换 | 第32-33页 |
| ·组织类模型与 ISPL 中组织关系的转换 | 第33-34页 |
| ·状态机模型与 DIS 中相关元素的转换 | 第34-36页 |
| ·本章小结 | 第36-37页 |
| 第4章 转换工具 AUML2DIS 的实现 | 第37-47页 |
| ·系统的需求分析 | 第37-38页 |
| ·AUML2DIS 的系统设计 | 第38-45页 |
| ·输入输出设计 | 第38-39页 |
| ·软件代码的设计 | 第39-45页 |
| ·AUML2DIS 的实现 | 第45-46页 |
| ·本章小结 | 第46-47页 |
| 第5章 实例分析 | 第47-61页 |
| ·实例验证的设计思路 | 第47-48页 |
| ·实验环境的搭建 | 第48-49页 |
| ·Cygwin 的安装 | 第48页 |
| ·Cygwin 环境下的 MCMAS 的安装和配置 | 第48-49页 |
| ·以 FDMAS 为指导的实例建模 | 第49-54页 |
| ·Book_store_System 的需求分析设计 | 第50-51页 |
| ·Book_store_System 的状态图 | 第51-53页 |
| ·Book_store_System 的状态机形式化描述 | 第53-54页 |
| ·Book_store_System 形式化规范的生成 | 第54-56页 |
| ·Book_store_System 的评估函数 | 第55页 |
| ·验证主体知识规范的形式化描述 | 第55-56页 |
| ·验证主体行为规范的形式化描述 | 第56页 |
| ·程序执行以及结果分析 | 第56-60页 |
| ·本章小结 | 第60-61页 |
| 结论 | 第61-63页 |
| 参考文献 | 第63-66页 |
| 攻读硕士学位期间承担的科研任务与主要成果 | 第66-67页 |
| 致谢 | 第67-68页 |
| 作者简介 | 第68页 |
