（计算机软件与理论专业论文）web服务编排语言的分析与测试.pdf

， p 尊 ， d i ss e r t a t i o nf o r m a s t e rd e g r e e ，2 011 删删1 i s c h o o lc o d e ：10 2 6 9 s t u d e n tn u m b e r ：51 0 81 5 0 0 0 1 0 e a s tc 皿n an r m a lu n r s v a n a l y s i sa n dt e s t i n go fw e b s e r v i c e sc h o r e o g r a p h y d e sc r i p t i o nl a n g u a g e d e p a r t m e n t ： s o f t w a r ee n g i n e e r i n gi n s t i t u t e m a j o r ： s u b j e c t ： t u t o r ： a u t h o r ： 2 0 11 0 4 墨一 竺坐些。竺量l 尘!|l坚藿l耋一胁一粪一叉 口hjjh 华东师范大学学位论文原创性声明 郑重声明：本人户厄呈交的学位论文( ( w e b , l i e 务编排语言的分析与测试是在 华东师范大学攻读额壬博士( 请勾选) 期间，在导师的指导下进行的研究工作及 取得的研究成果。除文中已经引用的内容外，本论文不包含其他个人已经发表或 撰写的研究成果。对本文的研究做出重要贡献的个人和集体，均已在本文中作了 明确的说明并表示谢意。 作者签名：灸途 b t n ：讪i ii f - j 月矽日 华东师范大学学位论文著作权使用声明 w e b 服务编排语言的分析与测试系本人在华东师范大学攻读学位期间在 导师指导下完成的硬生博士( 请勾选) 学位论文，本论文的研究成果归华东师范 大学所有。本人同意华东师范大学根据相关规定保留和使用此学位论文，并向主 管部门和相关机构如国家图书馆、中信所和”知网”送交学位论文的印刷版和电子 版；允许学位论文进入华东师范大学图书馆及数据库被查阅、借阅；同意学校将 学位论文加入全国博士、硕士学位论文共建单位数据库进行检索，将学位论文的 标题和摘要汇编出版，采用影印、缩印或者其它方式合理复制学位论文。 本学位论文属于( 请勾选) ( ) 1 经华东师范大学相关部门审查核定的“内部”或“涉密”学位论文宰， 于年月日解密，解密后适用上述授权。 2 不保密，适用上述授权。 新签名：垃厶一本人签名：扯 舢l 年s 月3 o 日 涉密”学位论文应是已经华东师范大学学位评定委员会办公室或保密委员会审定过的学位论文( 需附 获批的华东师范大学研究生申请学位论文”涉密”审批表方为有效) ，未经上述t t 器f l 审定的学位论文均为 公开学位论文。此声明栏不填写的，默认为公开学位论文，均适用上述授权) 。 肖浩硕士学位论文答辩委员会成员名单 姓名职称单位备注 刘静教授华东师范大学软件学院主席 陈铭松副教授华东师范大学软件学院 彭超副教授华东师范大学软件学院 张敏讲师华东师范大学软件学院秘书 厂一 l 摘要 w e b 服务编排描述语言( w e bs e r v i c e sc h o r e o g r a p h yd e s c r i p t i o nl a n g u a g e ，简 称w s c d l ) 从全局的视点描述服务组合各个参与方的行为规范，并且具有可重 用性以可及描述事务性等特点。在部署前对w s c d l 程序验证和测试可以有效 降低部署风险和项目成本。但是w s c d l 只是描述语言其程序不可执行，目前 由于w s c d l 程序没有解析器或模拟器，w s c d l 程序的验证与测试变得十分困 难。 本论文提出了通用的x m l 语言静态约束的验证方法。该方法与经典的模型检 查的方法类似，可以统一地验证不同语言的静态性质也可以统一地验证相同语言 的不同版本。该方法中用于描述静态制约的语言被称为约束逻辑，它基于一阶谓 词逻辑。论文同时提出了用于描述x m l 文档的形式化模型。另外，我们还设计了 使用模型化简技术优化后的验证算法用来验证x m l 文档是否满足其静态制约。 在我们小组自己开发的w s c d l 程序模拟器上，我们提出了一种自动测 试w s c d l 程序的方法。该方法通过使用从动态符号执行生成能达到分支覆盖标 准的测试用例从而自动完成对w s c d l 程序的测试。该方法支持w 曲服务组合的 异常处理，正常结束处理等特性，而其他研究往往没有处理这些特性。另外我们 提出了两种处理w s c d l 程序中断言的方法，这些断言可以描述w s c d l 程序预 期的行为。 我们在模块化的开源e c l i p s e 插件c d l c h e c k e rl - _ 实现了这些方法。c d l c h e c k e r 是w s c d l 的一个集成开发环境，它支持对w s c d l 程序的编辑、模拟、验证和 自动测试功能。最后，我们在c d l c h e c k e r 上设计了几组实验用来验证提出的方法 的有效性。实验结果显示本文的方法能够正确地处理w s c d l 程序。 关键词：w e b 服务组合，w s c d l ，关系演算，程序验证，符号执行，测试自 动化。 _ a b s t r a c t w e bs e r v i c e sc h o r e o g r a p h y d e s c r i p t i o nl a n g u a g e ( a b b r e v i a t e da sw s c d l ) w h i c h i sr e u s a b l ea n dc a p a b l eo fd e s c r i b i n gt r a n s a c t i o n a lr e q u i r e m e n t sr e g u l a t e st h ep a r t i c i p a n t s e x t e r n a lb e h a v i o r sf r o mt h eg l o b a lv i e w p o i n t v e r i f i c a t i o na n dt e s t i n go fw s c d l p r o g r a m sb e f o r ed e p l o y m e n tc a l ld r a s t i c a l l yr e d u c et h ed e p l o y m e n tr i s ka n dp r o j e c tc o s t s i n c ew s c d li sa d e s c r i p t i o nl a n g u a g ew h o s ep r o g r a mi sn o te x e c u t a b l e ，a n dt h e r ei s n ol a n g u a g ec o m p i l e ro rs i m u l a t o ra v a i l a b l e ，i ti sv e r yh a r dt ot e s ta n dv e r i f yw s c d l p r o g r a m s i nt h i st h e s i s ，w ep r o p o s eau n i f i e da p p r o a c ht ov a l i d a t et h es t a t i cc o n s t r a i n t so fx m - l l a n g u a g e s t h i sa p p r o a c hw h i c hr e s e m b l e st h em o d e lc h e c k i n gm e t h o di sl a n g u a g e a g o n i s t i ca n dv e r s i o ns c a l a b l e t h el o g i cu s e df o rd e s c r i b i n gs t a t i cc o n s t r a i n t si sc a l l e d c o n s t r a i n tl o g i cw h i c hi s b a s e do nt h ef i r s to r d e rl o g i c w ea l s op r o p o s eaf o r m a l m o d e lf o rc a p t u r i n gx m ld o c u m e n t s f u r t h e r m o r e ，a l la l g o r i t h mo p t i m i z e dw i t hm o d e l p r u n i n gt e c h n i q u ei sa l s od e s i g n e df o rv a l i d a t i n gx m l d o c u m e n t sa g a i n s ts t a t i cc o n - s t r a i n tf o r m u l a s b a s e do n a h o m e g r o w nw s c d lp r o g r a ms i m u l a t o r , w ep r o p o s e a i la u t o m a t i ct e s t - i n ga p p r o a c hf o rw s - c d ld o c u m e n t s t h i sa p p r o a c he m p l o y st e s tc a s e sg e n e r a t e df r o m s y m b o l i ce x e c u t i o nt oa u t o m a t i c a l l yt e s tw s c d ld o c u m e n t sr e g a r d i n gp a t hc o v e r a g e c r i t e r i a i ts u p p o r t sf e a t u r e ss u c ha se x c e p t i o nh a n d l i n ga n df i n a l i z a t i o nw h i c ha r ei g n o r e di no t h e rr e s e a r c h e s f u r t h e r m o r e ，w ei n t r o d u c et w ow a y so fh a n d l i n ga s s e r t i o n s w h i c ha r eu s e df o re x p r e s s i n gt h ed e s i r e db e h a v i o r a lr e s u l t sf o rw s - c d lp r o g r a m s w e i m p l e m e n tt h ea f o r e m e n t i o n e da p p r o a c h e si nam o d u l a rb a s e do p e ns o u r c ee 一 c l i p s ep l u g i nc a l l e dc d l c h e c k e r c d l c h e c k e ri sa ni n t e g r a t e dd e v e l o p m e n te n v i r o n m e n tf o rw s c d lw i t hf e a t u r e ss u c ha se d i t i n g ，s i m u l a t i o n ，v a l i d a t i o na n da u t o m a t i c t e s t i n g f i n a l l y , w ee v a l u a t et h ep r o p o s e da p p r o a c h e so nc d l c h e c k e rw i t hs e v e r a le x p e r i m e n t s t h ee x p e r i m e n t a lr e s u l t sr e v e a lt h a tt h ep r o p o s e da p p r o a c h e sw o r ke f f e c t i v e l y f o rw s c dl k e yw o r d s ：w e bs e r v i c ec o m p o s i t i o n ；w s - c d l ；r e l a t i o n a lc a l c u l u s ；p r o g r a m v e r i f i c a t i o n ；s y m b o l i ce x e c u t i o n ；t e s ta u t o m a t i o n r 一， 第一章 1 1 1 2 1 3 1 4 1 5 第二章 2 1 2 2 2 3 2 4 2 5 2 6 2 7 2 8 绪论 研究背景 研究现状 研究内容 论文结构 背景知识 目录 制约分析 方法概述 形式模型 约束逻辑 模型化简 静态制约检查 w s c d l 模拟器 动态制约检查 本章小结 第三章测试自动化 3 1 方法概述 5 9 5 9 1 l 2 4 6 6 4 4 7 1 5 7 2 6 7 9 9 3 7 9 0 1 l 6 7 1 1 1 2 2 2 3 3 3 3 3 4 4 4 5 5 5 5 5 5 2 本研究的不足6 0 参考文献 致谢 论文发表情况 6 8 6 9 7 0 l 一 第一章绪论弟一旱殖记 本章根据已有资料综述了w e b 服务流程组合技术的研究现状。并分析研究现 状并提出了本文的研究内容，陈述了本研究的贡献。本章最后介绍了本论文中涉 及到的相关背景知识。 1 1 研究背景 基于w i e b 服务( w e bs e r v i c e s ) 的面向服务架构( s e r v i c e o r i e n t e da r c h i t e c t u r e ，简 称s o a ) 技术为大粒度的软件复用提供了设计支撑。近年来，基于w e b 服务 的s o a 技术在企业的信息技术基础设施的设计和部署中得到广泛应用，企业已经 拥有许多定义良好的服务接口。组合现有的服务接口以提供功能更为强大的服务 产品具有成本低、风险小、较短的面市时间等优点。并且只有通过服务流程组合 才能发挥w 曲服务作为企业应用集成( e a i ) 的重要技术基础、跨组织机构、异构型 分布式计算的优势。w 幻服务流程组合技术因此而得到工业界广泛关注并且成为 近年w e b 服务研究领域的热点。 到目前为止，许多国际标准组织和服务机构都提出了自己的基于扩展标 记语言( 捌i ) 的服务流程建模语言以方便服务流程的集成，这些流程建模 语言包括x l a n g 【5 0 ，b p m l 1 l 】，w s f l 【3 2 ，w s c i 【1 2 ，w s c l 【1 3 ，x p d l 【4 9 】， w s b p e l 9 】，w s c d l 【3 】等，它们都提供用来表示可执行流程的模型。该流程模 型涉及到企业业务流程的各个方面，但它们使用了不同的范式。 x m l 流程定义语言( x p d l ) 为在不同工作流产品中定义的工作流程提供了 通用的交换格式作为一种交换语言，只可以支持任意内部表示到产品边界的 的标准转化，工作流建模和模拟工具可以生成x p d l 流程定义。b p m l 是一个基 于x m l 的元语言可以作为也为建模的方法。b p m l 有一个形式模型，该形式模 型设计到业务流程的各个方面，包括事物、补偿、并发以及异常处理等特性。 b p m l 并没有定义任何应用语义，只定义了表示一般流程的抽象模型和语法。在 实际中广泛使用的是业务流程执行语言( w s b p e l ) 。w s 。b p e l 是从单个参与方的 1 2 研究现状第一章绪论 视点描述服务组合中其他参与方应该遵守的交互规范。和w s b p e l 相比，w e b 服 务编排描述语言( w s c d l ) 贝j j 主要侧重描述从现有服务流程中组合新的业务流程。 w s c d l 是世界互联网协会关于w e b 服务编排的一个备选推荐方案，它从全局的 视角描述各个参与方为了协作所进行的交互规则，w s c d l 就像服务组合参与方 达成的协议。 尽管拥有这些语言，w 曲服务流程组合任然是一项高度复杂的任务，自动服 务组合仍然是一个巨大的挑战。 1 2 研究现状 当前由于w s b p e l 在工业界中得到广泛的支持与应用，w 曲服务组合研究的 重点对象是w s b p e l 语言。与w s b p e l 相比，w s c d l 更适用于跨组织机构的服 务组合描述所以具有很好的应用前景。w 曲服务编排语言的研究重点包括形式化 建模、性质验证以及测试自动化。其中w s c d l 程序测试自动化依赖其运行时环 境，w s c d l 程序运行环境的也必须得到了研究支持。 1 2 1 形式化建模 由于w s c d l 在设计之初并没有考虑到形式化的模型这给w s c d l 程序验证 带来了理论缺陷。在w s c d l 的形式化建模研究方面，b u s i 等在【1 8 】提出了一种 基于w s c d l 的编排描述语言。g o r r i e r i 在 2 6 提出7 w s c d l 中关键结构的形式 语义从而为处理交互提供了支持。蒲戈光小组在【4 3 ，5 2 ，5 3 也为w s c d l 的语言 子集提供了形式语义，但是他们省略t w s c d l 的些重要特性，比如编排组合 以及错误处理。 3 6 提出了一个基于r e o 和约束自动机的w s b p e l 和w s c d l 的 统一模型 1 2 2 模拟器 程序的执行依赖其程序可执行环境，由于w s b p e l 是可执行语言并且得到 了众多软件厂商支持，所以几乎没有以w s b p e l 可执行环境为对象的研究工作。 而w s c d l 只是一种描述语言其程序不可直接执行，当前只有一家软件厂商开发 7 w s c d l 程序的模拟运行环境( 简称为w s c d l 模拟器) 。在模拟器上模拟程序的 2 j 2 研究现状第一章绪论 执行可以形象地了解系统运行过程，理解程序动态行为。当前在w s c d l 模拟器 研究方面并没有太多的工作。王红兵小组 2 9 开发了一个名为w s c d l + 的执行引 擎，w s c d l + 基于一个扩展的w s c d l 语言为模拟w s c d l 程序提供了一个执行 环境，但这只是一个执行环境，并没有对w s c d l 文档的正确性做验证。p i 4 s o a 【2 开源项目基于7 r 演算【3 7 为w s c d l 提供了运行环境同时也提供了程序模拟功 能。 1 2 3 性质验证 近年来，在w 曲服务组合的性质验证方面研究者提出了一些方法【1 5 ，4 0 ，2 2 ， 2 3 ，2 4 。f u 等人【2 4 开发了一个名为w 曲服务分析工具( w e bs e r v i c ea n a l y s i st 0 0 1 ) ， 该工具使用模型检验验证w 曲服务组合的设计。他们用基于x p a t h 的带卫士条件 的有限状态自动机( g u a r d e df i n i t es t a t ea u t o m a t a ) 作为w 曲服务的中间模型，使 用s p i n 模型检查器 2 7 检验相关性质。o u y a n g 等在【4 0 通过将w s b p e l 流程翻译 成p e t r i 网，使用现有p e t r i 网分析工具静态检查是否满足某些性质。f o s t e r 2 2 开发 了一个使用名为带标记的迁移系统分析工具( l a b e l e dt r a n s i t i o ns y s t e ma n a l y z e r ) ， 使用有限状态进程( f i n i t es t a t ep r o c e s s ) 和消息序列图( m e s s a g es e q u e n c ec h a r t ) 同时 也使用w s b p e l 的一个扩展俩支持w 曲服务组合的建模与验证。a k e h u r s t 6 使用 对象约束语言( o b j e c tc o n s t r a i n tl a n g u a g e ，简称o c l ) 形式化描述w s - b p e l 的语言 约束，然后验证w s b p e l 文档的有效性。蒲戈光小组 4 u 也提出了类似的想法， 用u m l 和o c l 描述w s c d l 的语言约束。北大裘宗燕小组【5 4 也提出了验证w s c d l 核心功能子集的方法，他们也同样忽略掉一些重要的特性，比如说异常和 在 动 模 高 据 模 1 3 研究内容第一章绪论 型表示编排，从测试角度解决比如消息内容不一致等问题。k a t h r i n 等 3 0 提出了 基于公共协议的开放网络( o p e nn e t s ) 3 4 模型为交互的服务自动生成测试用例的 方法。w - e b 服务组合程序与传统的独立软件系统不一样，因此需要新的方法来测 试w 曲服务组合的设计。在w 曲服务组合的测试研究方面，很多研究者都做出了 贡献。张健小组 5 u 使用符号执行自动测试w s b p e l 程序，该方法将w s b p e l 程 序转换为x c f g ，在x c f g 上通过符号执行自动生成测试用例，但他们简化了一 些性质，比如范n l ( s c o p e ) 和异常处理。i b m 的b p e l 4 w su n i tt e s t i n g 3 3 i 具侧重 在w s b p e l 提供了测试流程自动化和用例重用。 1 3 研究内容 w s c d l 由于更适于描述跨组织机构的组合描述具有较好的应用前景，但当 前针对w r e b 服务组合的研究对象主要是w s b p e l ，w s c d l 并没有得到广泛的研 究支持。因此，本文将以w s c d l 为研究对象。 1 3 1 研究的问题 基于对以上研究现状的分析，结合自己的研究兴趣，本研究题试图解决当 前针对w s c d l 研究的问题和填补当前研究的不足。由于w s c d l 的全局性视角， w s c d l 适用于服务组合的设计阶段，而w s b v e l 贝, u 主要用来描述各个交互参与 者应在全局视角下需要其单方遵守的行为。由于w s c d l 被用在设计阶段，其正 确性直接影响到参与交互的所有参与方，为了保证各个参与方的行为最终正确， 保证w s c d l 程序的正确性是必需的。设计阶段的错误在系统实现后才发现并修 复的代价与在设计阶段就发现并修复所花费代价成几何倍数关系 7 】，所以尽早地 发现并修复设计的错误则会极大地降低开发成本。可以采用下面两种技术来达到 这个目标： 1 ) 通过程序分析技术来尽早发现程序设计错误； 2 ) 交互设计者还可以运用测试技术，通过模拟程序运行得到的反馈来进一步辅 助w s c d l 程序的正确性验证。 4 1 3 研究内容第一章绪论 w s c d l 的规范说明要求一个定义良好的w s c d l 程序必须满足其规范说明 中规定的性质。这些性质由“m u s t ”，“m a y 等关键字标示共有一百二十多条， 有静态性质和动态性质两类。这个现实给第一个目标的实现带来了极大的障碍， w s c d l 设计者在设计时很难同时准确地保证其程序满足这一百二十多条性质， 所以需要用计算机自动检查程序是否满足性质。传统的语言静态性质检查过程是 将静态性质检查行为硬编码，在程序编译时调用这些代码进行检查。这种方法的 缺点是不具有灵活性，当语言规范改变后这些硬编码的代码也必须更新。这种情 况对于w s c d l 等处于不断发展的语言尤其突出，目前w s c d l 现在还是w 3 c 下 的一个候选标准，其语言也经过最初的第一版到现在最新的第二版。因此，本文 对w s c d l 的研究主要集中解决以下两个问题： 1 由于w s c d l 具有十分复杂的语法和语义约束，能否提出新的w s c d l 约束 形式化描述模型以方便w s c d l 程序的制约检查。 2 w s c d l 由于不可直接执行所以在设计时对w s c d l 程序测试变得十分困 难，提出一种支持w s c d l 所有特性的自动化测试方法。 1 3 2 本文的贡献 w - e b 服务编排描述语言( w s c d l ) 是一种以全局视角来描述各个参与方 行为的x m l 定义语言。本文我们提出了两种方法来辅助程序设计者设计高质量 的w s c d l 程序，其一是在设计阶段对w s c d l 程序进行分析从而帮助服务组合 设计者尽早地发现程序的缺陷；其二是通过自动覆盖全路径测试帮助w s c d l 程 序设计者在部署前有效地发现缺陷。其中分析方法中提出了一种通用的基于关系 演算的性质检验方法，该方法适用于类似于x m l 的程序的分析。我们已经将本文 提出的方法实现了开源工具c d l c h e c k e r 。本文的具体贡献如下： 1 提出了一种基于一阶逻辑的通用x m l 语义约束描述语言一关系算子，该关 系算子不只能描述w s c d l 的约束，也能描述所有基于舭的语言的所有 静态性质。 2 基于以上约束描述语言，提出了类似模型检查的统一性质验证的方法，从而 改变了传统性质验证方式一需要针对不同性质编写不同的验证代码。 5 1 4 论文结构第一章绪论 3 提出了针对w s c d l 程序的基于符号执行的全自动分支覆盖方法。该方法能 在w s c d l 部署前对w s c d l 测试，增强服务组合流程设计者的信心，提高 流程质量。 4 将本文提出的方法实现为一个统一的工具c d l c h e c k e r ，包括约束分析功能， w s c d l 程序模拟功能以及自动测试功能。c d l c h e c k e r 作为e c l i p s e 插件的 开源项目，提供了用户界面以方便服务组合设计者编写、验证、模拟以及测 试w s c d l 程序。 1 4 论文结构 第一章，剩余部分将介绍本论文中用到的背景知识。简要描述了w 曲服务编 排描述语言、动态符号执行、模型检查的相关技术背景。 第二章，研究了w s c d l 程序验证的相关问题。提出了基于一阶谓词逻辑的 关系演算，统一地描述w s c d l 规范中的静态性质，采用类似模型检查技术验证 静态性质；提出了动态性质验证的相关相关方法。 第三章，研究了w s c d l 程序自动测试的相关问题。采用动态符号执行的方 法自动生成能达到的程序分支覆盖的参数输入值，在已经实现的解析器基础上采 用生成的输入值模拟运行w s c d l 程序从而测试程序时候能够满足期望的输出， 从而达到自动测试全程序的目标。 第四章，工具实现和相关实验。介绍了w s c d l 程序解析器、w s c d l 程序 验证方法和自动测试方法工具实现的相关问题给出了验证方法和自动测试方法 的相关实验设计以及实验结果分析。实验结果表明提出的方法能够有效解决程序 验证和自动测试的相关问题。 第五章，总结本论文的研究工作内容与研究的缺陷。 1 5 背景知识 w s c d l 作为w r e b 服务组合的备选推荐标准和本文的研究对象，它由于拥有 一些语法结构以及复杂的语义约束而不被大众知道，我将先介绍w s c d l 相关的 相关知识。我们用到类似于模型检查的检查算法自动检查对w s c d l 语义约束， 6 再则我们使用了符号执行相关技术自动生成测试用例，也有必要介绍一下符号执 行相关的知识。 1 5 1w s c d l w e b 服务编排描述语言( w e bs e r v i c e sc h o r e o g r a p h yd e s c r i p t i o nl a n g u a g e ) 是国 际互联网协会( w o r l dw i d ew e bc o n s o r t i u m ) 针对w 曲服务编排提出的主要标准。 它为描述多方参与的业务流程提供了一种实用性的方法。与抽象的w s b p e l 流程 一样，w s - c d l 的编排( c h o r e o g r a p h y ) 与w s - b p e l 抽象流程( a b s t r a c tp r o c e s s ) 只描 述多方参与的业务流程中外部可见的行为。 w s c d l 从全局描述点对点的协作流程，因此没有一个中心控制节点，协作 由各个参与方共同完成。w 曲服务接口作为协作的参与方，他们之间的交互具有 时间跨度长、有状态和受协调的特征。使用w s c d l 描述跨组织机构的协作能够 保证w 曲服务之间的一致性、互操作性增加协作的健壮性，也可以从w s c d l 中 生成各方的代码框架。需要提醒的是w s c d l 的编排只是组合流程的一个设计不 可执行。 模型概述 w s c d l 的模型包括以下组成要素： 1 角色类型，关系类型，参与方类型( r o l e t p e ，r e l a t i o n s h i p t y p e ，p a r t i c i p a n t - t y p e ) 。在一个编排中信息交换总是在参与之间进行，所有的交互是 在有关系的两个不同的角色之间进行。其中角色f l 了r o l e t y p e 定义，关系 m r e l a t i o n s h i p t y p e 定义，参与方被定义为p a r t i c i p a n t t y p e 。 2 信息类型，变量，标记( i n f o r m a t i o n t y p e ，v a r i a b l e ，t o k e n ) 。变量用以记录交换 的信息或者一个角色的可见信息，包括交换信息变量，状态变量。标记可以 用来表示一部分信息。 3 编排( c h o r e o g r a p h y ) 定义了交互参与方的协作流程。包括编排的生命周期、 异常处理模块、结束处理模块等。 7 1 5 背景知识第一章绪论 4 通道类型( c h a n n e l t y p e ) 实现了一个协作点用以表示交互的参与方在什么时 候可以以什么方式进行信息交换。 5 工作单元( w o r k u n i t ) 表示协作要前进的约束条件。 6 活动( a c t i v i t y ) 活动描述了一个编排里的动作。活动分为基本活动和顺序控 制活动顺序控制活动通过将基本活动和其他结构控制活动嵌套组合表示动 作之间的先后顺序关系。 7 交互( i n t e r a c t i o n ) 是编排里的基本活动用以完成不同参与方之间的信息交 换。 8 语义约束w s c d l 的规范说明中对每个结构有很多的语义和语法限制，这 些约束也是本文的研究问题之一。 主要结构 w s c d l 的各个结构之间的关系请见图1 1 在一个定义良好的w s c d l 文 档中有一个包( c d l ：p a c k a g e ) 。每个包包含信息定义和动作定义两个部分。其中 信息定义有变量定义，以及参与方相关定义；动作定义由一个或多个编排组 成。在w s c d l 中，各个协作参与方被定义为p a r t i c i p a n t ，一个参与方可以同时 拥有不同的角色( r o l e ) 。每个角色可以拥有多个动作( b e h a v i o r ) 。w s c d l 中的 变量定义可以分为状态变量和通道变量。一个编排被指定为”根编排”而作为 1 5 背景知识 第一章绪论 图1 1 ：w s c d l 文档结构 3 w o r k u n i t 在w o r k u n i t 中说明被包含的子结构执行的卫士条件或者循环执行 子活动的循环条件。卫士条件和循环条件可以包含有x p a t h 表达式和w s c d l 提供的函数。卫士条件和循环条件的计算方式阻塞式计算立即计算方 式( 通过设置w o r k u n i t 的b l o c k 属性实现) 。 4 c h o i c e 排他的选择执行。一般c h o i c e 以w o r k u n i t 作为子活动，按照子活动 定义的文本顺序计算它们的卫士条件，只有卫士条件满足后就执行对应 的w o r k u n i t 的动作。如果没有w o r k u n i t 子活动，选择哪个子活动执行是不确 定的。 基本活动是顺序控制活动的构成要素，包括以下结构： 1 i n t e r a c t i o n 用于描述两个角色之间的信息交换。需要指定用户信息交换的变 量名，也可以设定一个超时条件。如果其“a l i g n ”属性被指定为“t r u e ”，只 有两个角色都知道交互成功后其信息交换才最终有效，否则抛出异常信息交 换无效。 9 1 5 背景知识第一章绪论 2 n o a c t i o n 表示参与者不做任何动作，也可以用于描述从语法角度需要活动 的但又不做任何事情的地方。比如可用在e x c e p t i o n b l o c k q b 。 3 s i l e n t a c t i o n 可用于描述参与方的不可见但又必须要做的动作。 4 a s s i g n 用于在r 0 1 e 聊e 里创建，修改变量，变量的值为同一个r o l e t y p e 里的 表达式或变量值。也可用于产生异常。 5 p e r f o r m 通过复用已有编排的完成编排组合。一个编排通过使用p 加可以 1 5 背景知识第一章绪论 的谓词中搜集符号路径约束。在一条路径执行完后通过修改该符号路径约束内容 构造出新的可行路径的符号路径约束，并用约束求解器求解出一个可行的新赋值， 接着符号执行引擎在新赋值输入下进行一轮新的模拟执行程序。这样直到所有可 行路径都遍历完后动态符号执行过程就会终止。 动态符号执行与传统的静态符号执行方法相比，由于在执行过程中使用的是 具体值，仅在做路径收集时才会做符号运算，而路径收集数目远远小于程序执行 的语句数目，所以动态符号执行耗费的时间更少。 动态符号执行依赖程序的模拟器，并且符号执行的符号操作语义与具体执行 的操作语言具有区别，所以为了符号执行某种语言需要为该语言实现一个运行时 模拟器和符号操作语义。其中符号执行的操作语义是定义在c f g 之上，下面我们 定义c f g ： 定义1 5 1 函数厂的控制流程图gr = ( n ，e ) 中每个语句都有一个节点几o n ， 另外还有两个节点佗溉佗t 在厂中如果一个语句a i 紧接着语句口执行那么有一条 边( 几口，几o ，) e 对于，的第一条语句a l ，添加边( n 饥，扎口1 ) ，另外对每条语句0 7 在她执 行后控制流退出，则添加一条逆z ( n a 7 ，a o u t ) 空函数的卯g 定义为= 佗溉佗删) ，只 有一条边e = ( ，扎叫) ) 。 1 5 3 模型检验 模型检验( m o d e lc h e c k i n g ) 2 0 用来自动检查一个系统的模型m 是否满足由事 态逻辑( t e m p o r a ll o g i c ) 描述的系统需求p 。形式化地表示为：m p 或者m 乒p 。 模型检验具有全自动性，对于不满足的性质可以给出反例方便人工检查。模型检 查过程有3 个步骤：1 ) 系统建模将要验证的系统转换成模型检查器可以识别的形 式化模型。2 ) 需求描述系统需求用逻辑表达式表示，通常使用事态逻辑表示系 统需求，事态逻辑可以描述系统行为应该随着时间的流逝应该怎样变化。3 ) 验证 并分析而验证系统是否满足需求的过任务通常是自动化的。如果验证的结果是 系统不满足需求，用户可以得到导致错误的程序运行过程。对错误分析后可能需 要调整模型然后再重复上面的3 个步骤。这三个步骤详细的阐述如下： 1 5 背景知识第一章绪论 系统建模 首先要验证的系统需要转化为模型检查器可以处理的形式化输入格式。形式 化建模很重要但通常比较难。有时候，由于时间和空间的限制，对一个实际系统 建模通常需要采用一定的抽象技术。建模的时候需要考虑到实际系统中与验证性 质相关的点需要在抽象的而形式模型中表示出来，但又不能把不相关的细节抽象 掉，考虑过多无关细节会增加验证负担。 抽象系统中的一个状态( s t a t e ) 或配置( c o n f i g u r a t i o n ) 是系统中变量值在某一时 刻的系统快照。由一些动作带来的状态改变通常用状态迁移表示，系统迁移由致 该迁移发生的动作连接迁移前后两个状态表示。系统的运行是一个有限或无限的 状态序列，序列中的任意两个相邻的状态都是一个迁移。模型检查的系统模型 用k r i p k e 结构 2 8 表示 定义1 5 2 k r i p k e 结构m 是一个四元组m = ( s ，s o ，r ，l ) 其c s 是一个有限状态集 合；s o s 是系统的初始状态集合：s s s 为迁移关系；l ：s _ 2 a p 为标记 函数，它将每个状态标记上所有在该状态下为真的原子命题。其中a p 为非空原 子命题集合。 k r i p k e 结构可以用一个图表示，其中图中的节点就是其所有可达状态，边就 是其可达状态上的迁移。在本文中我们采用的是基于树形结构的模型，该模型 比k r i p k e 结构更简单。 需求描述和验证算法 需求就是一系列系统设计和实现都必须要满足的性质。性质可以使用不同方 法表示。在经典的有限状态模型中，性质通常用事态逻辑描述系统随着时间的发 展应该怎样变化。针对不同的模型和不同的性质要求可以使用不同的性质描述语 l 口。 传统的模型检查算法根据模型的不同表示有不同的算法，比如有基于自动机 的双深度优先搜索算法和基于b d d 的符号模型检查算法。模型检查算法的核心是 通过遍历模型所有状态判断性质公式是否满足。随着模型状态越来越多，会出现 全状态的遍历的代价变得不可能。这也就是所谓的“状态空间爆炸问题，针对 1 2 这个问题研究者们提出了针对特定模型或者性质的优化技术，比如抽象，对称化 简和偏序化简等。 第二章制约分析 弟一早币u 到万个丌 w s c d l 的语言规范中有一百多条由”m u s t ，”m a y ”等关键词描述的性质制 约，一个定义良好的w s c d l 文档( 本文从现在开始w s c d l 文档和w s c d l 程序 可以互换使用) 不仅需要符合由w s c d l 语言的s c h e m a 定义的语法形式，还需要 满足这些性质约束。w s c d l 性质检查是保证w s c d l 程序正确性过程中重要但 复杂的工作。针对w s c d l 的传统的性质制约检查方法需要对每个性质编写对应 的检查代码，不同类似于x m l 语言需要自己单独的检查代码，甚至对统一语言的 不同版本也需要重新编写检查代码。因此，该方法不具有可扩展性。 模型检查方法具有通用性，要检查不同性质只需要将要检查的性质用形式 逻辑描述后，整个检查过程自动完成。本章我们提出了类似于模型检查的性质 检验方法。在该方法中同样需要使用形式逻辑描述需要检查的性质，将要检查 的w s c d l 使用形式化模型表示后，通过搜索匹配算法自动完成w s c d l 程序是 否满足其性质制约。 本章首先通过一个w s b p e l 例子阐述通用静态性质制约验证方法，随后分别 介绍基于一阶谓词逻辑静态制约描述语言的语法以及语义，w s c d l 程序的形式 模型，基于搜索的性质检查算法。最后介绍w s c d l 静态性质制约描述的相关知 识。由于验证w s c d l 的动态性质依赖于模拟器，所以我们随后介绍w s c d l 模 拟器，最后介绍动态性质验证验证过程。 2 1 方法概述 本文提出的辅佐w s c d l 设计者的方法流程如下：1 ) 首先检查设计者编写 的w s c d l 程序是否满足