（计算机应用技术专业论文）web服务事务协调协议wstx的形式化分析与验证.pdf

j n a n j i n gu n i v e r s i t yo f a e r o n a u t i c sa n da s t r o n a u t i c s 功eg r a d u a t es c h o o l c o l l e g eo fi n f o r m a t i o ns c i e n c ea n dt e c h n o l o g y f o r m a l a n a l y s i sa n d v e r i f i c a t i o no fa mj d1 j n11 r lr a n s a c t l o nu 0 0 r n l n a t l o nr r o t 0 c 0 ln a m e d w s t xf o rw e bs e r v i c e s a t h e s i si n c o m p u t e rs c i e n c ea n dt e c h n o l o g ye n g i n e e r i n g b y l ix i a n g a d v i s e d b y p r o f h u a n g z h i q i u s u b m i t t e di np a r t i a lf u l f i l l m e n t o ft h er e q u i r e m e n t s f o r t h ed e g r e eo f m a s t e ro f e n g i n e e r i n g d e c e m b e r , 2 0 0 9 承诺书 本人声明所呈交的硕士学位论文是本人在导师指导下进 行的研究工作及取得的研究成果。除了文中特别加以标注和致 谢的地方外，论文中不包含其他人已经发表或撰写过的研究成 果，也不包含为获得南京航空航天大学或其他教育机构的学位 或证书而使用过的材料。 本人授权南京航空航天大学可以将学位论文的全部或部 分内容编入有关数据库进行检索，可以采用影印、缩印或扫描 等复制手段保存、汇编学位论文。 ( 保密的学位论文在解密后适用本承诺书) 作者签名：左益 日期：b 兰；：! 歹 1 - 盘 南京航空航天大学硕士学位论文 摘要 w e b 服务作为一种新的计算模型正受到越来越多的关注，保证w e b 服务组合执行结果的一 致性和可靠性是w e b 服务面临的重要挑战之一。将事务机制应用到w e b 服务领域是寻求解决 w e b 服务组合执行结果一致性和可靠性问题的重要手段。针对w e b 服务自治、跨组织以及长周 期等特点，工业界基于传统事务机制提出了新的事务处理协议和标准。其中，w e b 服务事务协 调协议w s - t x 由于利用了现有的和正在制订的标准，能够融入w e b 服务架构，得到了业界的 广泛关注。 由于w s - t x 协议采用自然语言描述，缺乏严格的语义，很多学者使用形式化方法对其进 行研究，验证协议本身的正确性。然而，协议的正确并不代表使用协议的应用场景也能满足事 务特性。本文采用p i 一演算对w s - t x 协议应用场景进行建模，使用符号化模型检测工具n u s m v 2 从“安全性”和“活性”两方面对模型进行验证和分析。主要工作分为以下三个方面： l - 针对w s - t x 应用场景的并发特性，采用p i 演算对其进行建模。给出了w s - t x 协议应 用场景与p i 演算元素的映射关系，并在此基础上给出了建模规则。通过对应用了w s - t x 中 w s a t 协议的银行转帐场景和w s b a 协议的旅行安排场景的协调过程进行p i 一演算建模，验证 了建模规则的可行性。 2 由于现有p i 一演算模型检测工具存在检测能力不足的问题，本文将p i 演算模型转化为 s m v 程序( 有限状态自动机模型) ，利用n u s m v 2 进行检测。根据标号变迁系统到k r i p k e 结 构的映射关系找出p i 演算模型到s m v 程序的转换规则，并实现了自动转换工具p i c a l 2 n u s m v 3 分析了w s - t x 中两个事务协议w s a t 和w s - b a 应用场景的安全性和活性，用计算树 逻辑c t l 进行描述，并采用n u s m v 2 检验银行转帐和旅行安排的业务协调过程是否满足这些 性质，验证结果表明应用场景满足事务特性并且协议本身是可靠的。同时，进一步讨论和分析 了n u s m v 2 生成的反例。 关键词：w e b 服务，事务处理，形式化方法，p i 演算，协议建模，模型检测 w e b 服务事务协调协议w s - t x 的形式化分析与验证 a b s t r a c t a san e w c o m p u t i n gm o d e l ，w e bs e r v i c e sa r eb e c o m i n gm o r ea n dm o r ea t t r a c t i v e i ti so n eo ft h e m o s ti m p o r t a n tc h a l l e n g e so fw e bs e r v i c e st oe n s u r et h a tt h er e s u l to fr u n n i n gc o m p o s i t e dw e b s e r v i c e si sc o n s i s t e n ta n dr e l i a b l e t r a n s a c t i o nm e c h a n i s mi sc o n s i d e r e dt ob ea p p l i e di nw e bs e r v i c e s c o m p o s i t i o nt og e n e r a t ec o n s i s t e n ta n dr e l i a b l eo u t c o m e n o w a d a y s ，n e wt r a n s a c t i o np r o t o c o l sa n d s t a n d a r d sb a s e do nt r a d i t i o n a lt r a n s a c t i o nm e c h a n i s m sa r ep r o p o s e di nc o n s i d e r a t i o no fw e bs e r v i c e s c h a r a c t e r i s t i c ss u c ha sa u t o n o m y , h e t e r o g e n e o u s ，l o n gp e r i o da n ds oo n a m o n gt h ep r o t o c o l s ，a c o o r d i n a t i o np r o t o c o ln a m e dw s - t xi sac o m m o n l yc o n c e r n e dp r o t o c o lf o ri th a su s e dt h ee x i s t i n g a n dd e v e l o p i n gs t a n d a r d sa n dc a nb ea c t i o n e da sac o m p o n e n ti n t h ew e bs e r v i c e sa r c h i t e c t u r e a sw ek n o wt h a tw s t xi sd e s c r i b e db yn a t u r a ll a n g u a g ea n dl a c k so fs t r i c t s e m a n t i c s ，l o t so f r e s e a r c h e r sa p p l yf o r m a lm e t h o dt od or e s e a r c ho nw s - t x h o w e r v e r , t h ec o r r e c t n e s so fp r o t o c o l d o e s n ti m p l yt h a tt h es c e n a r i o sa p p l y i n gw s - t xm e e tt r a n s a c t i o nn e e d s t h u sp i - c a l c u l u si su s e dt o m o d e lt h es c e n a r i o sa p p l y i n gw s - t xa n das y m b o l i cm o d e lc h e c k i n gt o o ln a m e dn u s m v 2i s a d o p t e dt oc h e c kw h e t h e rt h es c e n a r i o sm e e ts a f e t ya n dl i v e n e s s t h em a r er e s e a r c hw o r k sc a nb e l i s t e da sf o l l o w s f i r s to fa l l ，c o n s i d e r i n gt h ec o n c u r r e n c yo fw s - t xs c e n a r i o s ，p i - e a l c u l u si sa d o p t e da n dt h e m a p p i n gr e l a t i o n o fe l e m e n t so fw s t xs c e n a r i o sa n dp i - e a l c u l u si sp r o p o s e d f u r t h e r m o r e ， m o d e l i n gr u l e so fp i - c a l c u l u sa r es t u d i e d i no r d e rt ov e r i f yt h ep r a c t i c a b i l i t yo fm a p p i n gr u l e s ，a s c e n a r i oa b o u ta c c o u n tt r a n s f e ra p p l y i n gw s - a tw h i c hi sac o n c r e t ec o o r d i n a t i o np r o t o c o li nw s - t x a n da n o t h e rs c e n a r i oa b o u tt r a v e la r r a n g e m e n ta p p l y i n gw s = b aw h i c hi sa n o t h e rc o o r d i n a t i o n p r o t o c o li nw s - t x a r ep r e s e n t e da n dm o d e l e db yp i - c a l c u l u s s e c o n d l y , f o re x i s t i n gm o d e lc h e c k i n gt o o l sf o rp i - e a l c u l u sc a l l tm e e to u rc o m m a n d ，p i - c a l c u l u s m o d e l sa r et r a n s l a t e di n t of i n i t es t a t em a c h i n ed e s c r i b e db ys m vl a n g u a g e ，w h i c hi st h ei n p u to f n u s m v 2 t h et r a n s l a t i n gr u l e sf r o mp i - c a l c u l u sm o d e l st os m vl a n g u a g ec o d ea r ep r o p o s e dd e r i v e d f r o mt h em a p p i n gf r o ml a b e l e dt r a n s i t i o ns y s t e mt ok r i p k es t r u c t u r e b a s e do nt h er u l e s ，a l la u t o m a t i c t r a n s l a t i n gt o o ln a m e dp i c a l 2 n u s m vi sd e s i g n e da n di m p l e m e n t e d f i n a l l y , s a f e t ya n dl i v e n e s sa r ed e f i n e dr e s p e c t i v e l yi nw s - a ts c e n a r i o sa n dw s - b as c e n a r i o s ， w h i c ha r et h e nr e p r e s e n t e di nc t l ( c o m p u t a t i o nt r e el o g i c ) n u s m v 2i su s e dt oc h e c k i n gw h e t h e r t h ec o o r d i n a t i o np r o c e s s e so fa c c o u n tt r a n s f e ra n dt r a v e la r r a n g e m e n tm e e tt h ep r o p e r t i e sd e s c r i b e di n c t l t h er e s u l to fm o d e lc h e c k i n gs h o w st h a tt h es c e n a r i o sa p p l y i n gw s - t xh a v et r a n s a c t i o n i i 南京航空航天大学硕士学位论文 p r o p e r t i e sa n dt h ew s - t xp r o t o c o li t s e l fi sr e l i a b l e am e t h o da b o u th o w t oa n a l y s ec o n u t e r e x a m p l e s g e n e r a t e db yn u s m v 2 i sp r e s e n t e dl a s t l y k e y w o r d s ：w e bs e r v i c e s ，t r a n s a c t i o np r o c e s s i n g ，f o r m a lm e t h o d ，p i - c a l c u l u s ，p r o t o c o lm o i l i n g ， m o d e lc h e c k i n g w e b 服务事务协调协议w s - t x 的形式化分析与验证 南京航空航天大学硕士学位论文 目录 第一章绪论1 1 1 课题研究背景及意义。1 1 2 w e b 服务事务的国内外研究现状一2 1 3 本文研究内容和组织结构3 第二章w e b 服务事务问题描述。5 2 1w e b 服务及其相关技术。5 2 2w 曲服务事务研究现状。7 2 2 1 事务的概念。7 2 2 2w e b 服务中的事务问题8 2 - 3w e b 服务事务协调协议w s - t x 9 2 3 1w e b 服务协调w s c o o r d i n a t i o n 1 0 2 3 2w e b 服务原子事务w s - a t o m i c t r a n s a c t i o n 一1 2 2 3 3w e b 服务业务活动w s b u s i n e s s a c t i v i t y 1 5 2 4 本章小结1 7 第三章基于p i 演算的w s - t x 协议应用建模1 8 3 1p i 演算建模分析1 8 3 2 面向w s - t x 协议应用场景的p i 演算建模方法1 9 3 2 1w s - t x 协议应用场景元素与p i 演算元素的映射关系。1 9 3 2 2w s - t x 协议应用场景的p i 演算建模规则2 0 3 3w s - t x 协议应用场景建模2 2 3 3 1w s - t x 协议应用场景2 2 3 3 2w s - t x 协议应用场景的p i 演算模型2 3 3 4 本章小结2 9 第四章p i 演算模型的s m v 程序表述3 0 4 1 基于n u s m v 2 的模型检测方法3 0 4 2p i 演算模型到s m v 程序代码的转换3 1 4 2 1 理论基础。3 2 4 2 2 转换规则3 8 4 3 转换工具p i c a l 2 n u s m v 的设计与实现4 0 w e b 服务事务协调协议w s - t x 的形式化分析与验证 4 3 1p i 演算文本解析器4 0 4 3 2 转换适配器4 2 4 3 3s m v 程序产生器4 3 4 4 本章小结4 4 第五章基于n u s m v 2 的w s - t x 协议应用模型检测及分析4 5 5 1w s - t x 协议应用性质分析4 5 5 1 1w s - a t 应用场景的性质分析4 6 5 1 2w s b a 应用场景的性质分析4 6 5 2 基于计算树逻辑c t l 的w s - t x 应用模型的性质归约4 7 5 2 1w s - a t 应用场景性质的c t l 描述4 7 5 2 2w s b a 应用场景性质的c t l 描述。4 8 5 3 基于n u s m v 2 的模型检测及其分析4 9 5 3 1w s - a t 应用场景性质检测及分析4 9 5 3 2w s b a 应用场景性质检测及分析4 9 5 3 3 进一步思考5 0 5 4 本章小结5 l 第六章总结与展望5 2 6 1 论文工作总结。5 2 6 2 进一步的工作5 3 参考文献5 4 j 目贮谢5 ； 在学期间的研究成果及发表的学术论文5 9 附录6 0 附录1 银行转帐s m v 程序代码6 0 附录2 旅行安排s m v 程序代码6 2 附录3 飞机订票w 曲服务的原子性模型检测反例6 6 南京航空航天大学硕士学位论文 图表清单 图1 1w s - t x 协议应用的p i 一演算形式化验证方法一3 图1 2 论文组织结构4 图2 1w e b 服务基本架构。5 图2 2 协调服务组成结构。1 0 图2 3 协调工作过程1 1 图2 4c o m p l e t i o n 协议状态转换图1 3 图2 5 两阶段提交协议状态转换图1 3 图2 6b u s i n e s s a g r e e m e n t w i t h p a r t i c i p a n t c o m p l e t i o n 状态转换图。1 5 图3 1p i 演算迁移语义。1 9 图3 2 银行转帐参与者交互图2 2 图3 3 旅行安排参与者交互图，2 3 图3 4p i 一演算流图2 3 图3 5 银行转帐p i 。演算流图2 3 图3 6 旅行安排p i 演算流图2 4 图4 1c t l 表达式算子含义3 l 图4 2p i 演算进程的状态变迁图。3 4 图4 3p i c a l 2 n u s m v 基本架构4 0 图4 4p i 演算的e b n f g l 图4 5p i 演算内存结构类图4 2 图4 6s m v 程序内存结构类图。4 3 图4 7 模块的s m v 代码本文生成程序4 3 图5 1w s - t x 协议应用场景形式化验证方法框架。4 5 图5 2 银行转帐模型f s m 状态数4 9 图5 3 银行转帐模型检测结果。4 9 图5 4 旅行安排模型f s m 状态数5 0 图5 5 旅行安排模型检测结果。5 0 图5 6 旅行安排场景原子性检测结果5l 表2 1c o m p l e t i o n 协议中消息的含义1 3 表2 2 两阶段提交协议中消息的含义1 4 表2 3b u s i n e s s a g r e e m e n t w i t h p a r t i c i p a n t c o m p l e t i o n 协议中消息的含义。1 6 表3 1w s - t x 应用场景元素到p i 演算元素的映射关系2 0 表3 2 银行转帐进程、通道含义和缩写形式对照表一2 4 表3 3 旅行安排进程、通道含义和缩写形式对照表2 4 表4 1c t l 算子定义。31 w e b 服务事务协调协议w s - t x 的形式化分析与验证 注释表 w e b 服务( w e bs e r v i c e s ) 部署在w e b 上的可以通过s o a p 协议进行交互的平台无关组件。 s o a p ( s i m p l e0 b j e c ta c c e s sp r o t o c 0 1 ) 简单对象访问协议，是一种基于x m l 的分布式计 算协议，支持分布式系统中的消息传递和远程过程调用。 w s d l ( w e bs e r v i c e sd e s c r i p t i o nl a n g u a g e ) w e b 服务描述语言，是一种基于x m l 的w e b 服务接口描述语言。 u d d i ( u n i v e r s a id e s c r i p t i o n ，d i s c o v e r ya n di n t e g r a t i o n ) 统一描述、发现和集成协议，是 种服务描述和发现的标准规范。 p i 演算( p i - c a l c u l u s ) 一种用来描述并发、移动系统的进程代数。 w s - t x o a s i s 的w e b 服务事务技术委员会制定的w e b 服务事务标准，包括 w s - c o o r d i n a t i o n 、w s - a t o m i c t r a n s a c t i o n 和w s b u s i n e s s a c t i v i t y 三部分。 w s - c ( w e bs e r v i c e sc o o r d i n a t i o n ) w e b 服务协调，是可扩展的事务协调框架。 w s - a t ( w e bs e r v i c e sa t o m i c t r a n s a c t i o n ) w e b 服务原子事务，在w s - c 的基础上定义了一 个原子事务协调类型用于协调具有“a l l - o r - n o n e ”属性的活动。 w s - b a ( w e bs e r v i c e sb u s i n e s s a c t i v i t y ) w e b 服务业务活动，在w s - c 的基础上定义了两种 业务活动协调类型用于协调活动，这些活动使用业务逻辑来处理业务流程活动执行过程中发生 的异常。 n u s m v 2 一种开源的模型检测工具，用于验证有限状态系统是否满足时序逻辑描述的需 求，属于符号模型检测系统。 s m v 语言模型检测工具n u s m v 2 的系统描述语言。 l t l ( l i n e a rt e m p o r a ll o g i c ) 线性时序逻辑。 c t l ( c o m p u t a t i o nt r e el o g i c ) 计算树逻辑，属于分支时序逻辑。 南京航空航天大学硕士学位论文 第一章绪论 1 1 课题研究背景及意义 在现代社会中，信息广泛渗透到人类社会和经济生活中，人类经济社会的发展不仅仅依赖 物质、能量等资源，同时也越来越多地依赖于信息资源，关于如何使用、管理和保护这些信息 的计算机技术对人类和现代社会变得至关重要。这些信息数据集中描述或刻画了现实世界中的 某些现象或活动的状态和演化，为了正确地反映现实世界，许多信息数据要求一起被访问和修 改，因此必须保证相关数据的一致性，事务处理技术为这些关键信息资源的有效管理和使用提 供了必要的机制和措施【l 】。事务是指对物理和抽象的应用状态上数据访问和更新的操作集合， 要么全部成功，要么全部失败，并保证并发执行的事务彼此互不干扰【2 】，这种“a l l - o r - n o n e ” 的语义是传统数据库访问的基础。 随着i n t e m e t 的普及和基于i n t e m e t 应用的延伸，以w e b 服务为基础的面向服务计算体系架 构( s e r v i c e - o r i e n t e d a r c h i t e c t u r e ，s o a ) 应运而生。w e b 服务作为一种崭新的分布式计算模型， 成为w e b 上数据和信息集成的有效机制【3 】。为了完成客户的请求，多个w e b 服务需要通过编排 或编s d 4 的方式组合在一起完成新的功能。由于w e b 服务的最终目标是允许网络上不同类型的 服务能够协同合作 5 1 ，这就要求w e b 服务组合执行具有一致性和可靠性，并能及时解决运行时 发生的各种异常。这类问题可以借助事务机制来解决【6 】。虽然传统的事务技术在数据库系统和 分布式应用中得到了广泛的研究和应用，但由于w e b 服务自身的松散耦合性、运行时间长、开 放式环境，使其在网络的时延性、系统的可靠性和一致性方面面临新的挑战，使得传统的事务 模型无法直接用到w e b 服务中r 丌。因此，由w e b 服务组合而成的业务流程如何保证应用一致性， 即在失败、异常等情况下，组合服务的执行能结束于一致状态，是w e b 服务组合应用的一个关键 问题，也是当前研究的热尉1 1 。 b p e l ( b u s i n e s sp r o c e s se x e c u t i o nl a n g u a g e ，业务过程执行语言) 喁】作为w e b 服务事实上的 标准，并没有描述分布于多个供应商和平台的参与者之间的协调一致性【9 】，而是建议在这种分 布式业务环境中使用w s - t x 协议【l o 】来实现对业务的参与者提供注册或撤销等分布式协调的通 知。这表明用w s - t x 协议来解决分布式业务的事务问题是未来的发展方向。w s - t x 协议是 o a s i s ( o r g a n i z a t i o a nf o r t h ea d v a n c e m e n t o fs 仃u c t u r e di n f o r m a t i o ns t a n d a r d ，结构化信息标准促 进组织1 标准，描述了一个为协调分布式应用程序行为提供协议支持的可扩展框架，这种协调协 议可被用于支持多个业务流程实例的运行，它们在分布式事务的输出上有一致性的要求。 w s - t x 协议为分布式业务事务处理提供了解决方法。然而，如何保证w s - t x 协议应用的 正确性是将w s - t x 协议应用于分布式业务中必须解决的问题，本文将对这一问题展开研究。 w e b 服务事务协调协议w s - t x 的形式化分析与验证 1 2w e b 服务事务的国内外研究现状 如何保证w e b 服务业务流程的事务特性是w e b 服务研究中的热点问题，得到了学术界和工 业界的关注。学术界的研究者主要从以下两个方面对w e b 服务事务问题进行研究： ( 1 ) 学术界的研究者吸取了其它一些松耦合环境下事务模型的做法，适当调整并放松了 传统事务a c i d ( a t o m i c i t y ，c o n s i s t e n c y ，i s o l a t i o n ，d u r a b i l i t y ) 特性的要求，先后提出了各种 扩展事务模型，实现松散、长运行系统中的事务管理。面向长事务的s a g a s 1 1 】项目第一次提出 了补偿事务的概念，系统在失效时将按照逆序执行所有已安装的补偿处理块回退到初始状态。 柔性事务模型【1 2 】是一种对操作的原子性和隔离性要求较低的松耦合扩展事务模型，子事务之间 通过偏序和优先两种依赖关系组合在一起。z h a n g 等用可重试和可补偿两个属性来刻画服务的 事务能力，进一步研究了柔性事务的一致性问题【1 3 】。上海交通大学的唐飞龙博士等提出了一个 能够同时协调短事务和长事务的模型，给出了协调算法及恢复机s 0 t 1 4 1 。国防科学技术大学的任 怡博士等提出了事务执行阶段的依赖异常处理机制，保证整个事务不失败【1 5 】。中科院软件研究 所的黄涛教授等从保障服务协作可靠性角度，给出了一个基于应用语义的松弛事务模型【1 6 1 。 ( 2 ) 用软件形式化方法对w e b 服务合成和事务进行研究已经成了国际上学术研究的热点。 在现有对w e b 服务事务形式化建模研究中，基于自然描述并发系统的进程代数方法的研究较 多。b o c c h i 等提出了面t - c a l c u l u s 【17 1 ，对p i 演算作了扩展，加入事务模块控制算予以支持长事务。 b u t l e r 等在传统的进程代数上加入补偿算子，提出支持描述事务处理的语言s t a c t l 8 】，是最先将 补偿和进程控制紧密结合的进程演算之一。 许多年以来，为了解决传统的事务处理的语义和协议不合时宜的问题，工业界由重要1 1 r 厂 商组成的标准化组织o a s i s 、o m g 和w 3 c 等技术委员会，一直致力于制定分布式业务事务处 理协议的业界标准，主要包括w s - c a f ( w e bs e r v i c e sc o m p o s i t i o na p p l i c a t i o nf r a m e w o r k ) 1 9 1 、 b t p ( b u s i n e s st r a n s a c t i o np r o t o c 0 1 ) 2 0 j b w s - t x 1 9 1 。w s - t x 用于w r e b 服务，利用了现有的和正 在制订的标准，比如w s d l ( w e bs e r v i c e sd e s c r i p t i o nl a n g u a g e ) 口、w s - a d d r e s s i n 9 1 2 2 、 w s s e c t t r i t y 2 3 1 和w s p o l i c y 2 4 增。这使w s - t x 集中在w 曲服务环境，并且简化了规范，还 可以把它们作为一个组件放在w e b 服务架构中，w e b 服务架构在性能优化方面的任何进步都 可以自动为它利用。因此，w s - t x 成为业界广泛关注的标准。目前已有对w s - t x 的实现，其 中包括a p a h e 的k a n l u l a 2 5 开源项目、s u n 的w s i t ( w e bs e r v i c e si n t e r o p e r a b i l i t yt e c h n o l o g i e s ) 开源项目1 2 6 j 和微软的w c f ( w i n d o w sc o m m u n i c a t i o nf o u n d a t i o n ) 项目( 已包含于n e tf r a m e w o r k 3 0 产品) ，它们都已经实现了w s c o o r d i n a t i o n 和w s - b u s i n e s s a c t i v i t y 协议，并且宣称在不久 将加入w s b u s i n e s s a c t i v i t y 协议的实现。 工业界提出的w e b 服务事务标准有大的软件厂商的支持，很容易得到推广和应用。然而工 业界已有的关于事务的协议标准，大多采用自然语言表达，没有做过形式化的表示和分析，规 2 一 南京航空航天大学硕士学位论文 范中存在定义不清晰的细节，缺乏精确的语义。针对这个问题，已经有研究用软件形式化方法 对工业界的事务协调协议进行了相关研究。b e r g e r 等用异步p i 一演算对分布式事务处理中经典的 两阶段提交协议进行了形式化验证暖n 。上海交通大学的戚正伟博士等提出了一种细胞膜演算的 形式化方法【2 引，利用对象和细胞膜的反应过程，简明地描述了w e b 服务事务处理过程，并分析 检验了早期的w s - a t o m i c t r a n s a c t i o n 和w s b u s i n e s s a c t i v i t y 协议。这些说明用形式化方法描述 和分析事务协调过程是可行且有意义的。然而，已有研究大部集中在验证事务协议( 如 w s - a t o m i c t r a n s a c t i o n 和w s b u s i n e s s a c t i v i t y ) 本身的正确性，并没有验证将事务协议应用到 实际场景中是否也能满足需求的事务特性。 为了支持分布式业务事务，传统方法一般如同h a g e n 等通过跨组织工作流协同，组建可靠 的工作流管理系统来保证跨组织业务应用的一致性 9 1 。w s c o o r d i n a t i o n 就是这样一种保证业务 应用一致性的协议框架，而w s a t o m i c t r a n s a c t i o n 和w s - b u s i n e s s a c t i v i t y 则用来保证协调过程 具有事务特性。c u r b e r a 等将各b p e l 业务作用域之间的补偿对应关系表示成w s - t x 的协调上 下文，提出协调组合w e b 服务的框架【2 9 1 。y a n g 等以b p e l 和w s - t x 为基础，扩充 w s b u s i n e s s a e t i v i t y 协议，将业务补偿逻辑作为协调逻辑的一部分，实现业务的柔性多补偿机 帛u t 3 0 l 。s c h a f e r 等基于向前恢复策略，进一步扩充w s - t x 的协调框架，支持业务补偿逻辑和协 调逻辑相分离的灵活的补偿操作【3 1 1 。这些研究都没有提供对协调场景协调正确性的验证方法。 针对上述不足，本文将对使用w s - t x 协议的应用场景是否满足系统需求的事务特性进行 研究，提供w s - t x 协议应用场景是否满足事务特性的验证方法，以保证使用w s - t x 协议的应 用能够达到系统设计的需求。对w s - t x 协议应用场景进行形式化分析与验证既可以验证应用 场景是否满足事务特性从而指导场景的设计与实现，又可以验证协议本身的可靠性。 1 3 本文研究内容和组织结构 图1 - 1w s - t x 协议应用的p i 一演算形式化验证方法 w s - t x 协议为分布式业务事务处理提供了解决方法，得到了产业界和学术界的普遍关注。 在对w s - t x 协议的研究和应用中，对w s - t x 具体应用是否满足事务特性的研究较少，本文将 对此进行研究。图1 1 给出了本文研究的方法：w s - t x 协议应用的p i 演算形式化验证方法。 3 w e b 服务事务协调协议w s - t x 的形式化分析与验证 首先对w s - t x 应用场景进行p i 演算建模，再将p i 演算进程表达式转化为s m v ( 模型检测工 具n u s m v 2 的系统描述语言) 程序代码，得到使用s m v 语言描述的w s t x 应用场景模型。 然后使用c t l ( c o m p u t a t i o nt r e el o 舀c ，计算树逻辑) 对w s t x 应用场景应满足的性质进行描述， 并用n u s m v 2 检测系统是否满足性质。如果不满足，则可反馈到w s - t x 应用的设计并进行修 改，甚至可以查找出w s - t x 协议的模糊不清或待完善之处。 本文的主要研究内容分为六章，各章节内容概述如下： 第一章绪论。阐述了本文课题研究的背景及意义。分析了w e b 服务事务的国内外研究现 状，并给出了本文的主要研究方法和内容。 第二章w e b 服务事务问题描述。概述了w e b 服务及相关技术，阐述了什么是w e b 服务事 务问题，以及w e b 服务事务问题的解决方法。然后对目前广为关注的w s - t x 协议进行了分析。 第三章基于p i 演算的w s - t x 协议应用