| 摘要 | 第1-4页 |
| Abstract | 第4-10页 |
| 第一章 绪论 | 第10-20页 |
| ·研究背景 | 第10-11页 |
| ·研究目的和主要内容 | 第11-14页 |
| ·具体问题及研究途径 | 第14-16页 |
| ·论文主要创新点 | 第16-18页 |
| ·项目背景 | 第18页 |
| ·论文结构 | 第18-20页 |
| 第二章 相关工作 | 第20-36页 |
| ·引言 | 第20页 |
| ·MDA与UML | 第20-23页 |
| ·模型驱动体系结构MDA简介 | 第20-22页 |
| ·统一建模语言UML简介 | 第22-23页 |
| ·DSM与XMML | 第23-27页 |
| ·特定领域建模 | 第23-25页 |
| ·XMML元建模语言 | 第25-27页 |
| ·基于非形式化的一致性验证 | 第27-31页 |
| ·Xlinkit | 第27-28页 |
| ·CAMLE | 第28-29页 |
| ·GME | 第29-30页 |
| ·MetaEdit+ | 第30-31页 |
| ·基于形式化的一致性验证 | 第31-35页 |
| ·BON | 第31-32页 |
| ·基于ADT的类图形式化和验证 | 第32-33页 |
| ·基于一阶逻辑的类图形式化和验证 | 第33页 |
| ·基于Z的类图形式化和验证 | 第33-34页 |
| ·基于Horn子句的特定领域建模语言形式化 | 第34-35页 |
| ·其他UML形式化工作 | 第35页 |
| ·本章小结 | 第35-36页 |
| 第三章 研究基础和相关概念 | 第36-47页 |
| ·引言 | 第36页 |
| ·一阶逻辑理论介绍 | 第36-44页 |
| ·谓词演算Q的语法 | 第38-40页 |
| ·谓词演算Q的语义 | 第40-42页 |
| ·谓词演算Q的元理论 | 第42页 |
| ·一阶形式系统 | 第42-43页 |
| ·自动定理证明技术 | 第43-44页 |
| ·类型化与一致性 | 第44-46页 |
| ·本章小结 | 第46-47页 |
| 第四章 域和元域 | 第47-59页 |
| ·引言 | 第47页 |
| ·域与特定领域建模语言 | 第47-54页 |
| ·域 | 第47-52页 |
| ·域映射与特定领域建模语言 | 第52-54页 |
| ·元域与元建模语言 | 第54-58页 |
| ·元域 | 第54-55页 |
| ·元域映射与特定领域元建模语言 | 第55-58页 |
| ·本章小结 | 第58-59页 |
| 第五章 XMML元建模语言的形式化 | 第59-101页 |
| ·引言 | 第59页 |
| ·XMML元建模语言的定义 | 第59-60页 |
| ·XMML元建模语言基于一阶逻辑的形式化 | 第60-100页 |
| ·XMML元建模语言抽象语法分析 | 第60-62页 |
| ·XMML元建模语言核心元类型 | 第62-63页 |
| ·XMML元建模语言形式化及其约束关系分析 | 第63-96页 |
| ·XMML元建模语言类型化约束 | 第96-99页 |
| ·XMML元建模语言形式系统TXMML | 第99-100页 |
| ·本章小结 | 第100-101页 |
| 第六章 基于XMML元建模语言的元模型一致性验证 | 第101-131页 |
| ·引言 | 第101页 |
| ·XMML元建模语言形式系统TXMML的一致性 | 第101-106页 |
| ·TXMML的可靠性 | 第102页 |
| ·TXMML的一致性 | 第102-106页 |
| ·基于TXMML的元模型一致性验证 | 第106-116页 |
| ·元模型对XMML元建模语言满足关系的判定 | 第106-113页 |
| ·基于元域的元模型一致性 | 第113-116页 |
| ·元模型到一阶逻辑公式集的映射 | 第116-122页 |
| ·元模型结构映射 | 第117-120页 |
| ·元模型语义映射 | 第120-122页 |
| ·实例研究：基于TXMML的元模型一致性验证 | 第122-130页 |
| ·软件体系结构简化元模型MSA的一致性验证 | 第123-128页 |
| ·一个简单计算机网络拓扑元模型Mnet的一致性验证 | 第128-130页 |
| ·本章小结 | 第130-131页 |
| 第七章 基于元模型的模型一致性验证 | 第131-183页 |
| ·引言 | 第131-132页 |
| ·XMML元建模语言形式化与元模型形式化的比较 | 第132-134页 |
| ·基于域的元模型形式化 | 第134-150页 |
| ·基于域的元模型形式化框架 | 第134-135页 |
| ·元模型约束关系分析 | 第135-137页 |
| ·符号映射 | 第137-140页 |
| ·公理映射 | 第140-150页 |
| ·元模型形式化的复杂性分析 | 第150页 |
| ·基于域的元模型一致性 | 第150-162页 |
| ·基于一阶逻辑的元模型形式系统 | 第150-152页 |
| ·元模型基于域的逻辑一致性 | 第152-156页 |
| ·领域一致性约束 | 第156-162页 |
| ·基于域的模型一致性验证 | 第162-168页 |
| ·描述语义 | 第162-163页 |
| ·基于域的模型一致性 | 第163-168页 |
| ·模型到一阶逻辑公式集的映射 | 第168-173页 |
| ·模型结构映射 | 第168-171页 |
| ·模型语义映射 | 第171-173页 |
| ·实例研究：元模型形式化及基于元模型的模型一致性验证 | 第173-182页 |
| ·元模型形式化及基于元模型的模型一致性验证过程步骤 | 第173-175页 |
| ·简单计算机网络拓扑元模型Mnet的形式化 | 第175-177页 |
| ·基于Mnet的计算机网络拓扑模型的一致性验证 | 第177-182页 |
| ·本章小结 | 第182-183页 |
| 第八章 元模型及模型形式化自动映射程序的设计和实现 | 第183-198页 |
| ·引言 | 第183页 |
| ·SPASS简介 | 第183-186页 |
| ·SPASS逻辑系统构成 | 第183-184页 |
| ·SPASS基本用法 | 第184-186页 |
| ·形式化自动映射程序LMMBSS | 第186-196页 |
| ·LMMBSS的设计 | 第186-190页 |
| ·LMMBSS的实现 | 第190页 |
| ·MapMBD核心代码分析 | 第190-196页 |
| ·用SPASS进行模型验证的局限性 | 第196-197页 |
| ·本章小结 | 第197-198页 |
| 第九章 总结与展望 | 第198-202页 |
| ·工作总结 | 第198-201页 |
| ·未来工作方向 | 第201-202页 |
| 附录A XMML具体语法模式 | 第202-209页 |
| 附录B 由MapMBD生成的SPASS格式WSA代码清单 | 第209-212页 |
| 参考文献 | 第212-219页 |
| 致谢 | 第219页 |
