| 摘要 | 第1-15页 |
| Abstract | 第15-19页 |
| 第一章 绪论 | 第19-27页 |
| §1．1 研究背景 | 第19-21页 |
| §1．2 研究现状及存在的问题 | 第21-23页 |
| 1．2．1 研究现状 | 第21-22页 |
| 1．2．2 存在的问题 | 第22-23页 |
| §1．3 课题的研究思路和内容 | 第23-24页 |
| §1．4 本文的主要贡献与创新 | 第24页 |
| §1．5 论文结构 | 第24-27页 |
| 第二章 并发反应式系统的组合验证 | 第27-41页 |
| §2．1 引言 | 第27-29页 |
| §2．2 基本概念 | 第29-31页 |
| §2．3 组合精化检验 | 第31-34页 |
| 2．3．1 分枝精化 | 第32-33页 |
| 2．3．2 线性精化 | 第33-34页 |
| 2．3．3 计算复杂性 | 第34页 |
| §2．4 组合模型检验 | 第34-38页 |
| 2．4．1 (?)CTL~*和(?)VCTL性质 | 第35-36页 |
| 2．4．2 LTL性质 | 第36-37页 |
| 2．4．3 计算复杂性 | 第37-38页 |
| §2．5 比较和讨论 | 第38-39页 |
| §2．6 结论与展望 | 第39-41页 |
| 第三章 接口自动机与I／O自动机的集成 | 第41-69页 |
| §3．1 引言 | 第41-43页 |
| 3．1．1 背景介绍 | 第41-42页 |
| 3．1．2 相关工作 | 第42-43页 |
| 3．1．3 本章的组织结构 | 第43页 |
| §3．2 接口自动机 | 第43-53页 |
| 3．2．1 简介 | 第43-46页 |
| 3．2．2 定义 | 第46-48页 |
| 3．2．3 并发组合与相容性 | 第48-50页 |
| 3．2．4 精化关系 | 第50-53页 |
| §3．3 异常自动机 | 第53-55页 |
| §3．4 并发组合与相容性上的联系 | 第55-60页 |
| §3．5 精化关系上的联系 | 第60-68页 |
| §3．6 本章小结 | 第68-69页 |
| 第四章 对接口自动机理论的完善 | 第69-93页 |
| §4．1 背景介绍 | 第69-70页 |
| §4．2 接口自动机理论中的一个错误及其修正 | 第70-72页 |
| 4．2．1 错误 | 第70-71页 |
| 4．2．2 修正 | 第71-72页 |
| §4．3 基本精化 | 第72-85页 |
| 4．3．1 闭接口自动机 | 第83-85页 |
| §4．4 广义精化 | 第85-92页 |
| §4．5 本章小结 | 第92-93页 |
| 第五章 WRIGHT的基于接口自动机的语义解释 | 第93-111页 |
| §5．1 引言 | 第93-94页 |
| §5．2 WRIGHT概况 | 第94-96页 |
| §5．3 WRIGHT的基于接口白动机的语义解释 | 第96-101页 |
| 5．3．1 连接子的语义 | 第97-98页 |
| 5．3．2 联接(Attachments)的语义 | 第98页 |
| 5．3．3 相关的测试规则 | 第98-100页 |
| 5．3．4 性质 | 第100-101页 |
| §5．4 与原语义解释的比较 | 第101-102页 |
| §5．5 一种Web Services组合的解决办法 | 第102-109页 |
| 5．5．1 BPEL4WS协议 | 第102-105页 |
| 5．5．2 案例分析：网上超市 | 第105-109页 |
| §5．6 本章小结 | 第109-111页 |
| 第六章 一种接口自动机的组合精化检验方法 | 第111-127页 |
| §6．1 引言 | 第111-113页 |
| §6．2 基本知识 | 第113-115页 |
| §6．3 一种新的组合精化检验方法 | 第115-119页 |
| §6．4 案例分析 | 第119-121页 |
| §6．5 相对不可达迁移的计算 | 第121-126页 |
| 6．5．1 从接口自动机到标记迁移系统 | 第121-123页 |
| 6．5．2 迁移状态化 | 第123-126页 |
| §6．6 本章小结 | 第126-127页 |
| 第七章 基于逆观察等价的组合可达性分析 | 第127-151页 |
| §7．1 引言 | 第127-129页 |
| §7．2 基本知识 | 第129-131页 |
| §7．3 接口自动机的相对不可达迁移的计算(续) | 第131-133页 |
| §7．4 逆观察等价 | 第133-139页 |
| §7．5 基于逆观察等价的组合可达性分析 | 第139-141页 |
| §7．6 案例分析 | 第141-150页 |
| 7．6．1 简单令牌传递系统 | 第141-146页 |
| 7．6．2 令牌环互斥系统 | 第146-150页 |
| §7．7 本章小结 | 第150-151页 |
| 第八章 结束语 | 第151-154页 |
| §8．1 工作总结 | 第151-152页 |
| §8．2 研究展望 | 第152-154页 |
| 论文发表情况 | 第154-155页 |
| 致谢 | 第155-156页 |
| 参考文献表 | 第156-167页 |