| 摘要 | 第1-5页 |
| Abstract | 第5-13页 |
| 第1章 引言 | 第13-34页 |
| ·网格技术的起源和发展 | 第13页 |
| ·网格服务与网格服务流 | 第13-15页 |
| ·网格服务流的正确性保障与形式化验证 | 第15-20页 |
| ·网格服务流正确性保障的重要性 | 第15-17页 |
| ·研究挑战及原因 | 第17-19页 |
| ·本文的网格服务流形式化验证范畴和待解决问题 | 第19-20页 |
| ·网格服务流形式化验证技术的研究现状 | 第20-31页 |
| ·网格服务流的建模 | 第20-21页 |
| ·形式化建模与验证技术及其必要性 | 第21-24页 |
| ·π演算的应用与优势 | 第24-27页 |
| ·Web 服务资源框架与状态/事件混合形式化方法 | 第27-29页 |
| ·本文方法的不同点 | 第29-31页 |
| ·本文研究的主要内容和贡献 | 第31-34页 |
| ·研究什么和不研究什么 | 第31页 |
| ·本文组织与主要贡献 | 第31-34页 |
| 第2章 状态π演算及其类型约束的提出与分析 | 第34-51页 |
| ·本章引论 | 第34-35页 |
| ·状态π演算中的状态模型与状态操作 | 第35-39页 |
| ·状态模型的静态语义 | 第35-36页 |
| ·状态π演算的语法和状态操作 | 第36-39页 |
| ·状态标号迁移系统、同余和扩展操作语义 | 第39-41页 |
| ·状态互模拟关系 | 第41-43页 |
| ·状态π演算的类型约束 | 第43-49页 |
| ·数据类型结构的静态语义 | 第44页 |
| ·带类型约束的状态π演算操作语义 | 第44-49页 |
| ·小结 | 第49-51页 |
| 第3章 基于状态π演算的网格服务流形式化语义 | 第51-79页 |
| ·本章引论 | 第51-52页 |
| ·服务执行与基本活动的状态π演算形式化 | 第52-59页 |
| ·服务执行的状态π演算语义 | 第53-55页 |
| ·服务执行的多实例化语义 | 第55-56页 |
| ·基本活动的状态π演算语义 | 第56-57页 |
| ·服务选择的状态π演算语义 | 第57-59页 |
| ·DAGMan 控制流结构的状态π演算形式化 | 第59-62页 |
| ·DAGMan 中的NoPostFail | 第59-60页 |
| ·顺序结构的状态π演算语义 | 第60页 |
| ·同步并发结构的状态π演算语义 | 第60-61页 |
| ·重试结构的状态π演算语义 | 第61-62页 |
| ·BPEL4WS 服务流的状态π演算形式化 | 第62-67页 |
| ·顺序结构的状态π演算语义 | 第62页 |
| ·流结构的状态π演算语义 | 第62-63页 |
| ·循环结构的状态π演算语义 | 第63页 |
| ·分支结构的状态π演算语义 | 第63页 |
| ·选择结构的状态π演算语义 | 第63-64页 |
| ·同步联接的状态π演算语义 | 第64-65页 |
| ·范围限定的状态π演算语义 | 第65-66页 |
| ·异常处理与补偿的状态π演算语义 | 第66-67页 |
| ·全局终止的状态π演算语义 | 第67页 |
| ·服务流的形式化示例 | 第67-69页 |
| ·网格服务流中的并发与管道模式 | 第69-76页 |
| ·静态并发执行模式及其状态π演算语义 | 第70-71页 |
| ·动态自适应并发执行模式及其状态π演算语义 | 第71-72页 |
| ·尽力执行的管道执行模式及其状态π演算语义 | 第72-73页 |
| ·阻塞执行的管道执行模式及其状态π演算语义 | 第73页 |
| ·缓冲执行的管道执行模式及其状态π演算语义 | 第73-74页 |
| ·多实例的管道执行模式及其状态π演算语义 | 第74-75页 |
| ·流方式的管道执行模式及其状态π演算语义 | 第75-76页 |
| ·基于状态π演算的形式化结果与优势讨论 | 第76-78页 |
| ·小结 | 第78-79页 |
| 第4章 网格服务流的状态π演算形式化验证 | 第79-110页 |
| ·本章引论 | 第79-80页 |
| ·从状态π演算到状态标号迁移系统 | 第80-84页 |
| ·网格服务流的结构与规范语义约束验证 | 第84-90页 |
| ·网格服务流的业务逻辑验证及应用实例 | 第90-100页 |
| ·业务逻辑验证的服务流实例 | 第90-91页 |
| ·静态业务逻辑验证 | 第91-96页 |
| ·动态业务逻辑验证 | 第96-100页 |
| ·状态π演算形式化验证方法的优点与特点 | 第100-101页 |
| ·业务逻辑的一致性验证 | 第101-109页 |
| ·冲突业务逻辑与冗余业务逻辑 | 第101-102页 |
| ·业务逻辑一致性验证方法与实现 | 第102-105页 |
| ·应用实例与讨论 | 第105-109页 |
| ·小结 | 第109-110页 |
| 第5章 网格服务流形式化验证方法的性能改进 | 第110-153页 |
| ·本章引论 | 第110-111页 |
| ·基于域分析的验证分解方法 | 第111-130页 |
| ·网格服务流的建模约定 | 第111-113页 |
| ·基于标准域分析的服务流分解 | 第113-116页 |
| ·基于标准域分析的验证分解 | 第116-120页 |
| ·基于松弛域分析的服务流分解 | 第120-122页 |
| ·基于域分析的验证分解实现与应用结果讨论 | 第122-130页 |
| ·基于错误过程模式的验证向导方法 | 第130-151页 |
| ·错误过程模式的提出 | 第131-132页 |
| ·基本错误过程模式 | 第132-136页 |
| ·高级分支与同步错误模式 | 第136-138页 |
| ·结构错误模式 | 第138-139页 |
| ·多实例错误模式 | 第139-141页 |
| ·基于状态的错误模式 | 第141-142页 |
| ·取消错误模式 | 第142-143页 |
| ·带向导的快速错误过程模式验证 | 第143-147页 |
| ·应用与结果讨论 | 第147-151页 |
| ·小结 | 第151-153页 |
| 第6章 网格服务流验证系统(GridPiAnalyzer)及其实现 | 第153-166页 |
| ·本章引论 | 第153-154页 |
| ·GridPiAnalyzer 的系统框架与模块 | 第154-156页 |
| ·状态π演算模型在GridPiAnalyzer中的实现 | 第156-158页 |
| ·状态标号迁移系统及验证结果的封装 | 第158-160页 |
| ·GridPiAnalyzer 中的BPSL 可视化业务逻辑描述 | 第160-161页 |
| ·GridPiAnalyzer 的已有应用及背景介绍 | 第161-165页 |
| ·LIGO 数据网格的引力波探测数据分析应用 | 第162-163页 |
| ·基于BPEL4WS 的银行开户法律法规验证 | 第163-165页 |
| ·小结 | 第165-166页 |
| 第7章 结束语 | 第166-169页 |
| 参考文献 | 第169-179页 |
| 致谢 | 第179-180页 |
| 附录A LIGO 引力波探测数据分析实例SF1～SF3 的完整验证性能及其比较 | 第180-187页 |
| 附录B SF1～SF3 待验证业务逻辑的对应LTL 公式表 | 第187-188页 |
| 附录C 基于标准域分析的验证策略分解定理证明 | 第188-190页 |
| 个人简历、在学期间发表的学术论文与研究成果 | 第190-191页 |
