| 摘要 | 第1-5页 |
| Abstract | 第5-8页 |
| 第1章 绪论 | 第8-16页 |
| ·研究背景 | 第8-10页 |
| ·相关工作 | 第10-12页 |
| ·模型检查 | 第12-13页 |
| ·主要研究的内容 | 第13-15页 |
| ·本文结构 | 第15-16页 |
| 第2章 基于时态逻辑的 XML Schema 特征提取 | 第16-30页 |
| ·XML Schema 特征 | 第16-17页 |
| ·XML Schema 图 | 第17-19页 |
| ·Schema 图转换为 MCSG 模型 | 第19-22页 |
| ·MCSG 图的定义 | 第19-20页 |
| ·从 Schema 图到 MCSG 图的转换算法 | 第20-22页 |
| ·Schema 特征的时态逻辑公式表示 | 第22-28页 |
| ·RPC 特征的表示 | 第22-24页 |
| ·RAD 特征的表示 | 第24-25页 |
| ·PRPC 和 PRAD 特征的表示 | 第25-26页 |
| ·路径相关特征的表示 | 第26-28页 |
| ·本章小结 | 第28-30页 |
| 第3章 优化规则描述语言 ORS | 第30-42页 |
| ·Twig 模式定义 | 第30页 |
| ·ORS 语言 | 第30-35页 |
| ·ORS 语法 | 第30-32页 |
| ·ORS 优化规则表示实例 | 第32-34页 |
| ·ORS 优化规则简要说明 | 第34-35页 |
| ·ORS 语义 | 第35-40页 |
| ·sche_condition (Schema 条件)语义 | 第35-36页 |
| ·tree_condition 的语义 | 第36-37页 |
| ·action 的语义 | 第37-39页 |
| ·ors 规则语义 | 第39-40页 |
| ·本章小结 | 第40-42页 |
| 第4章 实现相关的重要算法 | 第42-58页 |
| ·基于 MCSG 的模型检查算法 | 第42-47页 |
| ·变量映射算法 | 第47-57页 |
| ·本章小结 | 第57-58页 |
| 第5章 ORS 支撑工具的实现 | 第58-64页 |
| ·系统实现架构 | 第58页 |
| ·相关工具简介 | 第58-60页 |
| ·主要模块和类设计 | 第60-61页 |
| ·优化动作输出的例子 | 第61-64页 |
| 结论 | 第64-66页 |
| 参考文献 | 第66-70页 |
| 攻读硕士学位期间所发表的学术论文 | 第70-72页 |
| 致谢 | 第72页 |