（计算机软件与理论专业论文）基于π演算的bpel4ws性质检验.pdf

摘要 随着w e b 服务的出现和推广，基于w e b 服务的动态服务组合技术也 成为近年的研究热点。w e b 服务的业务流程执行语言( b p e l 4 w s ) 作为一种 基于业务流程的服务组合方法，建模理论基础比较薄弱，组合正确性的 保证较弱。因此流程的正确性、无死锁性等问题，在它正式被实施前必 须得到形式上的模拟与检验。 基于形式化方法的研究工作，本文提出利用一演算和一演算对 b p e l 4 w s 进行性质检验的方法。 建模方面，除了提出利用一演算对b p e l 4 w s 的建模方法外，考虑 到手工建模的复杂度，在开发的检验工具中实现了一演算对b p e l 4 w s 建模的自动转换算法，用户可以利用本文的工具指定b p e l 4 w s 文件自动 生成其对应的一演算模型。 性质描述方面，分析b p e l 4 w s 可能出现的一些常规错误，并利用p 一演算给出了描述示例。 检验工具方面，开发了一个新的检验工具。实现上文提到的自动化 建模，嵌入已有的检验工具m w b ，对其检验算法加以改进，当模型不满 足性质时可以输出有错的子模型片段，并首次尝试把出错路径反馈到 b p e l 4 w s 源文件中做出标识，基本实现了对b p e l 4 w s 的自动化性质检验。 这样对于用户来说，从建模到检验几乎都是透明的，用户不用深入 了解形式化方法的知识，就可以直接用本文开发的工具进行性质检验， 并可以针对检验后标识的地方改进。本文的结果说明对b p e l 4 w s 的自动 1 化性质检验及出错路径的自动标识是可行的。 关键字：b p e l 4 w s ，模型检验， 一演算，“一演算 a b s tr a c t a 1 0 n gw i t ht h ep r o s p e r i t ya n da c c e p t a n c eo ft h ew e bs e r v i c e s ， t h et e c h n i q u eo fd y n a m i cs e r v i c ec o m p o s i t i o nb a s e do nw e bs e r v i c e s h a sb e e nr e g a r d e da so n eo ft h eh o tr e s e a r c ht o p i c s t h eb u s i n e s s p r o c e s se x e c u t i o nl a n g u a g ef o rw e bs e r v i c e s( b p e l 4 w s ) a st ob e as e r v i c ec o m p o s i t i o nm e t h o d ，w h i c hi sb a s e do nb u s i n e s sp r o c e s s ， i sw e a ki nm o d e l i n g ，a n dt h ea s s u r a n c eo ft h ev a l i d i t yi sa l s o w e a k s ot h ev a l i d i t yo ft h e p r o c e s sa n d t h e p r o p e r t y o f n o n d e a d l o c k sm u s tb es i m u l a t e da n dp r o v e db e f o r eb e i n g i m p l e m e n t e df o r m a l l y b a s e do nt h er e s e a r c ho ff o r m a lm e t h o d ，t h em e t h o do fc h e c k i n g t h ep r o p e r t yo fb p e l 4 w s ，w h i c hm a k eu s eo f了【一c a l c u l u sa n du c a l c u l u s ， h a sb e e np u tf o r w a r di nt h i sp a p e r 工nt h ea s p e c to fm o d e l i n g ，i na d d i t i o nt op u tf o r w a r dam e t h o d o fm o d e l i n g ，i nc o n s i d e r a t i o no ft h ec o m p l i c a t i o n so fm o d e l i n g b yu s e r ， w eh a v ec a r r i e do u tt h ea u t o m a t i cc o n v e r s i o na l g o r i t h m f o rm o d e l i n gt h eb p e l 4 w sb y 石一c a l c u l u s u s i n gt h et o o lm e n t i o n e d i nt h i sp 印e r ，t h eb p e l 4 w sf i l es p e c i f i e db yu s e rc a nc r e a t et h e 石一c a l c u l u sm o d e la u t o m a t i c a ll y 工nt h ea s p e c to fd e s c r i b i n gp r o p e r t y ，w eh a v ea n a l y z e ds o m e i i i e r r o r sw h i c ha p p e a rp r o b a b l yi nb p e l 4 w s ，a n dg i v e nt h ed e s c r i p t i o n e x a m p l ei n u c a l c u l u s i nt h ea s p e c to ft o o l ，w eh a v ed e v e l o p e dan e wt o o lw h i c h c a r r i e do u tt h ea u t o m a t i cm o d e li n gm e n t i o n e di np r e c e d i n gc o n t e x t t h i sn e wt o o l ， e m b e d d i n gt h eb e i n gt o o l 一m w ba n di 】p r o v i n g t h ea l g o r i t h ，c a nr e t u r n t h ee r r i n gs n i p p e tw h e nt h e o d e lc a n t f u l f i l ls o m eg i v e np r o p e r t i e s ，a n df i r s tt r yt or e m a r kt h ee r r o r p a t hi nt h eb p e l 4 w ss o u r c ef i l e ，i m p l e m e n t i n gt h ea u t o m a t i c a l l y c h e c ko nt h ep r o p e r t i e so fb p e l 4 w s i ti sa l m o s tt r a n s p a r e n tf r o mm o d e l i n gt oc h e c k i n gf o ru s e r s o ， t h eu s e rw h od o e s n tu n d e r s t a n dt h ef o r m a l e t h o dt h o r o u g h l y c a nd ot h ec h e c ku s i n gt h et 0 0 1a n dd ot h ei 唧r o v e m e n ta i m i n ga t t h et a g g e dp l a c e t h e r e s u l to ft h i sp a p e rh a se x p l a i n e dt h a t i tisf e a s i b l et oc h e c kt h ep r o p e r t yo fb p e l 4 w sa n dt a gt h ee r r i n g p a t ha u t o m a t ic a l l y k e yw o r d s ：b p e l 4 w s ， m o d e lc h e c k i n g ， 了【一c a l c u l u s ，u c a l c u l u s 基于一演算的b p e l 4 w s 性质检验 1 。1 研究背景 第一章绪论 随着i n t e r n e t 在各个领域应用的普及和深化，越来越多的数据资 源、计算资源与应用资源依托i n t e r n e t 成为可被公共获取和访问的网络 资源，如何有效地聚合开放网络环境下的各种资源成为具有广泛应用需 求的基础性研究问题。w e b 服务作为一种新的技术应运而生，提出了面 向服务的分布式计算模式，成为计算机领域的一个研究热点。w e b 服务 是一种使用诸如) ( m l 、s o a p 、w s d l 和u d d i 等w e b 标准的服务“1 ，其目的就 是在现有的各种异构平台基础上构筑一个通用的与平台无关、语言无关 的技术层，各种不同平台之上的应用依靠这个技术层来实施彼此的连接 和集成，提供一种开放式的发展平台，用于使用、展开、连接和管理分 布于全球的e s e r v i c e s 。但是单个的服务常常不能满足客户的需要，客 户需要的服务通常是由一系列不同的w e b 服务提供者提供的服务组合而 成。随着部署在i n t e r n e t 上的w e b 服务不断丰富，这些可被公共访问和 集成的服务构成了一个潜在的巨大标准组件库。因此，在w e b 服务互操 作技术的基础上，提供高层的服务集成手段、实现服务组合成为w e b 服 务技术发展的自然需求。 w e b 服务的业务流程执行语言( b u s i n e s sp r o c e s se x e c u t i o n l a n g u a g ef o rw e bs e r v i c e s ，简记为b p e l 4 w s ) 船3 是由i b m 和微软联合提 硕士学位论文 出的用于自动化业务流程的形式规约语言。它融合了w s f l ( w e bs e r v i c e f 1 0 wl a n g u a g e ) 和x l a n g ，采用结构、信息和行为等概念，定义w e b 服 务之间的业务流程行为，可以将已经存在的一组w e b 服务组合成一个新 的实现更复杂功能的w e b 服务。由于组合服务流程在实施服务组合的过 程中处于核心地位，组合服务流程的正确性决定了组合服务是否能正确 运行，有错的组合服务流程将导致有错的实现，在流程运行之后再更正 错误耗费巨大，所以在流程运行之前检验流程的正确性是很有必要的。 但是判断组合服务流程是否正确并不是轻而易举的事，尤其是对于具有 复杂流程逻辑的组合服务而言，仅仅依靠组合者的经验找出组合潜在的 错误是不可靠的。而且基于业务流程的服务组合方法一般由开发人员手 工完成，多基于非形式化的流程模型，建模理论基础比较薄弱，组合正 确性的保证较弱。所以w e b 服务业务流程的正确性、无死锁性等问题， 在它正式被实施前必须得到形式上的模拟与检验。但是对于w e b 服务的 组合语言现在很少提供整个流程正确性的保证方法。其中的原因并不仅 是因为流程的设计者没有认识到过程检验的重要性，更重要的是因为这 项工作从技术角度来看是非常困难的，这个问题已经引起了研究界和工 业界的高度重视，目前针对w e b 服务进行形式化检验已经成为当前w e b 服 务技术的热点之一。 1 2 研究现状 某些研究借鉴了工作流建模理论的成果，通过将组合服务模型与形 式化的建模方法，如p e t r i n e t 。1 、自动机或进程代数等形式化工具之间 基于一演算的b p e l 4 w s 性质检验 建立映射关系，从而为服务组合增强模型性质分析和检验的能力。这些 方面的研究目前刚刚起步，还很不完善。g p i c c i n e l l i 和s l w i l l i a m s 提出了类似c c s “1 的描述业务流程的演算，这个演算比较简单，不能描 述一些高级同步模式嘲。p e t r i n e t 提供了另一种业务流程建模方法1 ， z h a j l gj i a 提出了利用一种支持着色p e t r i n e t 语义和面向对象概念的描 述语言w s - n e t 来对w e b 服务进行检验的方法。“3 “。在w s 州e t 中，每个w e b 服务组件在三个层次被描述：接口网声明组件提供给其它组件的服务； 互连接网指定组件要完成其任务需要使用到的服务；互操作层描述组件 的内部操作行为。w s - n e t 实际是提出了一种体系结构模型，用于形式化 体系结构的拓扑结构以及每个服务组件的行为和系统行为，但是w s t 并没有提供将w s d l 转换成w s n e t 模型的自动转换工具。s c h r o e d e r 提出 了业务流程向c c s 的转换，接着用c w b ( t h ec o n c u r r e n c yw o r k b e n c h ) 口1 作检验哺1 ，但他研究的业务过程语言较本文研究的w e b 服务组合语言简 单。n a k a j i m a 描述了怎样用s p i n ( s i m p l ep r o m e l ai n t e r p r e t e r ) 阳”1 模 型检验工具去检验w e b 服务工作流，用于描述工作流的语言是w s f l ，它是 b p e l 4 w s 的前身之一，为了能用s p i n 检验，业务过程先要翻译成s p i n 提 供的p r o m e l a 规范语言“。将业务过程翻译成检验所用的形式化语言有 其缺点：不易将检验工具返回的出错路径与原来的过程联系起来。使用 l t s a 工具集和f s p 进程代数的方法“2 1 也有同样的弱点。k a r 鲫a n 0 1 i s 等人 将w e b 服务流程转换成f s p 进程( f i n i t es t a t ep r o c e s s ) 并使用l t s a 工具 ( t h el 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 ) 进行模型检验，”3 。l t s a 工具允许用户以确定性f s p 进程来指定属性，f o s t e r 等人描述了l t s a 工 硕士学位论文 具的b p e l 4 w s 插件m 3 “。他们把b p e l 4 w s 程序转换成f s p 进程并使用l t s a 工具来检验f s p 进程，但是l t s a 工具仅仅支持模型检验，而且f s p 进程所 能表达的属性集小于u 一演算所能支持的属性集。k o s h k i n a 等引入基于 b p e l 4 w s 的b p e 演算3 1 3 “，使用p a c 工具( p r o c e s sa l g e b r ac o m p i l e r ) 和 c w b n c 工具( c o n c u r r e n c yw o r k b e n c ho ft h en e wc e n t u r y ) 来建模和检 验w e b 服务协作。b p e 演算包含了b p e l 4 w s 的控制流结构，基于结构化操 作语义，b p e 演算作为p a c 的输入，其输出作为c w b 的输入，从而检验服 务组合，但是这一过程使得对b p e l 4 w s 进行检验变得比较烦琐。a n d r e a 提出用进程代数方法对w e b 服务、b p e l 4 w s 进行检验的思想m 1 ，并通过l 0 一 t o s 和b p e l 4 w s 的双向转换提出了两种方法对b p e l 4 w s 进行设计和检验， 虽然对检验内容作了阐述，但是却没有给出具体的检验方法以及如何有 效的利用这种双向转换。 已有的较普遍的模型检验工具如s p i n 、s m v ( s y m b o i i cm o d e l c h e c k i n g ) “，c w b 口1 其检验的系统模型与待检验的性质是交互输入的， 检验后的出错路径基于输入格式，与被检验的原系统结构相差甚远，要 求分析过程由人工进行。这需要检验者对工具的输入有一定的了解，并 要能反馈到真实系统中，对检验者有比较高的要求，延缓了对组合语言 进行形式化方法验证的应用。本文根据自动w e b 服务组合的运行环境， 开发性质检验的自动过程：系统模型与待检验性质的输入、检验后的出 错路径显示、根据检验结果对原系统做出标识。这意味着要对现有的检 验工具进行改进或者研制新型的检验算法和工具。 由于w e b 服务是在整个i n t e r n e t 上进行交互和组合，其面对的组合 基于一演算的b p e l 4 w s 性质检验 对象和环境( 如连接状况等) 复杂多变，同时鉴于专门用于描述移动进 程的一演算“3 “1 在描述这类问题上具有一定的优势，而且一演算在语 法结构上和本文要检验的b p e l 4 w s 结构比较相似，有利于实现两者之间 的相互转换，因此本文将采用一演算来进行建模，描述将b p e l 4 w s 映射 到兀一演算的自动映射方法，对得到的兀一演算表达式利用基于移动工作 台( m o b il i t yw o r k b e n c h ，m w b ) “5 1 1 开发的检验工具进行性质检验，并 把出错信息标识到b p e l 4 w s 源文件反馈给用户，实现自动化的检验过程。 1 3 本文的主要工作 1 3 1 研究内容 本文的研究工作主要是利用兀一演算“。“1 和u 一演算“8 1 对b p e l 4 w s 进 行性质检验。建模方面，除了提出利用丌一演算对b p e l 4 w s 的建模方法 外，考虑到手工建模的复杂度，在开发的检验工具中实现了丌一演算对 b p e l 4 w s 建模的自动转换算法，用户可以利用本文的工具自动生成指定 b p e l 4 w s 文件对应的一演算模型。性质描述方面，分析了b p e l 4 w s 可能 出现的一些常规错误，并利用u 一演算给出了描述示例。检验工具方面， 开发了一个新的检验工具，实现上文提到的自动化建模，嵌入已有的检 验工具m w b ，对其检验算法加以改进，当模型不满足性质时可以输出有 错的子模型片段，并把出错路径反馈到b p e l 4 w s 中作出标识，基本实现 了对b p e l 4 w s 的自动化性质检验。这样对于用户来说，从建模到检验几 乎都是透明的，用户不用深入了解形式化方法的知识，就可以直接用本 文开发的工具进行性质检验，并可以针对检验后标识的地方进行改进。 硕士学位论文 本文的结果说明对b p e l 4 w s 的自动化性质检验及出错路径的自动标识是 可行的。 1 3 1 1b p e l 4 w s 的建模 利用兀一演算对b p e l 4 w s 进行建模。本文考虑的是w e b 服务组合在 流程上的正确性，数据的兼容性问题不在本文的考虑范围内。而且鉴于 建模规则，由于时间和空间的限制，对一些细节进行抽象，忽略一些内 部细节。针对b p e l 4 w s 的有些活动与外部环境没有任何交互，统一把这 种类型的活动看作一演算中的内部动作。其它与外部环境有交互行为 的外部原子活动和结构化活动是本文的重点研究对象，通过分析其语法 结构给出了建模方法。对流程有影响的链接也纳入考虑并进行建模。 1 3 1 2b p e l 4 w s 的性质描述 b p e l 4 w s 是基于业务流程的组合方法，由于基于业务流程的服务组 合方法一般由开发人员手工完成，多基于非形式化的流程模型，建模理 论基础比较薄弱，所以当流程逻辑比较复杂时，有可能产生不易察觉的 错误，组合正确性的保证较弱。本文通过分析流程中可能出现的一些错 误，并利用u 一演算针对错误描述一些流程应该满足的性质，方便用户 直接调用或者进行一定的扩充来进行检验。 1 3 1 3 检验工具 开发了一个新的检验工具。该工具嵌入已有的检验工具m 1 l b ，对其 基于一演算的b p e l 4 w s 性质检验 检验算法加以改进，并实现自动建模和出错路径自动标识两大功能，基 本实现了对b p e l 4 w s 的自动化性质检验。首先，在利用一演算对b p e l 4 w s 建模的基础上实现了从b p e l 4 w s 到一演算的自动转化过程。用户不需 手工建模，只需指定b p e l 4 w s 文件就可以利用工具自动生成相应的“一 演算模型。其次，嵌入已有的检验工具m w b ，对其检验算法加以改进， 在系统出错时将会返回出错路径信息。最后，现有的检验工具在返回出 错路径时表现形式一般以工具的输入形式为基础，与被检验系统的原结 构有一定差距，用户必须从复杂的表达式中读懂错误信息并且自己反馈 到原系统中。本文通过一演算到b p e l 4 w s 的匹配过程，首次尝试将出 错路径自动反馈到原系统中并作出标识。用户不仅可以从一演算形式 的出错路径中分析错误，还可以直接从b p e l 4 w s 文件中被标识的部分分 析错误并加以改进。 1 3 2 研究难点和技术路线 本文在研究过程中存在的难点以及解决的技术路线如下： 在利用丌一演算对b p e l 4 w s 建模时，因为一演算中没有顺序表 达式，所以对b p e l 4 w s 中的s e q u e n c e 活动建模时不能直接映射 到一演算的顺序结构。本文采用在并发中加上通道传输、接受 消息来控制活动的执行顺序，即利用并发表示顺序来解决这一 问题。 已有工具m w b 在性质检验时并没有出错路径的提示，本文通过 分析其算法并加以改进，给予出错路径的提示。 硕士学位论文 对m w b 改进后出错路径的输出以一演算的形式给出，如何把 一演算的信息反馈到b p e l 4 w s 中是个难点。因为在建模过程中 b p e l 4 w s 和一演算之间并不是一一映射，所以本文利用工具s m l 语言中的注释语句，通过在丌一演算模型中加上注释，解决了 b p e l 4 w s 和一演算之间的非一一映射问题。 1 3 3 创新之处 b p e l 4 w s 在运行前得到形式化的检验有一定的难度，其中一个原 因就是因为这项工作从技术角度看是非常困难的，组合者不仅 需要掌握组合语言的知识，而且还要了解形式化方法的知识。 本文给出的从一演算到b p e l 4 w s 的自动转换算法则使用户可以 不用掌握建模知识就可以自动为b p e l 4 1 | f s 文件建立相应的模型。 提出用u 一演算描述要检验的性质。对于b p e l 4 w s 的形式化检验， 本文初步作出利用u 一演算描述性质进行检验的尝试，这样用户 可以根据实际情况定义各自需要满足的性质，而不是仅仅局限 于检验其死锁、互模拟等性质，增强了b p e l 4 w s 形式化检验的 灵活性。 理想的检验是完全自动的，然而实践中经常需要人来辅助。这 些人工的活动是分析检验的结果。在否定结果的情况下，通常 要给用户提供错误路径。这可以作为被检验性质的反例，能帮 助用户跟踪错误在哪出现。但是现有工具一般只支持以工具的 输入形式返回出错路径，与被检验的系统结构有很大差距，需 基于n 一演算的b p e l 4 w s 性质检验 要用户熟悉工具的输入与原系统的对应，并且能把出错路径返 回到原系统中，否则出错路径将没有任何意义，但是这个过程 需要一定的专业知识作为基础，具有一定的难度。对于本文研 究的b p e l 4 w s 性质检验来说，如果仅仅用一演算来表示错误信 息，用户可能还是不知道对应于b p e l 4 w s 文件到底哪里出现问 题，因此本文首次实现将出错路径返回到b p e l 4 w s 源文件，这 样即使用户不能读懂一演算的出错路径，也可以直接根据 b p e l 4 w s 文件中的错误标识来进行分析改进。 1 4 本文结构 本文分为七章，论文结构及各章节的关系如图卜1 所示： 第一章为绪论，阐述本文的研究背景、现状和内容。 第二章介绍模型检验的一些基本知识。首先介绍了模型检验的基本 思想和主要流程，然后根据不同的逻辑表示方式以及支持它们的工具进 行了介绍。 第三章利用一演算对b p e l 4 w s 进行建模。首先简单介绍了一演算 和b p e l 4 w s ，然后研究利用豇一演算对b p e l 4 w s 的建模方法。 第四章利用u 一演算描述性质。首先简单介绍u 一演算，然后对 b p e l 4 w s 行为进行分析，最后研究如何利用u 一演算来描述性质。 第五章介绍检验工具。首先介绍b p e l 4 w s 到演算的自动映射方 法，其次介绍m 1 】l b 中已有的检验算法，并对该算法做出的改进，最后介 绍将一演算的出错路径反馈到b p e l 4 w s 的实现。 硕士学位论文 第六章结合一个具体的b p e l 4 w s 实例给出对其性质检验的示例。 第七章总结全文，并对下一步工作进行展望。 图卜1 论文组织结构 基于n 一演算的b p e l 4 w s 性质检验 2 1 简介 第二章模型检验 随着计算机系统规模的不断增大，功能日趋复杂，系统开发中出现 错误和问题的可能性也越来越大，因而给系统的开发和维护带来许多困 难。为了提高系统的可靠性，对系统进行严格的检验越来越受到广泛的 重视。目前在实际应用中，普遍采用的方法是对系统进行大规模的测试， 通过输入多个测试用例并检查执行结果是否正确来发现系统中可能存 在的问题，但是这种方法在检验系统时通常无法穷举系统所有可能的行 为。因此人们提出了形式化方法，希望借助数学工具来完成系统的检验 工作。形式化方法就是用数学与逻辑的方法对系统进行描述和验证“。 从描述上讲，一方面是系统或程序的描述，另一方面是性质的描述。可 以用一种或多种语言来描述，这些语言包括命题逻辑、一阶逻辑、高阶 逻辑、代数、状态机、并发状态机、自动机、计算树逻辑、线性时序逻 辑、进程代数、一演算、u 一演算、特殊的程序语言以及程序语言的子 集等。 在过去二十多年间，各国研究人员为解决这个问题付出了巨大的努 力，取得了重要的进展。在提出的诸多理论和方法中，模型检验( m o d e l c h e c k i n g ) 以其简洁明了和自动化程度高而引人注目。 模型检验是一种很重要的自动分析和检验技术。主要通过显式状态 搜索或隐式不动点计算来检验有穷状态并发或实时系统的模态命题性 硕士学位论文 质。模型检验的研究始于八十年代初，当时c l a r k e 、e m e r s o n 等人妇们提 出了用于描述并发系统性质的c t l 【2 “逻辑，设计了检验有穷状态系统是 否满足给定c t l 公式的一个算法，并实现了一个原型系统。这一工作对 并发系统的性质检验开辟了一条新的途径，成为近二十年来计算机基础 研究的一个热点，被广泛应用于计算机硬件、通信协议、控制系统、安 全认证协议等方面的分析和验证中，近年来更被引入软件工程，用来辅 助较大规模软件系统的分析和验证中，取得了令人瞩目的成功。许多大 公司，如i n t e l 、h p 、p h i l l i p s 等成立了专门的小组负责将模型检验技 术应用于生产过程中啪1 。 一 模型检验的基本思想是用状态迁移系统( s ) 表示系统的行为，用模 态时序逻辑公式( f ) 描述系统的性质。这样“系统是否具有所期望的性 质( 模型是否满足性质) ? ”就转化为数学问题“状态迁移系统s 是否 是公式f 的一个模型? ”。 模型检验的主要流程参见图2 1 ，主要包括下面三个步骤： 建模：为系统建立形式化模型，使用模型检验工具能够接受的形 式语言来刻画系统。在某些情况下，由于时间和空间的限制， 建模需要进行抽象来消除无关或不重要的细节，用户将根据需 要和检验的系统类型选择相应的形式化描述方法，尽可能地忽 略冗余信息，保留与待检验性质相关的特征。 性质：在检验之前需要描述系统必须满足的性质，一般用某种 逻辑公式给出。模型检验只能检验模型是否满足给定的公式， 因此所提供的公式是否完整正确地刻画所关心的性质是得到正 基于n 一演算的b p e l 4 w s 性质检验 确检验结果的必要前提。 检验：把建模的结果和需要满足的性质输入工具来检验所给的 模型是否满足所关心的性质。狭义的检验就是简单的判定系统 的形式化模型是否满足所关心的性质，而从广义上来讲，这是 一个检验一报错一报错信息分析和模型修改一再检验的循环过 程。 图2 一l 模型检验的流程 不同的性质描述形式有不同的支撑工具来进行检验，本文将在下面 介绍几种应用不同的逻辑表示方式来进行模型检验的工具。 2 2 模型检验工具 2 2 1 基于计算树逻辑的模型检验工具 计算树逻辑( c o p u t a t i o nt r e el o g i c ，简写为c t l ，又叫分支时序 逻辑) 。”是一种分叉时序逻辑，是针对具有分支路径的状态转换图( 比如 个并发系统从一个初始状态开始运行，由于行为的不确定性，它可以 有多个可能的后续状态，每个这样的状态又可能有多个后续状态，依次 1 硕士学位论文 类推可以产生一颗状态树。) 定义的逻辑，可以描述状态的前后关系和 分支情况。c t l 公式由原子命题、逻辑连接符和模态算子组成。逻辑连 接符包括： ( 非) 、八( 与) 和v ( 或) ，它的模态算子表示有关分支路径 的特征，由两部分组成：一个是路径量词a 和e ，描述分支情况。其中 a ( a l w a y s ) 表示所有分支，e ( e x i s t s ) 代表至少存在一个分支。另一个是 表示时序的时间操作符f 、g 、u 和x ，描述状态的前后关系。其中 f ( f u t u r e l ) 最终操作符，表示现在或以后某一状态；g ( g l o b a l ) 全程操 作符，表示现在和以后所有状态；u ( u n t i l ) 直到操作符，表示直至某一 状态；x ( n e x t ti m e ) 次态操作符，表示下一个状态。c t l 中的路径量词 和表示时间的时序操作符必须成对出现，即一个路径量词的后面必须有 一个时序操作符。例如e g f 表示存在一条路径，且该路径上的每个状态 都满足f 。 s m v “”是美国卡耐梅隆大学开发的模型检验工具，用于检验一个有 限状态系统是否满足c t l 公式。其输入语言是以i ( r i p k e 结构作为语义 模型，描述有限i ( r i p k e 结构上的状态迁移关系，并支持模块化建模方 式。模块描述的基本元素包括不确定选择、状态迁移和并行赋值语句。 模块间基于共享变量方式进行通信。其模型检验的基本方法是用有序二 叉图( o b d d ) 表示状态迁移关系，用计算不动点的方法检测状态的可达性 和所满足的性质。 2 2 2 基于命题线性时序逻辑的模型检验工具 命题线性时序逻辑( p r o p o s i t i o n a ll i n e a rt e m p o r a ll o g i c ，简写 基于n 一演算的b p e l 4 w s 性质检验 为p l t l ) 晗”描述的是系统任意一次运行中的状态以及它们之间的关系。 p l t l 把时间轴看作一个线性序列，时间轴上存在一个无限状态序列，状 态之间按照一个隐含的时间参数严格排序，对每个状态都有唯一的后继 状态与其对应。c t l 把系统状态变化的可能性看成是一种树状结构，p l t l 则把系统状态变化看成是一些路径的集合，每条路径代表系统一次可能 的运行情况，也就是树状结构中的一条路径。p l t l 公式也由原子命题、 逻辑连接符和模态算子组成。逻辑连接符包括： ( 非) 、八( 与) 和v ( 或) ，模态算子包括f 、g 、u 和x ，其中f ( f u t u r e l ，也可以用表示) 最终操作符，表示现在或以后某一状态；g ( g l o b a l ，也可以用口表示) 全程操作符，表示现在和以后所有状态；u ( u n t i l ) 直到操作符，表示直 至某一状态：x ( n e x t t i m e ) 次态操作符，表示下一个状态。 s p in 9 埘是美国贝尔实验室开发的模型检验工具，用于检验一个有 限状态系统是否满足p l t l 公式及其它一些性质。其输入语言是p r o m e l a ， 在语法上与c 接近，其程序由进程、通道和变量构成。它通过把p r o m e l a 语言所写的程序转化成有限状态自动机，并和需要满足的性质( p l t l 公 式) 所构成的自动机的补相乘，断定得到的自动机所识别的语言是否为 空，从而验证系统模型是否满足性质。 2 2 3 基于u 一演算的模型检验工具 以上介绍的两种逻辑语言关心的是系统的状态以及他们之间的关 系，系统状态的改变总是由某种动作引起的，因此出现了一种关心系统 动作和状态之间关系的逻辑语言一u 一演算。p 一演算的具体介绍可以参 硕士学位论文 见本文第四章。 c 霄b 口1 的不同版本是英国爱丁堡大学和美国北卡洛莱纳州力大学相 继开发的模型检验工具。用以检验系统间的等价关系，p r e - o r d e r 关系， 以及系统是否满足u 一演算公式。它的建模语言为纯c c s 语言或者l o t o s 语言( 的子集) ，由于建模语言的局限性和模型检验方法复杂度较高， 这个工具的可应用性比前面描述的工具稍微差一些。 m w b “5 j 6 3 是一个用于操作和分析基于豇一演算描述的移动并发系统的 工具，用s m l 语言开发，在n e wj e r s e ys m l 编译器下运行。可以验证 死锁问题，判断有穷状态进程之间的开互模拟性，可分别验证强互模拟 和弱互模拟以及系统是否满足u 一演算公式。本文的工作将基于这个工 具展开。 因为u 一演算的表达能力非常强，c t l 和p l t l 都可以嵌入到它的真 子集中，且相应的子集具有与c t l 和p l t l 相同复杂度的模型检验算法， 因此本文将选择利用u 一演算来描述性质进行性质检验。 由于本文要检验的是w e b 服务的组合语言b p e l 4 w s ，鉴于w e b 服务 是在整个i n t e r n e t 上进行交互和组合，其面对的组合对象和环境复杂 多变，而用于描述移动进程的丌一演算在描述这类问题上具有一定的优 势，本文将采取利用一演算建模，u 一演算描述性质的基本思想来进行 性质检验。 基于n 一演算的b p e l 4 w s 性质检验 3 1 耳一演算 第三章一演算建模b p e l 删s 一演算是r m i l n e r 等人在c c s 的基础上提出的传名演算，可描述 通信拓扑结构动态变化的分布式通信系统1 。它允许进程之间传送和接 收通道名，并且可以引入和输出局部名。与传值c c s 不同，演算将 数据值、数据变元、输入参变元以及传递数据的通道不加区别，一律作 为名字来处理。因此，丌一演算不仅非常简洁，而且具有很强韵表达能 力。本文的研究基于一演算中不带类型的丌一演算，如果不作特殊说明， 本文中的一演算都指不带类型的一演算。 3 1 1 兀一演算的语法定义 设n 为无限名字集，用x 、y 、z 等小写字母表示名字集上的名字； 用a 、b 、c 等大写字母表示进程标识符；用p 、q 、r 等大写字母表示进 程表达式，一演算的语法定义如下： 尸：= ol 口p p + qp lql 【x = ，】pi ( w ) 尸i ! p4 ( 而，矗) 引= ri ( 功l i 解释如下： ( 1 )o 是一个不能做任何动作的进程； ( 2 )口是动作前缀，在孔一演算中有三类基本动作：t 表示内部通 信动作，口( x ) 表示输入动作，二 表示输出动作； ( 3 ) p + q 是不确定选择，表示选择执行p 或q ； 17 硕士学位论文 ( 4 )p i q 是并发表达式，表示并发执行p 和q ； ( 5 )瞳= y 】p 是匹配表达式，表示当工和y 相等时，执行进程尸，否 则执行进程q ； ( 6 )( 啪p 是限制表达式，表示名字x 是p 的私有名字； ( 7 )! 尸是重复表达式，表示，的无穷个复制； ( 8 ) 爿“，) 是进程标识符， 爿( 耳，) 对每个进程标识符来说， 必须有其定义爿( 咒，儿) ：= p ，其中m ，以是户中的自由名； 在名字限制( w ) p 和约束输入动作口( x ) 中，名字工在p 的范围内是约 束的，称为p 的约束名。形如( 惯) 尸的约束名表示引入了一个新的局部化 名字x ，其辖域为p ，不能被实例化。而形如a x ) 的输入参数名工只是一 个占位符，可被实例化；在p 中出现，但是没有被约束的名字称为p 的 自由名，一个进程所具有的自由名代表了该进程当前所拥有的关于其它 进程的知识或其它进程的联系。一般用力( 尸) 表示进程p 的自由名，抽( 尸) 表示进程p 的受限名集。 3 1 2 一演算的操作语义 1 9 肛：磊面： ， 尸旦斗尸 ( 2 ) s 咖：二_ 二二_ 一： | p + d 与p ( 3 ) i d e ：筹考( 删卅 爿( y ) ! l + p 、 ( 4 ) m a t c h ： ! 二兰三 ： f x = x 1 p 竺 p 基于n 一演算的b p e l 4 w s 性质检验 ( 5 ) p a r ：= 笔熹6 ，z ( 口) n 力( q ) ：矿： 尸i9 已p l9 、 一。 删：焉釜瑞：尸iq 二 p 。iq l ，y ) ( 7 ) c l o s e ：! 二竺! ! j 垡二：! ! ! ! 望! ： 尸iq 二斗( ) ( p iq ) ( 8 ) r e s ：i ：= ：；二兰，x 仨n ( 口) ： ( 惯) p 兰斗( 啪p t 。 一 ( 9 ) 0 p e n ：土芸掣t 一，x 栅z 芒力( ( 切尸x ( 们尸三三三_ p 扛y 。 c ，唧：淼 关于兀一演算的详细介绍可以参考文献“3 “。 3 2b p e l 4 w s 商业流程执行语言b p e l 4 w s ( 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 f o rw e bs e r v i c e s ) 是专为整合w e b 服务而制定的一项规范标准。它从 本质上说是i b m 的w s f l 和m i c r o s o f t 的x l a n g 的结合物，目前已经成 为业界标准。w s f l 支持图形化的流程，x l a n g 在结构化构造方面有独到 的方法，而b p e l 4 w s 正是吸取了两者的优点，同时摒弃了一些复杂繁琐 的部分，形成了一种较为自然的描述商业活动的抽象高级语言。 b p e l 4 w s 的文法是完全基于瑚l 规范的，如果不考虑它的程序语言 特性，完全可以把它理解为普通的) 【m l 文档规范，所以可以用d o m 方法 来解析b p e l 4 w s 文件，为本文后面的自动化建模提供了基础。 b p e l 4 w s 用于建模两种类型的流程，可执行业务流程和抽象业务流 硕士学位论文 程。抽象业务流程是业务协议的抽象，它说明了业务双方消息交换的方 式，并且没有泄漏双方内部的行为。可执行业务流程说明了活动执行顺 序，涉及的伙伴( i b m 在其网站上将p a r t n e r 翻译为伙伴) ，伙伴间交 换的信息及错误和例外处理机制。 下面简要地介绍b p e l 4 w s 的语法，该语言的基本结构是： 表3 1b p e l 4 1 s 的基本结构 基于一演算的b p e l 4 w s 性质检验 上文中的符号“? ”表示o 个或1 个，“木 表示o 个或多个， “+ ” 表示1 个或多个。 最高级别的属性如下： q u e r y l a n g u a g e 属性指定在赋值、特性定义和其它使用中用于选 择节点的l 查询语言。缺省值是x p a t h l o ，其代表是x p a t h l 0 夫见范的u r i ：垫篮仑；厶堂凸业：迎墨：q 固丛8 ! 垒坌坌基星坌：基q 坌l b ：! 垒垒窒! 11 昼。 e x p r e s s i o n l a n g u a g e 属性指定在流程中使用的表达式语言。缺 省值是x p a t h1 0 ，其代表是x p a t h1 o 规范的u r i ： 2 l 硕士学位论文 砼丝q ；型皇! 6 型：垫：q g ! 基! 星殳窒尽量；：丕仑坌! 垒：! 旦星坌】11 鱼。 s u p p r e s s j o i n f a i l u r e 属性决定是否抑制流程中所有活动的 j o i n f a i l u r e 故障。该属性在流程级的作用可以被使用该属性的 其它值的活动所覆盖，缺省值是“n o ”。 e n a b l e i n s t a n c e c o m p e n s a t i o n 属性决定流程实例是否可被作为 整体由特定于平台的方式来补偿，缺省值是“n o 。 a b s t r a c t p r o c e s s 属性指定所定义