软件服务业务流程设计的若干问题研究
| 摘要 | 第1-6页 |
| Abstract | 第6-9页 |
| 目录 | 第9-17页 |
| 第一章 引言 | 第17-29页 |
| ·软件服务与面向服务架构 | 第17-18页 |
| ·软件服务业务流程的设计 | 第18-20页 |
| ·研究问题 | 第20-25页 |
| ·软件服务选择和复用 | 第20-22页 |
| ·流程约束设计和实现 | 第22-24页 |
| ·长事务及补偿设计 | 第24-25页 |
| ·本文工作和主要贡献 | 第25-28页 |
| ·文章框架 | 第28-29页 |
| 第二章 背景和预备知识 | 第29-50页 |
| ·软件服务业务流程 | 第29-35页 |
| ·面向服务的架构与Web服务 | 第30-32页 |
| ·Web服务业务流程执行语言(WS-BPEL) | 第32-34页 |
| ·REST服务 | 第34-35页 |
| ·业务流程中的事务 | 第35-40页 |
| ·面向服务架构协议体系中的事务 | 第35-39页 |
| ·业务流程管理中事务相关的问题 | 第39-40页 |
| ·数据为中心的业务流程 | 第40-45页 |
| ·业务流程中的数据模型和操作 | 第41-43页 |
| ·Artifact为中心的业务流程建模 | 第43-45页 |
| ·Petri网和Z记法 | 第45-50页 |
| ·Petri网 | 第45-48页 |
| ·Z记法 | 第48-50页 |
| 第三章 场景驱动的服务行为调控 | 第50-80页 |
| ·行为调控问题概述及动机示例 | 第50-53页 |
| ·研究动机示例 | 第50-52页 |
| ·研究问题：服务行为调控 | 第52-53页 |
| ·基于Petri网的建模 | 第53-59页 |
| ·用基于Petri网的模型为BPEL流程建模 | 第53-57页 |
| ·BPN模型的化简 | 第57-59页 |
| ·服务需求模型：UML顺序图 | 第59页 |
| ·行为分析 | 第59-66页 |
| ·BPN模型的行为：运行和路径 | 第60-62页 |
| ·针对场景的行为分析 | 第62-66页 |
| ·调控服务的构造 | 第66-76页 |
| ·事件自动机 | 第66-69页 |
| ·构造行为约束自动机 | 第69-72页 |
| ·证明定理3.2 | 第72-75页 |
| ·运行时的行为调控 | 第75-76页 |
| ·原型工具 | 第76-77页 |
| ·相关工作比较 | 第77-79页 |
| ·本章小结 | 第79-80页 |
| 第四章 针对数据一致性的业务流程强化 | 第80-165页 |
| ·业务流程强化概述 | 第80-82页 |
| ·卫式注入的动机示例和挑战概述 | 第82-87页 |
| ·业务流程示例：GSMa | 第82页 |
| ·GSM业务流程建模 | 第82-85页 |
| ·完整性约束 | 第85-86页 |
| ·在GSM中保障完整性约束的方法：卫式注入 | 第86-87页 |
| ·数据为中心的业务流程设计语言：GSM | 第87-97页 |
| ·GSM语言的基本元素 | 第87-91页 |
| ·外部任务规约 | 第91-94页 |
| ·基于GSM的业务流程执行 | 第94-96页 |
| ·式注入中的GSM | 第96-97页 |
| ·基于转换系统的GSM形式化语义 | 第97-113页 |
| ·形式化基础 | 第97-100页 |
| ·状态空间和初始状态 | 第100-103页 |
| ·变迁及其规约：操作(Operation) | 第103-110页 |
| ·转换系统 | 第110-113页 |
| ·与现有语义的比较 | 第113页 |
| ·卫式注入机制 | 第113-141页 |
| ·统一stage更新artifact的记法 | 第114-116页 |
| ·完整性约束 | 第116-120页 |
| ·计算注入条件 | 第120-134页 |
| ·对GSMart中的各个stage的卫式注入 | 第134-141页 |
| ·卫式注入的正确性和保守完备性 | 第141-146页 |
| ·基于BPEL流程的运行时数据一致性调控 | 第146-148页 |
| ·支持数据库访问的BPEL业务流程 | 第148-152页 |
| ·流程实例：BPMart | 第148-149页 |
| ·BPEL的数据操作 | 第149-150页 |
| ·基于Petri网的语义 | 第150-152页 |
| ·数据一致性调控机制 | 第152-160页 |
| ·消息依赖的数据一致性问题 | 第152-153页 |
| ·更新有关的记法 | 第153-154页 |
| ·基于符号执行的流程数据调控 | 第154-158页 |
| ·正确性和保守完备性 | 第158-160页 |
| ·流程数据调控的扩展讨论 | 第160-163页 |
| ·相关工作比较 | 第163-164页 |
| ·本章小结 | 第164-165页 |
| 第五章 长事务补偿及正确性保障 | 第165-238页 |
| ·长事务设计及补偿正确性概述 | 第166-168页 |
| ·带事务的流程示例 | 第168-170页 |
| ·抽象的带有事务的流程设计语言：BaT | 第170-174页 |
| ·语法 | 第170-172页 |
| ·BaT的代数语法示例 | 第172-174页 |
| ·单个服务的事务流程的执行 | 第174-187页 |
| ·流程执行 | 第174-175页 |
| ·BaT的转换系统语义 | 第175-185页 |
| ·转换系统的运行 | 第185-187页 |
| ·长事务的正确性准则 | 第187-188页 |
| ·设计指导 | 第188-199页 |
| ·指导条件 | 第188-191页 |
| ·使用默认错误-补偿处理的设计指导 | 第191-192页 |
| ·使用用户自定义的错误-补偿处理的设计指导 | 第192-196页 |
| ·示例 | 第196-199页 |
| ·事务流程行为特性以及设计指导的证明 | 第199-206页 |
| ·行为和性质 | 第199-203页 |
| ·设计指导的证明 | 第203-206页 |
| ·跨服务的事务 | 第206-211页 |
| ·服务编排 | 第206-208页 |
| ·IST的示例 | 第208-210页 |
| ·跨服务的事务和服务间的协同 | 第210-211页 |
| ·支持跨服务事务的BaT的语义 | 第211-224页 |
| ·语义扩展 | 第211-213页 |
| ·完整的语义 | 第213-224页 |
| ·跨服务事务的设计准则和设计指导 | 第224-234页 |
| ·IST的事务准则 | 第224-226页 |
| ·针对IST的设计指导 | 第226-230页 |
| ·IST设计指导的示例 | 第230-234页 |
| ·长事务设计准则的验证 | 第234-235页 |
| ·相关工作比较 | 第235-236页 |
| ·本章小结 | 第236-238页 |
| 第六章 总结和进一步工作 | 第238-240页 |
| 参考文献 | 第240-252页 |
| 简历与相关情况 | 第252-254页 |
| 致谢 | 第254-256页 |
