摘要 | 第1-13页 |
ABSTRACT | 第13-15页 |
第一章 绪论 | 第15-22页 |
·研究背景 | 第15-16页 |
·问题陈述 | 第16-17页 |
·研究途径 | 第17-18页 |
·贡献和创新点 | 第18-20页 |
·论文结构 | 第20-22页 |
第二章 相关工作 | 第22-31页 |
·手工方式的一致性检查 | 第22-23页 |
·语法方式的一致性检查 | 第23-26页 |
·NDRDL | 第23-24页 |
·Xlinkit | 第24页 |
·UML/Analyzer | 第24-25页 |
·CAMLE | 第25-26页 |
·语义方式的一致性检查 | 第26-30页 |
·用ADT 检查类图 | 第27页 |
·用一阶逻辑检查类图 | 第27-28页 |
·用进程代数检查行为模型 | 第28-29页 |
·BON 模型的一致性 | 第29-30页 |
·小结 | 第30-31页 |
第三章 模型一致性的概念 | 第31-34页 |
·建模语言和模型 | 第31-33页 |
·一致性和一致性约束 | 第33-34页 |
第四章 基于GEBNF 语法定义一致性约束 | 第34-50页 |
·GEBNF | 第34-38页 |
·从GEBNF 推导约束语言 | 第38页 |
·实例研究1:CAMLE 语言的抽象语法和一致性约束 | 第38-48页 |
·CAMLE 语言的抽象语法 | 第38-43页 |
·CAMLE 模型的一致性约束 | 第43-48页 |
·小结 | 第48-50页 |
第五章 基于元模型的一致性规约 | 第50-60页 |
·元建模 | 第50-52页 |
·由元模型导出符号表 | 第52-54页 |
·实例研究2:从UML 元模型推导约束语言 | 第54-58页 |
·简化的UML 元模型 | 第54-57页 |
·UML 的一致性约束 | 第57-58页 |
·小结 | 第58-60页 |
第六章 一致性约束的语义基础 | 第60-81页 |
·对元模型的形式化 | 第60-68页 |
·对建模语言形式化的框架 | 第60-62页 |
·公理映射 | 第62-68页 |
·对元模型的分析 | 第68-72页 |
·元模型的一致性 | 第68-72页 |
·一致性约束的正确性 | 第72页 |
·实例研究3: 元模型的一致性检验 | 第72-78页 |
·案例 | 第73-75页 |
·主要发现 | 第75-78页 |
·实例研究4:一致性约束的正确性验证 | 第78页 |
·小结 | 第78-81页 |
·元模型语义形式化的复杂性 | 第79页 |
·有待解决的问题 | 第79页 |
·相关工作 | 第79-81页 |
第七章 基于逻辑推理的一致性检查 | 第81-102页 |
·描述语义 | 第81-88页 |
·描述语义的概念 | 第81-84页 |
·语义映射 | 第84-86页 |
·语境映射 | 第86-88页 |
·基于描述语义的一致性检查 | 第88-89页 |
·实例研究5:对模型的形式化和一致性检查 | 第89-96页 |
·简化的元模型 | 第91页 |
·UML 2.0 元模型 | 第91页 |
·聊天室模型 | 第91-95页 |
·会议管理系统模型 | 第95-96页 |
·实例研究6:规则的有效性 | 第96-98页 |
·小结 | 第98-102页 |
·相关工作 | 第99-100页 |
·存在的问题 | 第100-102页 |
第八章 翻译和分析元模型/模型的工具实现 | 第102-107页 |
·逻辑系统 | 第102-103页 |
·LAMBDES 的结构和功能 | 第103-107页 |
·对元模型的形式化 | 第105页 |
·对模型的形式化 | 第105-107页 |
第九章 一致性检查工具的测试 | 第107-129页 |
·数据变异测试方法概述 | 第107-113页 |
·实例研究7:测试CAMLE 一致性检查工具 | 第113-124页 |
·变异算子 | 第113-115页 |
·种子数据和变异数据 | 第115-116页 |
·测试结果 | 第116-119页 |
·测试充分性 | 第119-122页 |
·测试开销 | 第122-124页 |
·小结 | 第124-129页 |
第十章 结束语 | 第129-131页 |
·工作总结 | 第129-130页 |
·未来工作方向 | 第130-131页 |
致谢 | 第131-133页 |
参考文献 | 第133-147页 |
攻读博士学位期间取得的学术成果 | 第147-150页 |
攻读博士学位期间参与的主要科研项目 | 第150页 |