当前位置：文档库 › 一种基于认知模型检测的Web服务组合验证方法

一种基于认知模型检测的Web服务组合验证方法

第34卷第6期2011年6月

计算机学报

CH INESE JOURNA L OF COM PU TERS

Vo l.34N o.6

June 2011

收稿日期:2010-11-20;最终修改稿收到日期:2011-05-18.本课题得到国家/九七三0重点基础研究发展规划项目基金(2010CB328103)、国家杰出青年科学基金(60725207)、国家自然科学基金(60763004、61073033)、中国博士后科学基金(20090450389)、华侨大学中央高校基本科研业务费项目(JB -GJ1001)和华侨大学高层次人才科研启动费项目(11BS108)资助.骆翔宇,男,1974年生,博士后,副教授,主要研究方向包括模型检测、时态逻辑、认知逻辑、知识推理、多主体系统、安全协议验证等.E -mail:s hian gyuluo @https://www.wendangku.net/doc/d814626218.html,.谭征,男,1982年生,硕士,主要研究方向为模型检测、Web 服务.苏开乐,男,1964年生,博士,教授,博士生导师,主要研究领域包括模型检测、知识推理、非单调推理、多主体系统、模态逻辑、时态逻辑、概率推理、安全协议验证、逻辑程序设计等.吴立军,男,1965年生,副教授,主要研究方向为人工智能与网络安全.

一种基于认知模型检测的Web 服务组合验证方法

骆翔宇

1),2)

谭征3) 苏开乐

4),5)

吴立军

(华侨大学计算机科学与技术学院福建厦门 361021)

(清华大学软件学院北京 100084)

(中核兰州铀浓缩有限公司兰州 730065)

(北京大学教育部高可信软件重点实验室北京 100871)

(浙江师范大学数理信息学院浙江金华 321004)

(电子科技大学计算机科学与工程学院成都 410073)

摘要近几年Web 服务组合的形式化验证逐渐成为研究热点.模型检测作为形式化验证的一种主流技术,可以克服传统软件测试用例生成不完备的不足,同时具有验证自动化的优点.该文提出并实现了一种W eb 服务组合的认知模型检测方法,将W eb 服务组合建模为多主体系统,在分析BP EL 语言控制流程基础上,提出BP EL 活动的形式化模型,给出活动执行语义.进而以迁移七元组为中间形式,开发从BP EL 流程到迁移七元组集合以及从这些迁移七元组到M CT K (一种我们开发的多主体系统模型检测工具)输入语言的自动转换算法,最终通过M CT K 进行验证.实验结果表明开发的算法不仅可以有效验证Web 服务组合的时态逻辑规范,而且可以验证多主体系统特有的认知逻辑规范及其时态组合.

关键词模型检测;W eb 服务组合;BPEL;认知逻辑;多主体系统中图法分类号T P 301 DOI 号:10.3724/SP.J.1016.2011.01041

A Verification Approach for Web Service Compositions

Based on Epistemic Model Checking

LUO Xiang -Yu

1),2)

T AN Zheng 3) SU Ka-i Le

4),5)

WU L-i Jun

(Colle ge of Comp ute r Sc ienc e &Tec hnology ,H uaqiao Unive rsity ,X iamen,F uj ian 361021)

2)(S chool of S of tw are ,T singh ua Univ er sity ,B eij ing 100084)

(China N ational N uclear Corp or ation,N o 504P lant,L anz hou 730065)

(K ey la borator y of H ig h Conf idenc e S of tw are T ech nologies of M inistr y of E du cation (P eking Univ er sity ),Beij ing 100871)

(College of M athe matics Phy sics and I nf or ma tion Eng ineering ,Zhej iang N or mal Univ er sity ,Jinhua,Zhej iang 321004)

(S ch ool of Comp ute r Sc ienc e and Eng ine ering ,Univ er sity of Elec tr onic S cience and T ec hnology ,Cheng d u 410073)

Abstract In recent years,the formal v er ification of Web serv ice com po sitio ns is g radually be -coming a hot research area.As a mainstream technique for form al verification,m odel checking is

able to no t o nly overcome the shor tcoming o f traditional softw are test techniques that they cannot generate the com plete set of test cases,but also auto matizes the verificatio n pr ocess.In this pa -per,the autho rs propose and implement an epistemic m odel checking approach for the verification of Web service compositions by m odeling them as mult-i agent systems.After analyzing the BPEL

control flo w,the autho rs fir st pr opo se a form al m odel for the BPEL activ ities and give the seman -tics o f the im plementation of the BPEL activities.By taking the so -call transition seven -tuple as

the interm ediate form,the authors further develop tw o automatic transform alg orithms,one con-v erts the BPEL pro cess to the set o f sev en-tuples and the other converts this set of seven-tuples to the input language of M CTK(a m odel checker fo r mult-i ag ent sy stems developed by the authors),such that can finally implement the v er ification by MCT K.T he ex perimental results show that the proposed alg orithm s can effectively verify no t o nly the temporal lo gical specifica-tions,but also the tem po ral epistemic lo gical specifications,w hich are pro per to m ult-i ag ent system s.

Keywords m odel checking;Web service compositions;BPEL;epistem ic log ic;mult-i agent system s

1引言

随着面向服务的体系架构(SOA)的出现,许多软件资源与应用都封装成为服务,服务提供以功能为单位的调用标准,对服务的调用者展现统一的调用接口,而屏蔽服务的实现细节.可以说SOA将是80%的开发项目的基础,并且成为主流的软件工程实践方法之一.不过,当用户需要以某种定制的次序或规则调用多个功能或服务时,Web服务标准本身就显得无能为力了,而这恰恰是Web服务业务流程执行语言W S-BPEL(简称BPEL)所关注的焦点. BPEL将SOA系统中的孤立服务按照预订的规则进行调度与协调,从而提供有价值的流程服务. BPEL的这一特点使得其在SOA架构中具有固有的优势,被众多厂商所采用.

然而,由于服务及其协同的动态性,开放多变的互联网运行环境,以及松耦合的服务开发模式所导致的开发和运行过程不确定性,使得服务的正确性、可靠性、安全性、可用性、时效性等可信性质难以得到保证.如果单纯采用传统的软件测试方法,许多这样的可信性质是无法表示和测试的.另外,传统的测试方法也难以保证生成的测试用例集是完备的.因此,自从BPEL标准发布后,研究者们在BPEL的形式化建模和分析领域做了不少研究工作.Fu等人开发了针对Web服务的验证工具WSAT(Web Service Analy sis To ol),将BPEL转化为形式模型Guarded 自动机,接着将Guar ded自动机转化为模型检测工具SPIN的输入语言,验证线性时态规范[1-2]; Kazhamiakin对通信模型、控制流、数据流和时间属性进行形式化建模和分析,并且开发了BPEL验证工具WS-VERIFY对上述属性进行验证[3];Foster 等人使用进程代数的方法把BPEL建模成FSP,使用模型检测工具LTSA对其验证[4-5];Walton把Web服务看作为多主体系统,定义了一种名为轻量级的协议语言表示Web服务内部主体的交互,并将这种语言转化为SPIN的输入语言对通信属性进行了验证[6];Nakajima使用扩展的有限状态机(EFA)对BPEL进行建模,将EFA转换为SPIN的Promela语言,自动验证了Web服务组合的属性[7];M ongiello等人将每一Web服务建模为有限状态机,然后再将所有的有限状态机转换为NuSMV输入语言,对其属性进行自动验证[8]; Ouyang等人开发了一个自动分析BPEL流程的工具,先用工具BPEL2PNML将BPEL转化为Petri 网,然后将工具BPEL2PNM L的输出通过工具Wo fBPEL对活动的不可达及数据传递进行静态分析[9-10].

从上述研究进展看,目前Web服务组合的形式化验证方法的主流思想是针对被验证属性选择自动验证工具(通常是模型检测工具),提出该工具输入语言的形式模型,然后通过BPEL到形式模型以及形式模型到输入语言的转换,实现属性的自动验证.本文也沿用这种思路,但是我们侧重于对BPEL进行多主体系统建模,原由如下:在W3C工作组起草的Web服务体系结构文件中提出,Web服务是一个抽象的概念,必须由具体的主体执行,该主体是一个具体的能够发送或者接收消息的软件或者硬件.而多主体系统(M ult-i ag ent Sy stems,M AS)是指由多个相互交互的主体组成的系统,形成多个主体合作的问题求解网络.因此很自然地,我们可以把Web服务组合抽象为多主体系统,从而应用多主体系统模型检测工具对大多数基于传统模型检测工具(如SPIN和N uSM V等)的方法不能验证的多主体认知性质进行验证.比如时态认知性质p y FK i p表示如果p成立,则最终(F时态算子)主体i会知道p成立,其中嵌入的知识子公式K i p如果在状态s 成立,则表示在主体i认为可能的(即与s不能区分

1042计算机学报2011年

的)所有状态下p均成立,因此即使主体i当前不能肯定自己处于状态s中,它也可确定(知道)p均成立.这类性质体现了主体i的认知能力,是其它非认知模型检测工具无法验证的.事实上,我们已开发出一种多主体系统符号化模型检测工具MCT K[11-13],支持时态认知逻辑性质验证,其验证效率与类似的主流工具M CMAS[14]和M CK[15]相比均有不同程度的提高.基于上述情况,本文提出并实现一种基于MCT K的Web服务组合建模和自动验证方法学,支持通信通道的建模,使得我们能够直接以BPEL 作为输入语言进行建模和验证,不仅可以验证Web 服务组合的时态逻辑规范,而且还可以验证代表Web服务的主体的时态认知性质,这是传统模型检测技术所不支持的.据我们所知,与本文最相关的工作当属Lo muscio和Q u等人在文献[16-17]的工作,他们应用M CM AS对BPEL进行了关于时态和知识属性方面的验证,但对形式模型和语言自动转化算法未给出详细说明,对Web服务间的通信也未给出具体描述.更重要的是,我们的M CT K的时态部分支持CT L*(包含CT L和LT L),而M CMAS 的时态部分仅支持CT L,因此M CTK的时态表达能力更强.

本文第2节提出BPEL流程的形式模型并给出活动执行语义;第3节提出从BPEL到迁移七元组和从迁移七元组到M CT K输入语言的自动转换算法;第4节给出一个验证示例及其实验结果;最后在第5节给出结论并展望未来工作.

2BPEL形式模型和活动执行语义

211BPEL形式模型BFM

由于单一Web服务的自治性和松耦合性,我们将每一Web服务建模为主体.这些主体广泛分布于网络中,因此组合Web服务可被视为由多个交互主体组成的多主体分布式系统(简称多主体系统),它由若干主体和一个公共环境组成,某些主体之间可以进行交互.这里,为了便于后续工作对主体交互的建模,我们引入/通道0的概念.通道用来/连接0两个主体,这些主体通过通道发送或者接收信息,交互的主体互相能观察到对方的一部分信息,同时主体还可以和环境进行交互,因此它也可以观察到环境的一部分甚至全部.主体根据自身的当前局部状态和收发的信息决定下一步动作,所有主体和环境的联合动作导致系统状态发生迁移.

我们采用扩展的有限状态机对BPEL进行形式建模,这种扩展的有限状态机首先清晰刻画了系统状态的迁移关系.其次,采用的底层验证平台是我们自行研发的多主体系统模型检测工具MCT K(详见文献[11,13]),其输入语言实际上是有限状态机的符号化描述,该输入语言同时扩展了每一主体的可观察变量集合的定义.因此,该形式模型还应对信息的可观察性进行描述.为此,我们定义BPEL语言的形式模型BFM(BPEL Finite-state M achine)如下:

BFM=(8,O,D,P0,F),

其中:8为局部状态的有限集合;O为主体可观察变量的有限集合,包括通道变量的有限集合O e、链接变量的有限集合O l和条件变量的有限集合O g;D为8@$y8是状态迁移函数,其中$=O e@O l@O g@ channel@dir.P(p,a)I8@$,有D(p,a)y q,表示当前处于状态p时,由于主体执行活动产生条件$后迁移到状态q,$由主体执行活动产生;P0为系统初始状态,P0I8;F为终结状态集合,F A8.P p I F,p为终结状态.

该模型中,8表示主体执行过程中所经历的所有状态组成的状态空间.$中channel表示与此主体/连接0的通道名,在用MCT K编程时,不仅要考虑状态之间的迁移关系,也要考虑与主体相/连接0的通道中消息与状态之间的关系以及通道中信息的变化情况.因此,需要知道与每个主体相/连接0的所有通道的名称,它即为BPEL活动的端口类型名3portT ype name4.本文中,假设所有通道名皆不相同,并且每个主体皆有两个单向通道与其相连,用于发送及接收消息,对于异步双向交互,两个3po rt-Ty pe name4即为两个通道的名称,对于同步双向交互,人工定义一个3portTy pe nam e4作为另一个通道的通道名.通道名的定义使得运用M CTK输入语言建模时更加方便,但是仅从通道名属性中并不能分辨出该通道是用来发送消息还是用来接收消息.因此,dir表示此通道相对于与其/连接0的主体是发送消息通道(简称出通道)还是接收消息通道(简称入通道).BPEL语言中的变量主要分为3种:O e为主体能观察到的通道变量的有限集合,主体能观察到的通道变量是存储此主体与其它主体或者环境之间交互信息的变量.因此,一个主体除了观察到自身内部变量外,还能观察到一部分通道变量.这些通道变量明确出现在BPEL程序的3variables4标签中,实际上它们也是主体之间的共享变量.O l为主体能观察到的内部链接变量的有限集合,这些变量可以从

1043

6期骆翔宇等:一种基于认知模型检测的W eb服务组合验证方法

3links4标签中的3link4抽出,3link4指定了并发执行活动之间的控制流,可以将这些变量看做布尔变量,当其为真时表示该控制流存在.O g为条件变量的有限集合,每个条件变量对应一个可以表达条件表达式真或假的断言,这些条件表达式可以出现在诸如3w hile4,3sw itch4,3so urce4中的3tr ansition Cond i-tion4,3tar gets4中的3j oinCondition4中,因此,每个条件变量也是布尔变量,变量值为真说明表达式也为真.

实际上通过上节对BPEL语言的分析,我们可以知道该语言主要用来对流程进行描述,它反映了主体之间的数据交互以及主体内部变量赋值等情况,但它无法具体描述主体因为信息交互而发生的状态改变,它可以说明在某种条件下控制流转移到了另一个Web服务,却无法说明信息转移后相关主体处于什么样的状态下.M CTK是基于NuSM V开发的,引入了认知逻辑验证功能的模型检测工具,但其建模过程是一个针对具体状态迁移的描述过程,我们需要描述出各主体状态之间迁移关系以及相互联系的/通道0中信息的变化情况,前者可以用来说明主体的状态空间中各状态的关系,后者使得主体之间建立起联系.因此,如果将BPEL语言直接转化为M CTK输入语言将是十分困难的,我们必须找到中间/桥梁0将BPEL语言与模型检测工具M CTK 的输入语言联系起来.

为此,我们首先对流程经历的状态进行分析:

BPEL中某些基本活动的执行可引起变量值的改变,这些变量包括用来与外界交互的变量,也包括内部通过赋值操作改变的变量,如果用这些变量的/与0操作来标示状态,那么这些变量中的任一变量值的改变将导致状态发生迁移.例如,在状态p0中v1、v2是外部变量,即用来存储与外部主体的交互信息,v3是内部变量(例如该变量利用assign赋值活动得到值),并且变量v1=3,v2=4,v3=5,那么我们可以用(v1=3)C(v2=4)C(v3=5)标示状态p0.若主体执行某活动从外界主体得到新的信息存储于变量v2,使得v2的值发生变化变为5,之后执行活动使得内部变量v3的值变为6,则系统由状态p0迁移到状态p1:(v1=3)C(v2=5)C(v3=6).但对于em pty 活动,由于活动执行后内部外部变量的值均不发生改变,但主体确实执行了此活动,因此可以加入程序计数器PC来标示这种活动的执行.例如,系统在执行了活动empty后由状态p0:(v1=3)C(v2=4)C (v3=5)C p c0迁移到状态p1:(v1=3)C(v2=4)C (v3=5)C p c1.由此可见,主体在执行过程中的所有状态均可由主体中所有变量与PC的合取来标示,因此变量或者PC任何一方的改变都将引起状态的迁移,而在BPEL流程中基本活动的执行会修改PC 或者变量的值,结构活动与基本活动不同,前者主要用来说明在其内部的基本活动是按照何种顺序执行,或者顺序执行、或者并发执行、或者选择执行、或者循环执行等等.因此,欲实现BPEL流程的自动化验证就需要在结构活动所提供的框架下,研究其内部基本活动的执行对系统产生的影响,主要包括对主体所处状态的影响,并自动将这种影响刻画出来.

直观上看,对主体所处状态的影响主要指主体相关变量值的改变,由于我们用变量的合取标示状态,活动的执行将导致变量值发生改变,状态自然发生迁移.考虑到模型的简化,我们省去了状态记数器PC,只研究变量值的改变对状态迁移产生的影响.所以我们要找的/桥梁0必须能够直观反映出由于变量值改变引起的这种状态的迁移关系,这是其一;除此以外,该/桥梁0必须便于用M CTK对其进行描述从而进行形式化建模.因此,结合BPEL语言以及M CTK输入语言的特点,我们还需考虑到:交互信息的/流动0方向,即信息是进入本主体还是离开本主体,这是其二;交互信息进入/离开主体时经过的端口,这是其三.

由此,我们所找的/中间桥梁0应考虑到上述3个条件:第1个条件用来对BPEL流程的执行进行描述,便于M CT K描述状态迁移关系,后两个条件是为了方便MCT K建模语言对通道机制进行描述.

由以上分析我们知道了BPEL活动的执行产生相对应的状态迁移过程,为了刻画这种状态的变化信息,本文提出迁移七元组概念.它也是我们要找的/中间桥梁0.

一个迁移七元组(简称七元组)应具备如下形式:5(8,$,8).它将主体初状态、迁移条件、末状态组合在一起,迁移条件是主体执行某活动导致状态变迁过程中的相关信息值.七元组展开后语法格式为:

5(cur(state),O e,O l,O g,channel,dir,nex t(state)).其中:cur(state)为主体执行活动前的当前状态;O e 为主体执行活动后的通道变量值;O l为主体执行活动后链接变量的值;O g为主体执行活动后条件变量的值;channel为与主体连接的通道名;dir表示对本主体是出通道还是入通道;nex t(state)为主体执

1044计算机学报2011年

行活动完毕所处状态.

该七元组包含了主体活动执行完毕后状态的变化,由七元组看出状态的变化在这里主要指:

(1)状态名从cur(state)变为nex t(state),表明状态已发生迁移;

(2)主体活动执行完毕后O e、O l、O g、channel、dir的变化,这些信息不仅真实反映了BPEL活动执行导致的变量值的改变情况,同时也具备了MCT K建模所需的必要信息.

需要说明的是,完全运用变量与PC的合取标示状态,会对最后验证规范的书写带来很大困难,原因有两点:

(1)大量变量的书写很麻烦,尤其当系统的状态空间很大时,为表示状态又需要书写多个变量的合取,很容易出错,而实际中的软件系统大多具有超大规模状态空间,因此这种状态表示法并不实用.

(2)由于规范需要人为书写,因此,一般状态名都具有明确的意义,这符合人类语言习惯.同时,也为了简化七元组以及M CTK代码中状态的表示,降低程序出错的可能性.规范中状态的命名一般都带有特殊含义使得表达的意义更明确,使人一目了然,例如欲验证:无论何时只要A事件发生,则未来B 事件必将发生,其规范可写为A G(A_happen y AF(B_happen)),A_happen、B_happen均为状态名,其意义从字面上看很清晰,并且书写方便也便于MCT K代码的生成.再例如主体发送信息Msg 以前其状态为M sg,发送该信息后状态变为send_M sg,表示主体到达了/已经发送了M sg信息的状态0等等.但是为了扩大可验证规范的种类,同时又要便于迁移七元组的正确生成,我们将部分采取变量的合取标示状态的方法.具体状态表示方法将在311节给出.

由此,本文利用迁移七元组将BPEL语言刻画的组合Web服务与MCT K输入语言之间建立起联系.实际上,迁移七元组从本质上说就是对状态转换图中的每一对有迁移关系的/状态对0的一种文字性刻画,因为传统工作对BPEL流程的验证皆需要构造状态转换图,而状态转换图在计算机中是不存在的,这需要大量的人工操作,之后再用形式化验证工具的输入语言对该状态转换图进行刻画,进而验证.若要实现流程的自动验证,就需要自动生成能够反映状态转换关系的、文字性的、对流程进行刻画的规范.并且构造该规范时还要考虑到后续工作,也就是是否便于用MCT K利用该规范进行形式化建模.

通过对BPEL活动执行语义进行分析,我们发现活动的执行过程就是对活动中所涉及的相关变量的一次赋值操作,BPEL活动的属性显示了相关变量在活动执行完毕后得到的值以及其它一些必要的操作.因此,在构造七元组时我们需要将BPEL语言活动中的对我们后续工作有价值的属性值抽取出来,以构造七元组.于是,我们给出BPEL活动语义并结合该语义说明活动执行后相关七元组的产生. 212BPEL活动执行语义以及相关七元组的产生本节给出BPEL活动的形式化语义,为了方便后续说明,我们首先定义几个函数:

cur(state)表示活动的初始状态,也就是活动刚开始执行时主体所处状态.

nex t(state)表示活动执行后主体所处状态.

v alue(var iable)表示通道中的信息值.

c(source(state),d est(state))表示与主体连接的通道名,通道中信息的传输改变主体状态.

dir(channel)表示通道中信息传送方向,即信息离开主体还是到达主体.

基本活动.

(1)receive

功能:该活动允许商业流程等待一条匹配消息的到来,当此消息到来时该活动结束.

格式:3receive p artnerL ink=L p ortTy p e= P T op er ation=Op v ar iable=V4

迁移语义:

D Receive={T|P i,P i+1I8C V I O e C cur(state)=

P i C nex t(state)=P i+1C c(P i,P i+1)=

P T C value(PT)=V C d ir(PT)=I N}说明:

1P i,P i+1I8说明P i、P i+1为状态空间8中的状态,即为主体流程执行过程中系统经历的状态;

oV I O e说明V是通道变量,因此,v ar iable属性所指变量值为本主体与外界主体的交互信息,其值存储于变量V中;

?cur(state)=P i C nex t(state)=P i+1指出这两个状态之间存在直接的迁移关系是由状态P i迁移到状态P i+1;

?c(P i,P i+1)=PT指出端口类型p or tTy p e 属性指定了与本主体连接的用来发送或者接收消息的通道名;

?value(PT)=V说明通道中的信息是变量V 中存储的信息;

?dir(P T)=IN说明该活动接收外界到来的

1045

6期骆翔宇等:一种基于认知模型检测的W eb服务组合验证方法

信息,信息的流向是进入主体.同时也说明了PT 通道是入通道.

所有条件的/与0操作构成了该活动形式化语义,我们将语义中各个元素抽取出,按照迁移七元组定义将它们按顺序载入,得到产生的七元组如下(迁移图如图1所示):

T =(P i ,V ,E ,E ,PT ,IN ,P i+1

图1 3r eceive 4活动状态迁移示意图

(2)reply

功能:允许企业流程发送一条消息来响应诸如3receive 4、3o nM essag e 4和3onEvent 4这样的/接收0信息的活动.

格式:3reply p ar tnerlink =L p or tTy p e =

op er ation =Op

var iable =V 4.

迁移语义:D reply ={T |P i ,P i +1I 8C V I O e C cur (state)=P i C

nex t(state)=P i +1C c(P i ,P i +1)=

P T C value(P T )=V C dir (PT )=OU T }.说明:

1P i ,P i +1I 8说明P i 、P i +1为状态空间8中的状态,即为主体流程执行过程中系统经历的状态;

oV I O e 说明V 是通道变量,因此,variable 属性所指变量值为本主体与外界主体的交互信息,其值存储于变量V 中;

?cur (state)=P i C nex t(state)=P i +1指出这两个状态之间存在直接的迁移关系是由状态P i 迁移到状态P i +1;

?c (P i ,P i +1)=P T 指出端口类型p or tT y p e 属性指定了与本主体连接的用来发送或者接收消息的通道名;

?v alue(PT )=V 说明通道中的信息是变量V 中存储的信息;

?d ir (PT )=OU T 说明该活动响应外界到来的信息,主体执行活动完毕将信息返回给调用方,说明了P T 通道是出通道.

所有条件的/与0操作构成了该活动形式化语义,我们将语义中各个元素抽取出,按照迁移七元组定义将它们按顺序载入,得到产生的七元组如下(迁移图如图2所示):

T =(P i ,V ,E ,E ,PT ,OU T ,P i+1).

图2 3r eply 4活动状态迁移示意图

(3)同步invo ke

功能:允许流程在由合作伙伴提供的端口上调用该合作伙伴提供的服务,同步invoke 为/请求-响应0式调用.

格式:3invoke p ar tner L ink =L p ortTy p e =

P T

op er ation =Op

inp ut Variable =I V out -

p utVar iable =OV 4.

迁移语义:

D syn -invoke ={T 1|P i ,P i +1I 8C I V I O e C cur (state)=

P i C nex t(state)=P i +1C c(P i ,P i +1)=P T C value(PT )=I V C d ir (PT )=OU T }C

{T 2|P i +1,P i +2I 8C OV I O e C cur (state)=P i +1C nex t(state)=P i +2C c(P i +1,P i +2)=P T _back C value(P T _back)=

OV C d ir (PT )=IN }.

说明:

1执行该活动状态迁移两次,语义中是两次迁移T 1,T 2的/与0操作.P i ,P i +1,P i +2I 8说明P i 、P i +1、P i +2均为主体流程执行过程中系统经历的状态.由于是同步inv oke ,因此,主体调用其它Web 服务后等待响应信息的到来,其发送消息时通道变量的值发生变化,状态迁移一次,接收消息通道变量值再次发生变化,在上步基础上状态再迁移一次;

oI V,OV I O e 说明I V 、OV 都是通道变量,因此,inp utVar iable 、outp utVariable 属性所指变量值为本主体与外界主体的交互信息,其值分别存储于变量I V 或者OV 中.由于是同步invo ke ,主体调用其它Web 服务后等待响应信息的到来,信息的交互是双向的,因此该活动具有两个用于存储交互信息的变量;

?cur(state)=P i C nex t(state)=P i +1指出这两个状态之间存在直接的迁移关系是由状态P i 迁移到状态P i +1;cur (state)=P i +1C nex t (state)=P i +2说明主体在P i +1状态中等待,直到接收到外界的响应消息后迁移到状态P i +2;

?T 1中c(P i ,P i +1)=P T 与T 2中c(P i +1,P i +2)=P T _back 分别指出相应端口类型p or tTy p e 属性指定的,与本主体连接的用来发送或者接收消息的通道名.需要说明的是通道名PT 是BPEL 流

1046计算机学报2011年

程已经给出的,但为了实现通道机制,便于M CTK 代码的自动生成,我们前面约定任一主体皆有两个单向通道与其相连,作为两个相反方向的信息传输通道.因此,凡具有双向信息交互的活动,若其通道名只有一个,则对另一个通道采用自命名方式.在这里,本文将另一通道命名为PT _back;

?F value(P T)=I V 和value(PT _back)=OV 说明通道中的信息是变量I V 和OV 中存储的信息;

?d ir (PT )=OU T 和dir (PT )=IN 说明T 1中通道是出通道,主体首先调用外界服务;之后说明T 2中通道是入通道,响应信息通过该通道进入主体.

单步迁移中所有条件的/与0操作构成了该步迁移的形式化语义.因为只有等到响应消息的到来,同步invo ke 活动才算结束,因此两步迁移采用/与0操作连接起来.我们将语义中各个元素抽出,按照迁移七元组定义将它们按顺序载入,得到产生的七元组如下(迁移图如图3所示)

图3 同步3invo ke 4活动状态迁移示意图

(4)异步invoke

功能:允许流程在由合作伙伴提供的端口上调用该合作伙伴提供的服务,异步invoke 为单向请求式调用.

格式:3invoke p ar tnerL ink =L p or tT y p e =PT op eration =Op inp utVar iable =I V 4.迁移语义:D asyn -invoke ={T |P i ,P i +1I 8C I V I O e C cur (state)=

P i C nex t(state)=P i +1C c(P i ,P i +k )=P T C v alue (P T )=I V C dir (PT )=OU T }.

说明:

1P i ,P i +1I 8说明P i ,P i +1为状态空间8中的状态,即为主体流程执行过程中系统经历的状态;

oI V I O e 说明I V 是通道变量,因此,v ar iable 属性所指变量值为本主体与外界主体的交互信息,其值存储于变量I V 中;

?cur (state)=P i C nex t(state)=P i +1指出这两个状态之间存在直接的迁移关系是由状态P i 迁

移到状态P i +1;

?c(P i ,P i +1)=PT 指出端口类型p or tTy p e 属性指定了与本主体连接的用来发送或者接收消息的通道名;

?value(PT )=I V 说明通道中的信息是变量I V 中存储的信息;

?dir(PT )=OUT 说明该活动发送调用信息到其它合作伙伴,信息的流向是进入被调主体,因此P T 通道是出通道.

所有条件的/与0操作构成了该活动形式化语义,我们将语义中各个元素抽取出,按照迁移七元组定义将它们按顺序载入,得到产生的七元组如下(其迁移图与reply 活动类似,如图2所示):

T =(P i ,I V ,E ,E ,PT ,OU T ,P i+1).

结构活动.(5)switch

功能:用于从一组选择中挑出一个分支,执行该分支包含的活动.

格式:3sw itch 4

3case cond ition =C 14,3/case 43case cond ition =C 24,3/case 4,

3otherw ise 4,3/otherw ise 4

3/sw itch 4

迁移语义(假设该活动具有N 分支):

D switch =á1F k F n {T k |P i ,P i +k I 8C C k I O g C C k =

true C cur (state)=P i C nex t(state)=P i +k }.说明:

1á1F k F n 表示互斥,即在待选的N 分支中,只有一个分支(k 分支,1F k F n)被选中触发;

oP i ,P i +k I 8说明P i 、P i +k 为状态空间8中的状态,即为主体流程执行过程中系统经历的状态;?C k I O g C C k =tr ue 说明C k 是条件变量,也可以说是代表condition 后条件表达式的断言变量,其值或为真或为假.C k =true 表明当其为真时,该条件表达式为真,说明该分支被选中,流程执行该C k 所在3case 4内的活动.当一个分支被选中后,在本次实例流程中其余分支将不再被触发;

?cur(state)=P i C nex t(state)=P i +k 指出这两个状态之间存在直接的迁移关系是由状态P i 迁移到状态P i +k .需要说明的是,对于N 分支中的任一分支,其状态迁移的初始状态皆为P i ,选择不同分支则流程由P i 状态迁移到不同状态P i +k ,具体迁移到哪个状态由条件变量的真值决定.

1047

6期骆翔宇等:一种基于认知模型检测的W eb 服务组合验证方法

所有条件的/与0操作构成了某一被触发迁移的形式化语义,我们将语义中的各个元素抽取出,按照迁移七元组定义将它们按顺序载入,得到产生的七元组如下(迁移图如图4所示

图4 3switch 4活动状态迁移示意图

(6)pick

功能:用于等待一系列可能消息中的一个到达本Web 服务并执行相应活动或者等到超时事件发生.

格式:

3pick 4

3onmessag e var iable =m 1porttype=

PT 14,3/onmessage 43onmessag e var iable =m 2porttype=

PT 24,3/onmessage 4,3/pick 4迁移语义:

D pick =á1F k F n {T k |P i ,P i +k I 8C m i I O e C

cur(state)=P i C nex t(state)=P i +k C

c(P i ,P i +k )=PT C dir (P T)=IN }.

说明:

1á1F k F n 表示互斥,3pick 4等待互斥信息的到来,当到来的消息与某个3onmessag e 4中的v ar iable 属性相匹配时,则相关活动被执行;

oP i ,P i +k I 8说明P i 、P i +k 均为状态空间8中的状态,即为主体流程执行过程中系统经历的状态;

?cur (state)=P i C nex t(state)=P i +k 指出这两个状态之间存在直接的迁移关系是由状态P i 迁移到状态P i +k .需要说明的是,对于N 分支中的任一分支,其状态迁移的初始状态皆为P i ,不同分支被触发则流程由P i 状态迁移到不同状态;

?m i I O e 说明m i 是通道变量,因此,v ar iable 属性所指变量值为到达本主体的外界信息,也就是主体等待发生的事件,其值存储于变量m i 中;

?c (P i ,P i +1)=P T 指出端口类型p or tT y p e

属性指定了与本主体连接的用来发送或者接收消息的通道名;

?说明主体等待事件的发生,信息的流向是进入该主体,因此PT 通道是入通道.

所有条件的/与0操作构成了某一被触发迁移的形式化语义,我们将语义中各个元素抽取出,按照迁移七元组定义将它们按顺序载入,得到产生的七元组如下(迁移图如图5所示):

图5 3pick 4活动状态迁移示意图

(7)flow -source -activity

功能:用以实现程序的并发同步执行.格式:3flow 4

(迁移条件tr ansitionCondition 简写为tC,假设有两个目标链接活动,其余类推)

3--activity --4

3so urce linkN ame =L 1tC =C 143so urce linkN ame =L 2tC =C 243/--activ ity --4迁移语义:

D flow -s -a ={T 1|P i ,P i +1I 8C ,C cur (state)=P i C

nex t(state)=P i +1}C {T 2|P i +1,P i +2I 8C L 1,L 2I O l C C 1,C 2I O g C (C 1D C 2)I O g C

cur(state)=P i +1C nex t(state)=P i +2}.

说明:

1该活动迁移两次,T 1迁移触发后再触发T 2

迁移,语义中是两次迁移T 1,T 2的/与0操作,由于source 容器存在,说明此活动为多个活动的源链接.因此活动先执行,引起状态迁移T 1,T 1执行完毕将迁移条件tC 分别赋值为C 1和C 2,由于C 1,C 2都是条件变量,因此,由于tC 的赋值导致变量值改变状态再次发生迁移,于是T 2被触发;

oP i ,P i +1,P i +2I 8说明P i 、P i +1、P i +2均为主体流程执行过程中系统经历的状态;

?T 1中cur (state)=P i C nex t(state)=P i +1指出由于活动执行导致状态迁移,由状态P i 迁移到状

1048计算机学报2011年

态P i +1;

?T 2中L 1,L 2I O l C C 1,C 2I O g C C 1D C 2I O g 指出L 1,L 2为链接变量,当链接存在时,这些变量为真;C 1,C 2为条件变量,若C 1D C 2为真,则该活动作为其它活动的源链接是有效的.显然,C 1D C 2I O g ;

?T 2中cur(state)=P i +1C nex t(state)=P i +2

指出由于T 1执行完毕给tC 赋值导致条件变量O g 改变,状态再次发生迁移,于是T 2被触发,系统状态由T 1执行末状态P i +1迁移到状态P i +2.

所有条件的/与0操作构成了单步迁移的形式化语义,由于两步迁移具有先后顺序,我们用/与0操作将其联系起来.于是,将语义中各个元素抽取出,按照迁移七元组定义将它们按顺序载入,得到产生的七元组如下(迁移图如图6所示):

T 1=(P i ,,,P i+1),

T 2=(P i+1,E ,E ,C 1D C 2,E ,E ,P i+2

图6 flow -so urce -activ ity 状态迁移示意图

(8)flow -tar get -activity

格式:3flow 4

(迁移条件j oinCondition,简写为j C)3--activity --4

3target linkN ame =L 1

j C =Q 143target linkN ame =L 2j C =Q 24

,3/--activity --4迁移语义:

flow--t a ={T 1|P i ,P i +1I 8C L 1,L 2I O l C Q 1,Q 2I O g C ((L 1C Q 1)D (L 2C Q 2))I O g C

cur (state)=P i C nex t(state)=P i +1}C {T 2|P i +1,P i +2I 8C ,C cur(state)=

P i +1C nex t(state)=P i +2}.

说明:

1该活动迁移两次,T 1迁移触发后再触发T 2

迁移,语义中是两次迁移T 1,T 2的/与0操作,由于targ et 容器存在,说明此活动为多个活动的目标链接.因此先判断该目标活动被触发需满足条件的真值,即jC 被赋值,迁移T 1被触发;若条件为真则活

动被执行,状态再次发生迁移,T 2被触发;

oP i ,P i +1,P i +2I 8说明P i 、P i +1、P i +2均为主体流程执行过程中系统经历的状态;

?T 2中L 1,L 2I O l C Q 1,Q 2I O g C ((L 1C Q 1)D (L 2C Q 2))I O g 指出L 1,L 2为链接变量,L 1,L 2链

接状态的确定是链接发生的前提条件,当这两个链接有效时,这些变量为真.于是,在链接变量有效的前提下,判断Q 1,Q 2的真值,若为真,则控制流转移到本活动中来,因此,L 1与Q 1必须同时为真,链接才能转移,对其它情况类似.显然,((L 1C Q 1)D (L 2C Q 2))I O g ;

?T 1中cur (state)=P i C nex t(state)=P i +1指出由于给jC 触发条件赋值并判断,条件变量O g 改变,系统状态由P i 迁移到状态P i +1;

?T 2中cur (state)=P i +1C nex t(state)=P i +2

指出由于目标活动执行条件满足,于是活动执行导致状态迁移,由状态P i +1迁移到状态P i +2.

所有条件的/与0操作构成了单步迁移的形式化语义,由于两步迁移具有先后顺序,我们用/与0操作将其联系起来.于是,将语义中各个元素抽取出,按照迁移七元组定义将它们按顺序载入,得到产生的七元组如下(迁移图如图7所示):

T 1=(P i ,E ,E ,(L 1C Q 1)D (L 2C Q 2),E ,E ,P i+1),

T 2=(P i+1,,,P i+2).

图7 flo w -tar get 状态迁移示意图

WS -BPEL 210支持的活动种类繁多,因此实际的建模工作复杂且繁琐,以上只给出了部分重要

活动语义及相关说明,在后续研究中我们将不断扩展对其它活动的建模方法,因此对于这些活动,本文简化处理如下:3assig n 4活动代表变量的赋值操作,3ex it 4活动用于立即终止流程,3w ait 4活动用于实现流程等待某个时间点的到来,这些活动的语义简单,这里不再详述;3thr ow 4、3r ethrow 4、3com pensate 4是作用域3sco pe 4的实现机制,分别用来抛出错误和补偿处理,它们用来处理流程中的非设计性失误这类错误,我们用3empty 4活动代替它们,从而在建模过程中忽略它们;3if 4活动用来实现双分支选择,可用3sw itch 4活动替换3if 4活动;对于3validate 4和3ex tensionActivity 4活动,前者用于验证存储在变量

1049

6期骆翔宇等:一种基于认知模型检测的W eb 服务组合验证方法

中的XML信息的有效性,后者用于对BPEL语言进行扩展,本文暂不考虑这两个活动.另外,3r epea-tU ntil4、3fo rEach4用于处理循环,可用3w hile4活动代替.3w hile4活动初步的转化过程并不复杂,但是我们在转化算法实现和测试时发现循环活动往往会生成大量的系统状态,使得转化出的OBDD形式模型过大,导致在可接受的时限内无法得到验证结果,因此严谨起见,本文暂不讨论3w hile4等循环活动,我们将在后续工作中深入研究这些活动的优化转化算法.

模型检测的状态爆炸问题始终是阻碍模型检测技术投入实用的一大瓶颈,M CT K作为认知模型检测工具也不例外.虽然我们在M CTK中采用OBDD 实现符号化建模和验证算法,已大大减少形式模型和验证所需的内存空间,但是OBDD的规模可能会因为OBDD变量的增多而迅速扩大,因此在M CTK 输入语言中定义的变量要尽量减少.而且BPEL语言本身的复杂性可能令MCT K生成复杂的状态迁移关系,也可导致其OBDD表示的规模迅速增大.因此,本文在转换过程中忽略掉上述活动中某些与验证无关的属性,从而简化转化过程,减小最终生成的M CTK形式模型的规模.此外,我们还将采用3.1节介绍的状态命名规则,避免多变量标示带来的书写以及理解上的麻烦,同时将活动与七元组建立映射关系,使得活动的执行转化为与其对应的七元组的产生,简化了活动执行的复杂性,使得后续算法更好把握流程的执行带来的状态变化的影响.

我们看到BPEL结构化活动可以用来组织基本活动,使得基本活动在结构化活动的/安排0下按照某种特定顺序执行,从而使得各Web服务协作完成即定任务.前面我们已经分析了基本活动向迁移七元组的转换过程,为了实现流程自动化验证我们必须找到一种算法,使得各基本活动能够按照其所在结构活动的结构框架下按正确顺序执行产生相应迁移七元组.因此,这样的算法实际上是将结构活动的性质用算法的形式表示出来,期间遇到基本活动就按照上节介绍的映射关系将其映射为相应七元组,实现BPEL流程向七元组集合的转化.基于这一思想,我们提出将BPEL流程转化为迁移七元组集合的算法.

3BPEL语言的自动化模型检测方法由前述可以看出,由于BPEL语言自身的复杂性,如何建立该语言到某种规范的统一映射以及如何自动利用模型检测工具对此规范进行描述是实现流程自动化验证需克服的两个技术难点.由于BPEL语言与模型检测工具MCT K输入语言之间无直接联系,传统工作主要是将BPEL语言转化为状态转换图,之后对状态转换图进行描述.根据上节提出的迁移七元组的语法及语义,BPEL代码中每一个活动的执行都将产生一个相应的七元组,此七元组包括了主体交互的所有信息.因此,如何产生正确的迁移七元组以及如何方便地利用一组迁移七元组写出M CTK代码,进而验证组合服务,就是下文的主要内容.

311将BPEL模型转化为迁移七元组

(1)状态命名规则

迁移七元组明确指出了状态之间的迁移关系,以及状态迁移后各相关变量值的变化.因此,状态的命名对于迁移七元组的自动生成十分重要.在前面章节我们已经说明,完全用变量的合取标示状态对于实现自动化检测并不适用,但是为了实现对更多的涉及数据流的规范进行验证,本文部分采取用变量的合取标示状态的方法,但与传统方法又有很大不同,具体状态命名法则如下:

1对于由通道变量O e值的改变引起的状态迁移,状态命名采用/send_消息0表示主体/发送了某信息0状态,用/g et_消息0表示主体/接收了某信息0状态,例如主体的初始状态为sleep,当其发送了信息M sg以后,状态从sleep迁移到了send_M sg,表示状态从/睡眠0迁移到/发送了M sg0状态.

o对于由链接变量O l、条件变量O g值的改变引起的状态迁移,状态命名采用/源状态C O l0或者/源状态C O g0原则,/C0号后面的变量是在源状态中,其值在活动发生后有可能发生变化的那些O l或者O g类型的变量.例如:主体在get_r equest状态下,若活动执行将对该状态下的条件变量tC进行赋值操作,那么执行活动后系统状态就由get_ r equest迁移到状态get_r equest C tC.若主体在get_ r equest状态下,活动执行将对其中条件变量tC1或者tC2进行赋值操作,那么活动执行后系统状态就由get_request状态迁移到get_r equest C(tC1D tC2)状态.

(2)转换算法

3sequence4和3flow4是BPEL语言中最基本的两种控制结构,前者用来处理顺序流程,后者用来处理并发流程.对于顺序流程,活动按照出现的先后顺

1050计算机学报2011年

序执行,3sequence4内可以嵌套基本活动与结构活动3sw itch4或者3pick4等,此时,如果将该流程用状态转换图表示出来,则该图是一个多分支的状态转换图,可以用M CTK这样验证分支时态逻辑的模型检测工具对其进行刻画,进而验证.对于嵌套在3sequence4中的基本活动,我们可以按照顺序的方式产生与各个活动对应的迁移七元组,然后用MCT K对产生的迁移七元组集合进行描述.

下面给出3sequence4结构框架下的业务流程转化为迁移七元组的算法,由于在设计七元组时也同时考虑到了M CTK输入语言的特点,因此通过该算法生成的七元组可以用来进一步自动生成M CTK 的输入代码,使得流程验证过程的自动化程度大大提高.

算法B2T.3sequence4y迁移七元组.

B2T(A CT(S),ST AT(S))

输入:描述W eb服务的BP EL源码

输出:迁移七元组集合

1.Init A ct.T op=3sequence4;Init Stat.T op=sleep;

cur(state)=sleep;

2.scan from curr ent activity3,2,4to the last activity;

3.for each element3,2,4do

4.{/*将活动及活动执行后的状态入栈*/

5.A ct.T op++&A ct.P ush3,2,4;

6.W3,2,4;

7.Stat.T op++&Stat.Push(nex t(state));

8.cur(state)=nex t(state);

9.If(3,/2,4S3/case4OR3otherw ise4)

10.{/*活动栈及状态栈同步弹栈直到switch*/

11.do

12.{

13.A ct.Pop&A ct.T op--;

14.S tat.Pop&Stat.T o p--;

15.}w hile(A ct.T op!S3case4O R3sw itch4);

16.cur(s tate)=S tat.T op;

17.}

18.If(3,/2,4S3/onmessag e4)

19.{/*活动栈及状态栈同步弹栈直到pick*/

20.do

21.{

22.A ct.Pop&A ct.T op--;

23.S tat.Pop&Stat.T o p--;

24.}w hile(A ct.T op!S3pick4);

25.cur(s tate)=S tat.T op;

26.}

27.}

算法说明:/S0符号代表纯文本的匹配,当/S0号左右的文本内容完全一样时,该关系成立.算法设置两个栈用以实现对结构活动的结构框架的描述,一个状态栈Stat用来存放主体在执行过程中所经历的所有状态;一个活动栈Act用来存放流程执行过程中所经历的所有活动.我们用这两个栈来处理流程中活动与状态之间的关系.3,2,4表示任一活动的开始标记,3,/2,4表示活动的结束标记,例如流程遇见3receive4活动则表示该活动准备开始执行,遇见3/r eceive4则表示该活动执行完毕.需要说明的是3,/2,4不进栈,因此扫描时跳过3,/2,4.我们用W表示/执行活动0,所谓执行就是流程执行该活动指定的操作,因此在本算法中W3,2,4就是产生与活动相对应的迁移七元组.cur(state)用来存放下一个即将执行的活动的初始状态,显然初始状态的确定非常重要,对于顺序执行的活动A、B,B 活动的初始状态即为A活动的终结状态.而对于带有分支的活动,例如3sw itch4活动,假设流程刚进入3sw itch4活动时的状态为state0,则该活动中任一分支的初始状态皆为state c0,如图4所示:设P i= state0,P i+1=state1,P i+2=state2,,则流程执行完第1个3case4包含的活动后状态由state0迁移到state1,执行完第2个3case4包含的活动后状态由state0迁移到state2,,.起初,活动栈被初始化为3sequence4,状态栈与当前状态cur(state)都初始化为sleep.算法步2指明从当前活动开始向后执行,由于是顺序结构,对于已经执行完毕的活动,流程不可能返回执行,只能继续向下执行直到3sequence4结构中的最后一个活动为止;算法步3开始循环,从3r eceive4活动开始(3receive4用来接收外界信息使流程开始执行,一般它都是流程的第1个活动)向下扫描;算法步5~8将扫描到的基本活动进栈,注意这里说的是活动的名称;步7将执行活动完毕产生的末状态nex t(state)进状态栈,之所以保存每个活动执行完毕的末状态原因有两点:其一,该状态是下一个活动的初始状态;其二,若下一活动为带有分支的结构活动,则这些分支的初始状态皆为此进栈状态.需要注意的是,本算法自始至终要保证活动栈与状态栈的同步进栈,也就是这两个栈的栈顶指针要保持同步增加或者同步减少.这样做是为了保证两个栈的栈顶元素具有高度相关性,即状态栈的栈顶保存的是活动栈栈顶活动执行完毕的末状态;算法步8将进栈状态赋值给cur(state),说明下一活动的初始状态,该算法采用双栈配合使用方法来描述结构活动的相关结构性质,但具体的活动执行时的状态衔接点还需要额外变量保存,这将在实例中看到;步9~17说明若扫描到3otherw ise4或者3case4,则

1051

6期骆翔宇等:一种基于认知模型检测的W eb服务组合验证方法

表明3sw itch 4活动已经进栈,此时需要找到流程刚进入3sw itch 4时的状态,因为无论是3otherw ise 4还是3case 4代表的都是3sw itch 4中的分支,这些分支拥有同一个迁移原状态.因此,将状态栈与活动栈同步退栈,当活动栈栈顶指针退栈到A ct .T op S 3sw itch 4时,说明状态栈栈顶指针指向的即为流程刚进入3sw itch 4时的状态.之后将S tat .Top 所指状态赋给cur (state),用做分支活动的原状态;步18~25用来处理3pick 4活动,其原理与3sw itch 4相同,这里不再赘述.由于算法需要从上到下扫描所有活动,当活动数为n 时,算法的时间复杂度为O(n).

3flow 4活动用以处理并发程序的执行,该活动根据迁移条件的不同,业务流程将选择不同的分支路径执行,被执行的活动又可以按照迁移条件选择下一个需要执行的活动,.如图8所示,第一条链路中链接变量L 1的源迁移为活动A ct 1,目标迁移为活动A ct 2,L 2的源迁移为Act 2,目标迁移为A ct 3,,,L k 的源迁移为A ct k ,目标迁移为A ct k +1.而在3flow 4结构中,一个活动往往是多个目标活动的源迁移,例如链接变量L c 1的源迁移依旧为A ct 1,但目标迁移活动变为Act c 2,链接变量L c 2的源迁移活动为A ct c 2,目标活动却为A ct 3,

图8 3flow 4抽象流程示意图

第212节给出了flow -sour ce -activity 和flow -targ et -activity 迁移语义,在flow -source -activity 中,activity 的执行导致T 1迁移的触发,执行完毕后给迁移条件tr ansitionCondition 赋值,条件变量O g 改变,T 2迁移触发,系统状态再次发生变化.因此T 2迁移的末状态即表示transitionCondition 被赋值后的状态;同理,在flow -target -activity 中,首先给j oinCondition 赋值,O g 改变,导致T c 1触发,状态迁移,之后执行相应活动activity ,T c 2触发,状态再次发生改变.

B2T 算法给出了3sequence 4结构框架下BPEL 流程向迁移七元组的转换方法,下面我们基于212节给出的活动语义,提出将3flow 4转化为迁移七元组的转换算法F2T .为此首先提出活动图的概念,所谓活动图即是由活动作为顶点,迁移作为边的有向图,对于迁移L,若其迁移源活动为A ,迁移目标活动为B,则用A y B 代表流程执行完活动A 转到活动B 执行.

我们将研究对象简记为A ct 3flow 4,A ct 3flow 4本身是简单的3flow 4活动,所谓简单是指其内部不再嵌套3flow 4.我们用T 1、T 2、T 3、,表示顺序执行的迁移序列,其中T 2的初状态为T 1的末状态,T 3的初状态为T 2的末状态,.

算法F2T . 3flo w 4y 迁移七元组.

输入:简单3flow 4结构下的组合业务流程

输出:该组合流程的迁移七元组集合/*phase1:构建活动图*/

1.查找BPEL 源码中3link name 4属性值,找到所有迁移,为每个迁移设置集合:L ink i {so ur ceA ct,des tA ct}

2.for each L ink

3.{

找到Link i 链接的源活动和目标活动,放入L ink i {sour ceA ct,d estA ct},这可通过查找L ink i 所在的3sour ces 4或者3tar gets 4所属的活动实现;5.

建立单步链接图:L ink i .sourceA ct L ink i

L in -

k i .

destA ct;

6.If (Link i .des tA ct ==Link j .sour ceA ct)

建立单步链接图:L ink i .des tA ct L ink j

L ink j .destA ct;

8.}

/*phase2:创建状态转换图*/9.流程进入3flow 4,保存此时状态

10.查找无入链接的活动,从这些活动开始:11.{

12.对于活动图中具有Link i .sourceA ct L ink i

L ink i .destA ct 形式的链接:13.{

14.

根据flow -so ur ce -activ ity 语义,执行Link i 的

1052计算机学报2011年

源活动activity:产生相应迁移;

15.根据flow-t arg et-act ivity语义,以步14末状态

作为该步初始状态,执行Link i的目标活动

activ ity:产生相应迁移;

16.If(L ink i.destA ct==L ink j.so ur ceA ct)

17.{

18.根据flo w-sour ce-activity语义,执行L ink j

的源活动:以步15末状态作为该步初状

态,执行链接条件tr ansitionCondition的

赋值操作,产生相应迁移;

19.根据flow-targ et-activ ity语义,以步18末

状态作为该步初状态,执行L ink j的目标

活动:产生相应迁移;

20.}

21.}

22.}直到没有新的迁移生成;

算法phase1阶段说明了活动图的产生过程, phase2根据212节给出的活动语义,执行活动图的每个顶点活动,并转化为相应迁移七元组.步10~ 15说明若该活动是某迁移源活动,则先执行活动,再给条件变量tr ansitionCondition赋值;若该活动是某迁移目标活动,则先给条件变量j oinCondition 赋值,再执行活动;步16~21说明若此活动即是某迁移的目标活动,又是另一迁移的源活动,则当其作为目标活动执行完毕后,给下一迁移的链接条件tr ansitionCond ition赋值,之后执行下一迁移的目标活动.

算法的研究对象是针对简单3flow4结构下的组合业务流程,很多时候活动之间是相互嵌套的.例如:3flo w4活动内可以嵌套3sequence4,3sequence4也可以嵌套3flow4,同时3flow4可以嵌套3flow4,对于这些情况,其控制流程有时候是非常复杂的,控制流常常在多个Web服务之间来回调用,但由于流程进入3flo w4活动后,将返回3flow4内活动执行的统一结果,因此可以将3flow4看做一个具有双向交互性质的基本活动,于是:

对于3sequence4嵌套3flow4情况可以看作3sequence4中包含了一个特殊的基本活动,活动按照顺序流程执行,当执行到3flow4时再进行相应处理即可,而3flow4的输出状态则是其在3sequence4结构中下一活动的输入状态.该结构如图9所示.

对于3flow4中嵌套3sequence4情况,由于3flow4根据不同的迁移条件选择不同的分支执行,因此,可以将每个分支看作3sequence4流程,各3sequence4流程具有相同的初始状态即为流程刚进入3flo w4时的状态.可以对于每个分支调用B2T算法产生状态迁

移关系,最后验证.该结构如图10所示.

对于3flow4中嵌套3flow4情况,我们对最内层3flow4调用F2T算法,生成相应状态转换图,之后将内层3flow4看作基本活动,对外层3flow4递归调用F2T算法,生成更大范围的状态转换图,.该结构如图11所示.

图113flo w4中嵌套3flow4

1053

6期骆翔宇等:一种基于认知模型检测的W eb服务组合验证方法

通过F2T算法,我们将具有3flow4结构的BPEL流程转化为了迁移七元组集合,实际上迁移七元组的提出就是为了描述状态转换关系,因此,该算法的最终目的就是将流程转化为状态转换图,这是进行形式化验证的步1,也是关键一步,能否自动生成状态转换图是关系到能否实现BPEL流程自动化验证的核心环节,有了状态转换图更能方便地利用模型检测工具对流程进行刻画.F2T算法相比B2T算法,加入了对数据流的支持,使得对流程的建模不仅仅是考虑到控制流的转移关系,更涉及到数据变量的变化情况,增加了状态空间中的状态数量,可验证的规范数量也大大增加,更能确保软件的正确性.

B2T与F2T算法主要用来生成迁移七元组,这是工作的第1步,而我们的最终目的是验证组合服务流程,因此,下面还必须用合适的模型检测工具对这些转换而来的七元组进行描述.本文采用自主开发的多主体系统模型检测工具M CTK作为底层验证平台.

312MCTK与主体声明

通过上节算法得到的迁移七元组集合必须自动转化为多主体系统模型检测工具M CTK的输入语言,才能实现对组合业务流程的自动化模型检测.因此,本节简要介绍M CT K,具体理论和系统开发方法请参考文献[11,13].

MCT K是我们开发的多主体系统符号化模型检测工具,在Linux环境下用C语言在经典模型检测工具NuSM V21112基础上扩展开发而来,采用Fabio Somenzi的CU DD OBDD软件包开发M CTK 的符号化模型检测算法.M CT K的输入语言是我们提出的多主体有限状态机的符号化描述,所刻画的多主体系统由一个环境和多个主体组成,主体间可进行交互.每一主体可以观察环境的部分或全部,不同的主体对环境的观察可以重叠,即它们可以同时观察环境中的同一部分.目前MCT K支持的时态认知逻辑ECKL n是H alpern和Vardi提出的时态知识逻辑CKL n[19]的一种扩展,ECKL n的语法定义如下:

f J=tr ue|p|?f|f C f|X f|f Uf|Ef|K i f|C#f.

显然,ECKL n语言是在线性时态逻辑LT L语言中扩展路径量词E(存在路径)、知识算子K i(对于每个智能体i)以及公共知识算子C#(对于一组智能体#)得到的,因此ECKL n的时态部分支持计算树逻辑CTL*.我们已在引言中通过一个时态认知规范展示其含义.篇幅所限,相关形式模型和语义请参考文献[11,13].

M CTK输入语言是在时态模型检测工具NuSMV21112输入语言上扩展定义的,因此M CTK利用m ain()模块定义环境变量和行为,并利用MODU LE定义主体的行为,支持每一主体的可观察变量集合的定义和声明.值得一提的是M CTK不必明确地表示主体的行为,仅需定义系统状态迁移关系即可,这一建模方法即可缩减状态空间,又有利于灵活定义环境和主体的行为所导致的状态迁移.

(1)M CTK的输入语言

M CTK的输入语言是在NuSM V基础上扩展而来,可以参考N uSMV手册来查阅其余相关细节,下面给出MCT K输入语言的语法结构:

M CT K_pr og ram J=

EnvDef;;环境定义

A g entDefL ist;;主体模块定义

EnvDef J=

"M ODU L E""main""("")"

V arD ef;;环境变量

A g entL ist;;主体声明

[Var A ssignDef];;环境变量赋值

[Var InitDef];;环境变量初始化

[ECK L nSpecD ef];;规范定义

A gentL ist J=

atom":"A gentType";"|Ag entList atom":"AgentType";"

A gentT ype J=;;主体ato m使用的模块名

ato m["("AP araL ist")"]

|"ar ray"number".."number"of"A gentT y pe

A Par aL ist J=;;实际参数列表

simple_f|A Pa raL ist","simple_f

A gentDefL ist J=A gentDef|Ag ent DefList Ag entD ef

A gentDef J=;;主体模块定义

"M ODU L E"at om["("FP araL ist")"]

L var Def;;局部变量

A ctDef;;动作变量

O var Assig nD ef;;可观察变量的赋值

P rot Def;;动作变量的赋值

F ParaL ist J=;;形式参数列表

["O bserv able"]atom;;如果指定Observ able,则表示

;;形参ato m可观察

|FPa raL ist","["O bser vable"]atom

A ctDef J=;;动作变量at om的定义

ato m":{"Ato mL ist"};"

A tomL ist J=ato m|A tomL ist","atom

ato m J=[A-Za-z_][A-Za-z0-9_\#-]*

1054计算机学报2011年

主体运行环境我们用m ain模块定义,VarDef 定义了一些环境变量,这些变量可用来表示环境的状态,当中的某些成员可以作为主体相互通信的共享变量.

(2)主体声明

我们对每一主体建立模型,下面介绍有关建模过程中涉及到的一些重要概念:

形式参数.一个主体模型的形式化参数在/Fpa-raList0中定义,其值将被实参替代,主体模型中的形参对于主体来说是可观察的,一个主体可以观察环境的部分变量,甚至其它主体的一部分变量. MCT K规定可观察变量的前缀必须是/ObsPrm_0,表明该变量是可观察的.

可观察变量.一个主体的可观察变量的集合O i 主要由该主体的局部变量以及可观察的实际参数组成,在我们实验中,主体的局部状态由其可观察变量指定.如果在LvarDef中定义的变量是一个模块实例,则在动作变量集合A ctDef中定义的变量也是主体的可观察变量.

可观察变量赋值.主体中关于可观察变量的评价函数实际上用来描述主体的可观察变量的值是如何改变的,是一个从主体部分状态集合到另一个部分状态集合的映射函数,迁移函数在OVarInitDef 和OvarTransDef中定义.

313将七元组转化为MCTK的输入语言

上节简单介绍了M CTK及其输入语言,由此可见MCT K实际上是在NuSMV基础上引入了可观察变量的概念,两者形参的唯一不同之处就是MCT K需要在形参前面加上前缀/ObsPrm_0,表示该形参是可观察的.对于模型的描述M CTK与NuSM V基本相同,需要详细刻画状态转换过程,主要包括某状态在一定条件发生情况下迁移到另一状态.迁移七元组详细给出了状态转换关系,其第1项指明了迁移的初始状态,最后一项指明了迁移的末状态,第2、3、4项则分别指明了导致迁移发生的状态变量的变化情况,使得MCT K可以方便地利用这些信息对状态迁移过程进行描述.

在211节我们引入/通道0及/通道变量0的概念,/通道0实际是一种消息机制,是为了方便实现对服务之间交互过程的建模而引入的/通道0概念,它实际是不存在的.但是,组合W eb服务的各原子服务必须相互/联系/起来,否则单个主体无法与外界交流,如果反映在状态转换图中,则多个主体的状态转换图相互独立,不存在/联系0,也就无法实现组合流程的模型检测.因此,从直观上看主体通过所谓/通道0建立联系,但从本质上说主体实际是通过/通道变量0建立起的/联系0,因为/通道变量0是具有直接交互关系的两个主体之间的共享变量,相互/联系0的主体通过此变量实现信息的发送与接收.为了方便对服务之间信息交互过程进行建模,实现将多个服务/联系0起来的目的,我们将服务之间的交互过程看成是/通道变量0通过/通道0在交互的Web 服务之间传输的过程.为此,我们必须对/通道0这种消息机制进行建模.

在用M CTK对/通道0建模时,将/通道0看作与Web服务一样的实体,只不过主体的状态通过主体的变量标识,而/通道0的状态则由/通道0中当时的信息标识.

对主体状态的迁移我们是这样刻画的:在活动执行前,主体处于状态state0,信息M sg到来,执行活动,此时该主体入通道P T的值:v alue(P T)= M sg,主体执行活动完毕迁移到state1.假设该主体名为A gentEx a,则上述迁移可形式化表述为

(Ag entEx a.state=state0&value(P T)=M sg)] nex t(A gentEx a.state)=state1.

当我们将/通道0看作与Web服务一样的实体时,其描述思想与状态迁移的描述思想是类似的.需要记录此时刻主体状态以及上一时刻导致主体变为此状态的信息及其经历的通道名.例如:主体A gentE x a在接收到通道Por tT y p eI n传来的信息M sg后,状态变为get_Msg,之后又通过通道P or tT y p eOut发送信息Msg1,则我们可以将上述迁移形式化描述为

(state=get_Msg)&(Por tT y p eI n.state=M sg)] nex t(P or tT y p eOut.state)=M sg1.

这样,我们通过通道将各个主体连接在了一起,确切地说是通过通道中交互的信息将它们联系起来.当某个主体发送了某消息后,另一主体则通过相同/通道0接收了该消息,使得两个主体在此时有了联系,更具体地说就是将具体的Web服务方联系了起来.因此,由于七元组中包含了通道名称、该通道中的交互信息以及该信息的流动方向,再加上清晰的状态转换关系和相应变量的赋值,使得我们利用M CTK对流程的建模更加方便.

基于上述思想,本文提出了将迁移七元组转换为MCT K代码的转换算法,这样做是因为描述BPEL的控制流程时,MCT K的编码工作繁琐、冗长,但更重要的是机械化,为了进一步提高模型检测的自动化程度,我们提出T2M算法,用来将产生的一组迁移七元组自动转化为M CT K代码.

1055

6期骆翔宇等:一种基于认知模型检测的W eb服务组合验证方法

算法T2M7-tuple y M CT K描述代码.

输入:迁移七元组集合

输出:M CT K描述代码

/*假设共产生n个七元组*/

/*预处理阶段:该阶段用来初始化与通道建模有关的变量和集合,产生的代码放在M CT K文件的最上端*/

1.设置source{}集合和des t{}集合,初始化为none.

搜索多主体组合流程BPEL源代码,将3p ar tner-

L ink s4中的3p ar tner L ink name4属性值放入这两个

集合中;

2.设置M sgty pe{}集合,初始化为none.搜索多主体

组合流程BPEL源代码,将3v ar iables4中的3v ar ia-

ble name4属性值放入这个集合中;

3.搜索每个W eb服务的WSDL源代码,抽取代码中

的3p or tT y p e name4属性,找到所有与本主体相联

系的通道,包括所有入通道和所有出通道;

/*迁移描述阶段:从步4起是针对原子服务的建模过程,步4的主体定义完成后,将片段1和片段2的

代码放在其后*/

4.按照如下格式定义主体:M ODU LE主体名(通道i

名称,ObsPrm_通道i.M sg ty p e,O bsP rm_通道i.

sour ce,O bsP rm_通道i.des t);

5.设置state{}集合,将本Web服务对应产生的所有

七元组中的源状态和末状态放入此集合;

/*片段1:对单个W eb服务产生描述状态迁移的代码片段*/

6.for each tup le[i](i F n)

7.{

8.nex t(state)B=case

9.(state=tup le[i](1))&(O bs Pr m_tup le[i](5).

M sg ty p e=tup le[i](2)):tup le[i](7);

10.}

/*片段2:对单个Web服务产生描述通道中信息变化的代码片段:*/

/*假设满足tup le[i](6)=OUT的元组共有m个,则:*/

11.for each tup le[j](j X i C j F m F n)

12.{

13.if(tup le[i](1)==tup le[j](7))then

14.{

15.nex t(tup le[i](5).M s gty p e)B=case

(s tate=tup le[i](1))&(ObsPr m_tup le[j]

(5).Ms gty p e=tup le[j](2)):tup le[i](2);

16.nex t(tup le[i](5).s our ce)B=case

(state=tup le[i](1))&(ObsPr m_tup le[j]

(5).M sgty p e=tup le[j](2)):tup le

[i](5).sour ceA gent;

17.nex t(tup le[i](5).d est)B=case

(s tate=tup le[i](1))&(ObsPr m_tup le[j]

(5).M s gty p e=tup le[j](2)):tup le

[i](5).des tA gent;

}

算法说明:我们标记tup le[j]的第i项为tup le[j](i),于是tup le[j](1)代表迁移七元组的第一项,即活动的初始状态,tup le[j](7)为最后一项,即活动的末状态等等.我们将预处理阶段和迁移描述阶段的代码按照如图12所示顺序组合在一起就完成了BPEL流程的形式化描述.

预处理阶段:

M ODULE ch ann el

VAR

Sou rce:{,};

Dest:{,};

M s gtyp e:{,};

迁移描述阶段:

原子服务1:状态迁移描述代码;

通道建模代码;

原子服务2:状态迁移描述代码;

通道建模代码;

原子服务n:状态迁移描述代码;

通道建模代码;

待验证规范

图12M CT K代码的组成

从图12中可以看出,预处理阶段产生的代码放在整个程序的最上面.算法步1用来找到所有参与流程的Web服务方;步2、3分别确定所有用到的交互变量和与每个主体相连接的/通道0.前3步用来初始化为了实现通道机制所必须设置的相关变量和集合.步4是主体定义,其括号中的参数皆为形式参数,用来接收由主模块传来的实参值,该步与后面生成的代码组合在一起构成对单个W eb服务BPEL 流程的形式化描述;步5声明单个Web服务流程的所有状态变量.片段1用来产生七元组中各状态的转换关系,步6开始循环,产生描述主体状态迁移关系的代码;步9可解释为当主体状态为cur(state)时,通过入/出通道接收/发送信息后,状态变为nex t(state).片段2用来描述各通道中信息的变化情况,为了不产生混乱,我们针对主体的出通道进行建模(实际上,一个主体的入通道必为另一主体的出通道),当某个七元组L1的tup le[i](6)=O UT时,说明其中的channel表示此主体的出通道,此时搜索其余七元组,若找到七元组L2,其末状态与L1初状态相同,说明L2是L1的上一个迁移,则L1对应的活动执行时,其通道的建模需考虑L2通道信息的变化情况,这也是算法步15的思想;步16、17说明交互通道的源Web服务和目标Web服务.由于算法需要针对某一七元组扫描其余n-1个七元组以找到满足步13判断条件的元组集合,故而在最差情况下其时间复杂度为O(n!).由以上说明可知,为了将Web服务组合建模为多主体系统,算法在转换过

1056计算机学报2011年

程中需要先将参与Web 服务组合的每个服务(组件)建模为主体,然后在环境中对每一主体与代表其它Web 服务的主体的交互通道进行建模,从而构造相应的多主体系统.以下我们通过一个示例来说明算法的执行过程,实验结果表明实例流程形式化验证的自动化程度大大提高.

4 一个示例:虚拟旅游系统

本节利用我们开发的基于时态认知逻辑的模型检测工具MCT K 对虚拟旅游系统Virtual Travel Agency(V TA)

[18]

进行验证,V TA 通过对机票预订

服务商和酒店预订服务商的整合来为即将旅行的人提供服务,该系统接收用户输入,并将最终相关预订结果返回给用户.如图13所示

图13 虚拟旅游订票系统示意图

该Web 服务组合涉及4个主体:用户、VT A 、机票预订服务商、酒店预订服务商.用户向VT A 发送预订机票及酒店请求,之后V TA 向机票预订服务商发送请求订票信息,机票预订服务商查询航班,若无法满足用户需求(例如航班临时取消),则返回信息给VTA,VT A 将该结果返回给用户,流程终止.若可以预订,则VT A 向酒店预订服务商发送请求信息并将机票预订服务商提供的offer 返回给用户,用户可以选择接受或者拒绝预订结果,若接受,则最终VTA 返回用户关于酒店、机票及旅行成本等信息.

我们将这4个Web 服务看作4个主体,用BPEL Designer 创建每个Web 服务的BPEL 源代码,在此过程中需要注意各主体之间共享变量的设置.然后将此BPEL 源代码作为B2T 算法输入,从而生成四个相应迁移七元组集合.因此,转换工作不是针对Web 服务组合流程的BPEL 源代码,而是针对每个参与组合的单个Web 服务的流程代码.限于篇幅,本文以状态数量较少的机票预订服务商为例说明转换过程,在转换前我们去掉描述该服务的

BPEL 源代码中那些没有在212节介绍的活动,然后调用B2T 算法得到迁移七元组集合如下:

(sleep ,f r equestM s g,E ,E ,Flight _P T ,I N ,get _f r equestM s g);(get _f r equestM sg,f of fer M sg ,E ,E ,Flight _CallbackP T ,OU T ,send _f of fer M sg );

(send _f of f er Msg ,f ackMs g,E ,E ,Flight _PT ,IN ,get _f ackMs g);(get _f ack Ms g,f ticketM sg,E ,E ,Flight _CallbackP T ,O U T ,send _f ticketM sg);

(send _f tick etM sg,f ticketA ckM s g,E ,E ,Flight _PT ,I N ,get _f ticketA ckM s g);(send _f of f er M sg ,f N ackM s g,E ,E ,Flight _PT ,I N ,get _f N ack Ms g);

(get _f r equestM sg ,f N otavailM sg,E ,E ,F light _CallbackP T ,OU T ,send _f N otavailM sg).

下面将迁移七元组作为算法T 2M 的输入,得到自动生成的代码,将其输入M CTK,从而验证该组合Web 服务的正确性.根据算法:

(1)搜索该组合流程的BPEL 源代码,找到用3partnerLink name 4属性标示的所有Web 服务,将这些Web 服务名放入sour ce{}集合和tar get{}集合中.在该组合流程的BPEL 源代码中找到4个主体的声明,分别是Flight_PLT 、H otel_PLT 、U ser_PLT 、VT A,分别代表机票预订服务商、酒店预订服务商、用户、V TA 代理,将它们放入上述两个集合,

则:sour ce ={none,Flight _P LT ,H otel _P L T ,User _P L T,VTA };dest ={none,F light _P L T,H otel _P L T,User _P L T,VT A };

(2)设置Msgty p e{}集合,该集合存放组合流程中所有Web 服务的交互变量,这些变量可以从组合流程BPEL 代码中的3variable nam e 4属性中抽出.对于机票预订服务商而言,需要将每个迁移七元组的第2项tup le[j ](2)放入该集合,它们是Msgyty p e ={f r equestM sg 、f off erM sg 、f ackMsg 、f ticketMsg 、f ticketA ckM sg 、f N ackMsg 、f N otavailMsg ,};

(3)搜索本Web 服务的WSDL 源代码,抽取3portT ype name 4属性值,找到本主体与外界联系的通道.对于本例而言,它们是Flight _P T 和Flight _CallbackP T ,前者的源主体为VTA ,目标主体为Flight _P L T,后者相反.为了书写方便本文分别将它们按上述顺序简写为ch 1、ch 2;

(4)对机票预订服务商模块进行定义:MOD -UL E F light _P LT (ch 1,ch 2,ObsPr m _ch 1.M sg -ty p e,ObsP r m _ch 1.sour ce,ObsPr m _ch 1.d est,Ob -sPr m _ch 2.Msgty p e,ObsPr m _ch 2.sour ce,ObsPr m _ch 2.dest);

1057

6期骆翔宇等:一种基于认知模型检测的W eb 服务组合验证方法

(5)设置state{}集合,该集合存放了原子服务流程执行过程中经历的所有状态,可以从该Web服务对应的所有迁移七元组的第一项tup le[j](1)和最后一项tup le[j](7)抽出,这可由程序自动完成.对于本例,它们是state={sleep,get_fr equestMsg, send_f o f fer M sg,get_f ackM sg,send_f ticketMsg, get_f ticketA ckMsg,get_f N ackM sg,send_f N o-tav ailM sg,};

(6)针对每个Web服务,根据其相应七元组集合产生状态迁移描述代码,对于机票预订服务商模块,我们以其中一个七元组为例说明代码的产生过程.例如对于七元组(get_f requestMsg,f off er Msg, E,E,Flight_CallbackP T,OUT,send_f of f er Msg):算法说明当主体当前状态为get_f r equestMsg,运用通道Flight_CallbackPT发送了信息f of f er Msg 后,主体状态迁移到send_f of f er Msg,该过程可写为:

nex t(s tate)B=case

(state=get_f requestM sg)&(Flight_CallbackP T.Ms gty p e=

f of f er M sg):send_f of f er M sg;

据此,对应每个七元组,再考虑到可观察变量概念,最后根据算法自动生成相应状态迁移语句.以下列出描述本主体状态迁移的部分代码:

nex t(s tate)B=case

(state=s leep)&(ObsP r m_ch1.M s gty p e=f r eq uestM sg): get_f r eques tM s g;

(state=send_f of f er M sg)&(ObsP rm_ch1.M s gty p e=

f ack M sg):get_f ackM sg;

(state=send_f of f er M sg)&(ObsP r m_ch1.M s gty p e=

f N ackM sg):get_f N ackM sg;

(7)针对每个Web服务,根据其相应七元组集合产生描述通道中信息变化的代码模块,算法首先从迁移七元组中找到tup le[i](6)=O UT的元组,也就是刻画主体运用出通道发送信息的迁移元组,在本例中它们是:

(get_f r equestM sg,f of f er M sg,E,E,Flig ht_Cal lbackPT, OU T,s end_f of f er M sg);

(get_f ackM sg,f tick etM sg,E,E,Fl ight_Cal lbackPT,OU T, send_f ticketM sg);

(get_f reques tM sg,f N otav ailM s g,E,E,Flight_Cal lbackPT, OU T,s end_f N otavailM sg).

然后,找到末状态与它们的初状态相同的七元组,按照算法展开操作.例如:针对5(get_f ackM sg, f tick etM sg,E,E,Flig ht_CallbackP T,OUT,send_ f tick etM sg),搜索其余元组,若某个元组的末状态与5的初状态get_f ackMsg相同,证明我们找到了5的上一迁移5p,于是,在5p迁移发生的情况下,下一时刻5的通道Flight_CallbackP T中的内容变为f ticketMsg,并且根据(3),该通道源主体为Flight_P L T,目标主体为VT A.

由此,对上述3个七元组,根据算法自动生成相应通道描述语句,以下列出描述本主体出通道模型的代码:

/*说明在上一迁移发生情况下,本次迁移导致的通道中的信息变化*/

nex t(ch2.M sg ty p e)B=case

(state=get_f reques tM sg)&(ObsP r m_ch1.M sgty p e=

f R equestM sg):f off er M sg;

(state=get_f reques tM sg)&(ObsP r m_ch1.M sgty p e=

f R equestM sg):f N otav ailMs g;

(state=get_f ack M sg)&(O bs Pr m_ch1.Ms gty p e=

f ackM sg):f tick etM sg;

/*说明Flight_CallbackP T的源主体与目标主体*/

nex t(ch2.sour ce)B=case

(state=get_f reques tM sg)&(ObsP r m_ch1.M sgty p e=

f reques tMs g):Flight_P L T;

(state=get_f ack M sg)&(O bs Pr m_ch1.Ms gty p e=

f ackM sg):F light_PL T;

nex t(ch2.dest)B=case

(state=get_f reques tM sg)&(ObsP r m_ch1.M sgty p e=

f reques tMs g):VT A;

(state=get_f ack M sg)&(O bs Pr m_ch1.Ms gty p e=

f ackM sg):V T A;

需要说明的是,之所以在针对主体的建模过程中,只描述其出通道信息的变化而未理会入通道,主要是考虑到统一、整齐,防止重复建模,实际上某一主体的入通道必然也是其它主体的出通道,在对其它主体建模时还是会考虑到;

(8)最后,根据图12,将(4),(5),(6),(7)生成的代码组合起来,得到机票预订服务流程的部分M CTK描述代码如下:

/*定义主体*/

M O DU L E Flig ht_P L T(ch1,ch2,ObsP r m_ch1.M sgty p e, ObsPr m_ch1.sour ce,ObsP rm_ch1.des t,ObsPr m_ch2.

M sgty p e,O bs Pr m_ch2.sour ce,ObsPr m_ch2.d est)

/*声明状态*/

State:{sleep、get_f r equestM sg、send_f of f er Ms g、get_f ackMs g、send_f tick etM sg、get_f tick etA ck M sg、get_f N ack M sg、send_f N otav ailM sg}

/*描述状态迁移*/

nex t(state)B=case

(state=sleep)&(ObsPr m_ch1.M s gty p e=f r equestM sg): get_f r equestM sg;

1058计算机学报2011年

(state=send_f of f er M sg)&(ObsP r m_ch1.M sgty p e=

f ackM sg):

g et_f ackM s g;

(state=send_f of f er M sg)&(ObsP r m_ch1.M sgty p e=

f N ack Ms g):get_f N ack Ms g;

/*描述通道变化*/

nex t(ch2.Ms gty p e)B=cas e

(state=get_f r equestM sg)&(ObsP r m_ch1.M sg ty p e=

f reques tMs g):f of f erM s g;

(state=get_f r equestM sg)&(ObsP r m_ch1.M sg ty p e=

f reques tMs g):f N otav ailM s g;

(state=get_f ack M sg)&(O bs Pr m_ch1.M sgty p e=

f ackM sg):f ticketM sg;

nex t(ch2.sour ce)B=case

(state=get_f r equestM sg)&(ObsP r m_ch1.M sg ty p e=

f reques tMs g):Flight_P LT;

(state=get_f ack M sg)&(O bs Pr m_ch1.M sgty p e=

f ackM sg):Fl ight_PL T;

nex t(ch2.des t)B=case

(state=get_f r equestM sg)&(ObsP r m_ch1.M sg ty p e=

f reques tMs g):VT A;

(state=get_f ack M sg)&(O bs Pr m_ch1.M sgty p e=

f ackM sg):V T A;

根据此方法,我们继续生成其它Web服务的MCT K代码并定义主模块,将它们按照图12所示放在同一M CTK源文件下,就自动生成了组合Web服务流程的MCT K描述代码.

在生成M CTK代码后,需要手工将待验证规范加入自动生成的M CTK代码.我们已成功验证了若干时态认知规范.下列规范中SPEC表示时态规范, ECKLnSPEC表示时态认知规范,为了书写方便,用ag entA代表用户主体、ag entB代表VT A、agentC 代表航空订票系统、agentD代表酒店预订系统.篇幅所限,下面仅列出两个规范的验证结果.首先是一个时态逻辑规范:

SPE C A G((agentA.state=send_cr eques tM s g)y

EF(agentD.s tate=send_hoff er M sg)).

这个规范的含义是当用户主体发送了请求信息后,酒店预订服务商有可能在将来某个时刻发来相关酒店预订信息.验证结果为true,验证时间为01428s.当用户发送请求信息后,若没有机票可供预订,则预订酒店服务不会被启动,若有机票可以预订,则V TA将马上向酒店预订服务商发送请求,若酒店可预订,则此规范成立.

此外,我们还验证了下列时态认知逻辑规范:

ECK L nSP EC A G((ch5.M sgty p e=ticketMs g)y

A F(ag entA K((ch2.Ms gty p e=f ticketMs g)&

(ch4.M s gty p e=hticketM sg))))其中形如/a K f0的公式表示主体a知道f成立.该规范的意思是当用户预订成功相关服务后,它必然知道机票预订服务商发送了机票并且酒店预订服务商发送了酒店预订成功的相关信息.验证结果为true,验证时间为11832s.

5结论与展望

本文从Web服务流程描述语言WS-BPEL的形式化验证需求出发,提出BPEL语言的形式模型并给出活动执行语义,结合该语言与模型检测工具M CTK自身特点提出迁移七元组这一中间形式,建立BPEL活动与迁移七元组之间的一一对应关系,在此基础上给出该语言到模型检测工具M CTK输入代码的转换算法,实现BPEL流程的自动化验证,从而支持时态和认知逻辑规范的验证.实验结果表明了该方法的有效性.下一步工作将对BPEL的其它活动,如错误处理等进行建模,从而更完整地支持BPEL建模,进一步提高建模和验证过程的自动化程度.

参考文献

[1]Fu X,Bultan T,Su J.Analysis of in teracting BPEL w eb

services//Proceedings of the13th intern ational con feren ce on

W orld W ide W eb(WW W.04).New York,U SA,2004:

621-630

[2]Fu Xiang.Formal specification an d verification of asyn-

chr on ou sly com municating w eb services[Ph.D.diss ertati on].

Un iversity of Californ ia,Santa Barb ara,2004

[3]Kazhamiakin R.Form al analysis of w eb ser vice com position

[Ph.D.dis sertation].Un iversity of T rento,Tr ento,2007 [4]Foster H,Uchitel S,M agee J,Kramer J.M ode-l based ver-i

fication of w eb service compos ition s//Proceeding of the18th

IEEE Intern ational Conference on Automated S oftw ar e En g-i

neering(AS E.03),M ontr eal,Canada,2003:152-163

[5]Foster H,U chitel S,M agee J,Kram er https://www.wendangku.net/doc/d814626218.html,patibility ver-

ification for web s ervice ch oreography//Proceedings of the

IEEE Intern ational Confer ence on Web Services(ICW S.04).

San Diego,California,US A,2004:738-741

[6]W alton C D.M odel checking mult-i agent w eb services//Pro-

ceedings of the2004AAAI Spring Symposiu m on Seman tic

W eb Services.S tanford,California,2004:68-75

[7]Nakajima S.Ligh tw eight form al analysis of web s ervice

flow s.Progress in Inform atics,2005(2):57-76

[8]M ongiello M,Castelluccia D.M odelling and verification of

BPEL b usiness processes//Proceedings of the J oin t M eeting

of the4th W or kshop on M ode-l Based Development of Com-

puter-Based Sys tems and the3rd Internation al W orks hop on

M ode-l Based M eth odologies for Pervasive and Em bedded

Software.Potsdam,Germany,2006:144-148

1059

6期骆翔宇等:一种基于认知模型检测的W eb服务组合验证方法

[9]Ouyang Chun,Verbeek E,van der Aals t W M P,Breutel S,

Dumas M a,ter H ofstede A H M.WofBPEL:A tool for au-

tomated an alys is of BPEL processes//Proceedings of the3rd

In ternation al Conference on Ser vice Orien ted Computing

(ICSOC2005).Amsterdam,T he Neth erlands,2005:484-489 [10]Ouyang Chun,van der Aals t W M P,Breutel S,Du mas M,

ter Hofstede A H M,Verb eek H M W.Formal semantics

and analysis of control flow in W S-BPEL.Science of Com-

pu ter Pr ogramming,2007,67(2-3):162-198

[11]Luo Xiang-Yu.Sym bolic m odel checking mult-i agent systems

[Ph.D.dissertation].Sun Yat-sen University,Guangzhou,

2006(in Ch ines e)

(骆翔宇.多主体系统的符号模型检测[博士学位论文].中

山大学,广州,2006)

[12]Su Ka-i Le.M odel checkin g temporal logics of know ledg e in

distributed sy stems//Proceedings of the19th National Con-

ference on Artificial In tellig ence,th e16th Conference on In-

n ovative Application s of Artificial Intelligence.S an J ose,

California,U SA,2004:98-103

[13]Su Ka-i Le,Sattar A,Luo Xiang-Yu.M odel checking tempo-

ral logics of know ledge via OBDDs.The Computer Journal,

2007,50(4):403-420

[14]Lom uscio A,Qu H ong-Yang,Raimondi F.M CM AS:A

model checker for the ver ification of mult-i agent system s//

Proceedings of the21st International Conferen ce on C om put-

er Aided Verification(CAV2009).Grenoble,France,2009:

682-688

[15]Gam mie P,van der M eyden R.M C K:M odel ch eck ing the

logic of know ledge//Proceedings of the16st International

Conference on Com pu ter Aided Verification(CAV2004).

Boston,M A,U SA,2004:479-483

[16]Lomus cio A,Qu H ong-Yang,Solanki M.T ow ards verifying

contract regu lated service comp os ition//Proceedings of the

IEEE Intern ational Confer ence on Web Services(ICW S.08).

Beijing,C hina,2008:254-261

[17]Lomus cio A,Qu H ong-Yang,S ergot M,Solanki M.Verif-

ying temporal and epistemic properties of w eb s ervice compo-

sition//Proceedings of the5th International Conference on

Service-Oriented Computi n g(ICSOC2007).Vienna,Au stria,

2007:456-461

[18]Formal R K.An alys is of w eb service compos ition[Ph.D.s u-

pervisor].U nivers ity of T ren to,T rento,2007:79-84 [19]H alpern J Y,Vardi M Y.M odel checkin g vs.th eorem pro-

ving:a manifes to//Proceedin gs of the2nd International Con-

ference on Principles of Know ledge Representation and Rea-

soning.Cambridge,M ass achusetts,U SA,1991:325-

334

LUO Xiang-Yu,bo rn in1974,

Ph.D.,associate pro fesso r.H is r e-

sea rch int erests include mo del checking,

tempor al log ics,epist emic log ics,r ea-

soning about know ledge,mult-i ag ent

systems,and v erificat ion of security

pro tocols.

TAN Zheng,bo rn in1982,M.S..H is r esear ch inter-

ests include mo del checking,tempo ral lo g ics,epistemic log-

ics,and Web services.

SU Ka-i Le,bor n in1964,Ph.D.,pro fesso r,Ph.D.

super viso r.H is research inter ests include model checking,

r easo ning about know ledge,non-mono tonic reasoning,

mult-i agent systems,modal log ics,tempo ral log ics,proba-

bility reasoning,and v erification o f secur ity prot ocols,log ic

pro gr amming.

WU L-i Jun,bo rn in1965,Ph.D.,associat e pr ofesso r.

H is research inter ests include model checking,reasoning

about kno wledg e,mult-i ag ent systems,and ver ification o f

secur ity pr oto co ls.

Background

T oday,Web ser vices are w idely dist ributed o ver the In-

ter net,the tasks of co mpo site Web serv ices are solved

throug h t he interactions betw een these Web services in-

v olved.H owev er,during the inter action process,it is poss-i

ble that some unexpected o r/not no rmal0infor mation inter-

actio ns w ill occur,w hich may cause some inco rr ect r esult

generated and serio usly low er the quality and r obustness of a

sy stem.O n the other hand,due to the autonomy of single

Web ser vice and the lo ose-coupling betw een co mpo site Web

ser vices,it is ver y suitable to model W eb serv ice compos-i

t ions as mult-i ag ent sy stems.T her efore,to ensure Web

ser vices can pro vide cor rect functio n,it is necessar y to apply

for mal ver ificatio n techniques,such as model checking,to

the v erification of the tempor al and epistemic specificat ions o f

Web ser vice composit ions,w her e epist emic specificatio ns ar e

pr oper to mult-i ag ent sy stems.T his w o rk is g radually be-

co ming a hot ar ea of research on formal v erificat ion domain.

T o t he best of o ur kno wledg e,such fo rmal ver ificatio n tech-

niques fo r Web serv ice co mpo sitio n ar e in the init ial research

st age,and the entir e ver ification process is not automatic,

ther e ar e a lo t of manual operatio ns during the ver ification

pr ocess,especially in the modeling stag e.T herefor e,in o r-

der to make the W eb serv ices v erification pro cess mor e auto-

mat ic,the autho rs pr opose a ser ies of alg o rithms for transla-1060计算机学报2011年

安全模型Read

Windows 安全模型：每个驱动程序作者都需要了解的内容 Updated: July 7, 2004 On This Page 简介 W indows 安全模型安全场景：创建一个文件驱动程序安全责任行动指南和资源本文提供关于为 Microsoft Windows 家族操作系统编写安全的内核模式驱动程序的信息。其中描述了如何将 Windows 安全模型应用于驱动程序，并解释驱动程序作者必须采取哪些措施来确保其设备的安全性。简介 Windows 安全模型基于安全对象。操作系统的每个组件都必须确保其负责的对象的安全性。因此，驱动程序必须保证其设备和设备对象的安全性。本文总结了如何将 Windows 安全模型应用于内核模式驱动程序，以及驱动程序编写人员必须采取哪些措施来确保其设备的安全性。一些类型的设备适用于附加的设备特定要求。请参阅 Microsoft Windows Driver Development Kit (DDK) 中的设备特定的文档，以了解详细信息。注意：关于本文中讨论的例程和问题的当前文档，请参见 Windows DDK 最新版本。关于如何获取当前的 DDK 的信息，请参见 https://www.wendangku.net/doc/d814626218.html,/whdc/devtools/ddk/default.mspx. Top of page Windows 安全模型 Windows 安全模型主要基于每个对象的权限，以及少量的系统级特权。安全对象包括（但不限于）进程、线程、事件和其它同步对象，以及文件、目录和设备。

对于每种类型的对象，一般的读、写和执行权限都映射到详细的对象特定权限中。例如，对于文件和目录，可能的权限包括读或写文件或目录的权限、读或写扩展的文件属性的权限、遍历目录的权限，以及写对象的安全描述符的权限。更多信息（包括完整的权限列表）请参见 MSDN 库的“安全性”节中的“安全性（常规）”，该库位于https://www.wendangku.net/doc/d814626218.html,. 安全模型涉及以下概念： ?安全标识符 (SID) ?存取令牌 ?安全描述符 ?访问控制列表 (ACL) ?特权安全标识符 (SID) 安全标识符（SID，也称为安全主体）标识一个用户、组或登录会话。每个用户都有一个唯一的 SID，在登录时由操作系统检索。 SID 由一个权威机构（如操作系统或域服务器）分发。一些 SID 是众所周知的，并且具有名称和标识符。例如，SID S-1-1-0 标识所有人（或全世界）。存取令牌每个进程都有一个存取令牌。存取令牌描述进程的完整的安全上下文。它包含用户的 SID、用户所属组的 SID、登录会话的 SID，以及授予用户的系统级特权列表。默认情况下，当进程的线程与安全对象交互时，系统使用进程的主存取令牌。但是，一个线程可以模拟一个客户端帐户。当一个线程模拟客户端帐户时，它除了拥有自己的主令牌之外还有一个模拟令牌。模拟令牌描述线程正在模拟的用户帐户的安全上下文。模拟在远程过程调用 (Remote Procedure Call, RPC) 处理中尤其常见。描述线程或进程的受限制的安全上下文的存取令牌被称为受限令牌。受限令牌中的 SID 只能设置为拒绝访问安全对象，而不能设置为允许访问安全对象。此外，令牌可以描述一组有限的系统级特权。用户的 SID 和标识保持不变，但是在进程使用受限令牌时，用户的访问权限是有限的。CreateRestrictedToken函数创建一个受限令牌。受限令牌对于运行不可信代码（例如电子邮件附件）很有用。当您右键单击可执行文件，选择“运行方式”并选择“保护我的计算机和数据不受未授权程序的活动影响”时，Microsoft Windows XP 就会使用受限令牌。

基于KANO模型的商业银行产品服务质量评价研究

基于KANO模型的商业银行产品服务质量评价研究随着我国金融市场的不断发展,居民收入水平不断提高,一方面,我国居民的金融需求正日益增加,另一方面,互联网金融的发展与融资渠道的增加,也使得我国商业银行所面临的市场竞争日趋激烈。商业银行如何迎接新兴科技、新兴市场的挑战,如何满足消费者更细化更专业的金融需求,其实是一个问题的正反两面。本文即基于此,运用KANO模型,探究消费者对商业银行所提供产品或服务质量特征的判定规律,找出影响消费者满意度或吸引引消费者关注度的魅力质量、一维质量等关键质量要素,并探究消费者的不同性格特征与其对质量要素的判定之间的关联程度,以期为商业银行进一步获取市场,赢得消费者建言献策。本文得出的主要研究结论有：1、消费者的性格特征可以分为三类：内向理智型、外向顺从型与外向独立型。其中,内向理智型消费者在购物过程当中,不喜与他人产生过多的交互；外向顺从型性格的消费者,会体现出对他人较高的顺从性；外向独立型消费者,善于在与他人交流过程中获取关键产品信息。2、从样本总体来看,银行主流的22个质量特性中,被归为魅力质量的共有5个,分别为营业网点或ATM机到达方便；银行卡卡面花色可以定制或卡号可以自主选择；银行卡拥有较多的特惠商户,会有各种刷卡打折优惠活动；贷记卡有约定账户自动还款功能；银行卡有偿提供余额变动短信提醒等。其余17个质量特性中,除“在业务办理中,员工能快速回应您的要求,办事效率高“为一维质量要素,其他项均为无差异质量要素。3、不同性格消费者之间对质量要素的判定结果有所不同：肉向理智型消费者多为女性,年龄偏大,收入较高,而消费产品较为传统,被其判定为魅力质量的银行产品质量特征仅为5项；外向

认知ABC理论

认知ABC理论情绪不是由某一诱发性事件本身所引起的，而是由经历了这一事件的个体对这一事件的解释和评价所引起的。这一理论又被称作ABC理论。ABC来自 3个英文字的字首。在ABC理论的模型中，A是指诱发性事件（Activating events）；B是指个体在遇到诱发事件之后相应而生的信念（Beliefs），即他对这一事件的看法、解释和评价；C是指在特定情景下，个体的情绪及行为的结果（Consequences）。通常，人们会认为人的情绪及行为反应是直接由诱发性事件A引起的，即是A引起。RET的ABC理论指出，诱发性事件A只是引起情绪及行为反应的间接原因；而B——人们对诱发性事件所持的信念、看法、解释才是引起人的情绪及行为反应的更直接的起因。当我们的日常生活出现问题，大多数人会不假思索地认为，是那些发生了的事情使我们感到难受。例如，当我们感到愤怒或忧伤，我们会认为是别人使我们产生这样的感受;当我们感到焦虑、受挫或忧伤，我们倾向于责怪自己的处境。然而，正如埃利斯指出的那样，并不是人和事让我们喜悦或悲伤－－它们只不过是提供了一种刺激。其实，是我们的认知决定了我们在特定情况下的感受。为了阐明这一理论，埃利斯提出了“A-B-C”模型: A代表“前因”(antecedent)(引发反应的情况)。 B代表“观念”(beliefs)(我们对该情况的认知)。 C代表“结果”(consequences)(我们的感受和行为)。尽管我们倾向于责怪“A”(前因)造成了“C”(结果)，其实是“B”(观念)使我们产生了那样的感受。让我们来看一个简单的例子: 设想你约会要迟到了，你感到很着急。 A:前因:约会将要迟到 C:结果:焦虑，烦躁，开车鲁莽你感到焦虑(C)，不是因为你将要迟到(A)，而是因为你认为自己必须守时并且担心迟到的后果(B)。在这种情况下使人感到焦虑的典型观念包括:“我必须守时。如果我迟到，别人就不会喜欢我了。不论何时，我都必须得到每个人的赞赏。如果他们对我有看法，那可麻烦了。” 行为的决定因素：中介变量托尔曼强烈反对把行为看作是刺激-反应的简单做法，认为介于环境刺激和行为反应之间的心理过程与有机体所作出的行为反应具有密切的关系，他提出中介变量的概念，认为认知、期望、目的、假设和嗜好等都是中介变量的具体表现形式。他还认为，对于行为的最初

安全防护用具的检验方法

安全防护用具的检验方法姓名：XXX 部门：XXX 日期：XXX

安全防护用具的检验方法个人安全防护用品常用的安全护具安全鞋，劳保鞋，防静电鞋，绝缘鞋，防护服等等必须认真进行检查、试验。安全网是否有杂物，是否被坠物损坏或被吊装物撞坏。安全帽被物体击打后，是否有裂纹等。经常对安全护具的检查按要求进行一安全帽：检验周期为每年一次。3kg重的钢球，从5m高处垂直自由坠落冲击下不被破坏，试验时应用木头做一个半圆人头模型，将试验的安全帽内缓冲弹性带系好放在模型上。各种材料制成的安全帽试验都可用此方法。二安全带：安全带的检验周期为：每次使用安全带之前，必须进行认真的检查。对新安全带使用两年后进行抽查试验，旧安全带每隔6个月进行一次抽检。国家规定，出厂试验是取荷重120kg的物体，从2～2.8m高架上冲击安全带，各部件无损伤即为合格。一些施工单位经常使用的方法是：采用麻袋，由装木屑刨花等作填充物，再加铁块，以达到试验负荷的重的标准。用专作实验的架子，进行动、静荷重试验。施工单位可根据实际情况，在满足试验负荷重标准情况下，因地制宜采取一些切实可行的办法。锦纶安全带配件极限拉力指标为：腰带1200～1500kg，背带700～1000kg，安全绳1500kg，挂钩圆环1200kg，固定卡子60kg，腿带700kg。安全带的负荷试验要求是：施工单位对安全带应定期进行静负荷试验。试验荷重为225kg，吊挂5min，检查是否变形、破裂等情况，并做好记录。需要注意的是，凡是做过试验的安全护具，不准再用。第 2 页共 4 页

三个人防护用品的检查还必须注意： 1产品是否有生产许可证单位生产的产品； 2产品是否有产品合格证书； 3产品是否满足该产品的有关质量要求； 4产品的规格及技术性能是否与作业的防护要求吻合。第 3 页共 4 页

认知结构知识模型理论

认知结构知识模型理论什么是认知结构知识模型理论认知结构知识模型理论是范丰会和宋文红在其新书《新视界心理学——认知结构知识模型理论及其在学科教学、心理咨询和学习心理障碍辅导中的应用》中提出来的一个关于西方心理学的新理论体系。作者试图通过这一理论模型解决西方心理学“像灌木丛一样，流派林立、各说各话、相互矛盾”的现状，尝试进行西方心理学学科内综合，以便提高西方心理学对理论精华的继承性，更有效地发挥其在实践中的指导作用。认知结构知识模型理论提出者简介范丰会，物理学科教育学硕士、心理咨询师。1990年获首都师范大学物理系基础物理教育学硕士。曾从事过中学物理教学、中学教师继续教育、教育软件及教学资源开发、心理咨询、学习困难学生辅导、家长培训等工作。1990年完成硕士论文《大学生物理认知结构的定量研究》，之后工作28年来，对心理学基础理论、心理的发生发展、学科教学、学习心理障碍等相关领域的基础理论问题和重要实践问题进行了不懈的探索，颇有心得。宋文红，1991年毕业于北京医科大学临床医学专业，从事儿科临床工作。2008年在北京大学第六附属医院进行精神科研究生课程，之后进入儿童保健和儿童心理专业，对儿童各类常见病、儿童发育性行为问题及儿童情绪行为障碍有丰富的诊疗经验。认知结构知识模型理论形成过程在《新视界心理学》一书中，作者从批评西方心理学各流派心理观和方法论缺陷出发，借鉴20世纪物理学的科学观和方法论成果，确立了指导心理学理论探索的心理观和方法论；在此基础上，秉持心理结构化和建构论的观点，沿着“用知识描述心理”的思路，创新提出了基于“认知结构知识模型”的基本理论框架；然后在这一理论框架基础上，继承各主流心理学流派的理论成果，融合形成了认知结构知识模型理论。根据这一理论，现行西方心理学主要流派和主要应用领域的问题都可以用一套基本范式进行解释，从而初步实现了对心理学各流派理论的综合与创新。认知结构知识模型理论的主要内容认知结构知识模型理论主要包括以下内容： 1．意识和潜意识共同构成心理活动的容器或空间。 2．用认知结构作为描述整体心理（包括意识和潜意识）结构的基本概念。认知结构是由陈述性知识、意象、程序性知识和策略性知识四种知识构成的网络化结构。 3．认知结构网络可以进一步划分为由以上四类知识构成的、相互依存的两层网络——认知结构潜网和认知结构显网。认知结构潜网是在由遗传获得的“原始意象-本能”结构基础上于人类幼年期逐渐建构并在6、7岁基本完成的“意象-程序性知识”结构，其基本作用模式是象征性思维，即以情绪感受为依据，通过同化、泛化和顺应而建构知识经验并作用于环境，如同所有哺乳动物的学习和适应方式一样；认知结构显网的构建是在人类抽象逻辑思维出现时开始的，是在认知结构潜网基础上建构起来的“陈述性知识-意象-程序性知识-策略性知识”结构，其基本作用模式是抽象逻辑思维，即以陈述性知识为核心、以抽象逻辑思维为主导进行的同化和顺应过程。通俗地讲，潜网、潜意识、象征性思维是“讲情”的；而显网、意识、逻辑思维是“讲理”的。双网融合、和谐一致、具备充分的环境适应性是一个心理发展良好人（人本主义心理学家所称“自我实现者”）的认知结构特征；否则，可能会产生各种内部冲突性和外部适应性心理问题。 4．认知结构有四种发展机制：同化、顺应、条件反射和整合。其中同化与顺应是从皮亚杰等理论引进。条件反射作用来源于行为主义的经典发现，在认知结构知识模型理论中作为潜意识学习规律，可以解释潜意识情结和行为习惯形成的原因。整合（类似于精神分析所

Web服务组合技术框架及其研究进展

第17卷第2期计算机集成制造系统 Vol.17No.22011年2月 Computer Integrated Manufacturing Systems Feb.2011 文章编号:1006-5911(2011)02-0404-09 收稿日期:2009 10 13;修订日期:2010 08 25。Received 13Oct.2009;accepted 25Aug.2010. 基金项目:国家自然科学基金资助项目(60803004);国家863计划资助项目(2009AA01Z121);浙江省科技计划资助项目(2009C31109);浙江省教育厅科研资助项目(Y200909534)。Founda tion items:Project sup ported by th e National Natu ral Science Foundation,China(No.60803004),the National H igh T ech.R&D Program,Ch ina(No.2009AA01Z121),the S cien ce &T echnology Plan of Zhejiang Province,China(No.2009C31109),and th e Education Bureau Research Foun dation of Zhejiang Province,Chin a(No.Y200909534). Web 服务组合技术框架及其研究进展邓水光,黄龙涛,尹建伟,李莹,吴健 (浙江大学计算机科学与技术学院,浙江杭州 310027) 摘要:为了研究Web 服务组合技术,以促使服务计算从概念走向应用,提出了Web 服务组合的技术框架,该框架涵盖了服务组合过程涉及的主要关键技术。讨论了该研究框架中的服务发现、服务组合、服务验证三大关键问题,对当前国内外的主要方法和研究成果进行了分类和比较。最后指出了服务组合面临的问题和未来的发展方向。关键词:W eb 服务;面向服务的计算;服务发现;服务组合;服务验证中图分类号:T P393 文献标志码:A Technical framework for Web Services composition and its progress D EN G Shui guang ,H UA N G Long tao,YI N J ian wei ,LI Ying,W U J ian (Co llege of Com puter Science &T echno lo gy ,Zhejiang U niver sity,Hang zhou 310027,China) Abstract:T o study W eb Serv ices co mpo sitio n techno lo gy ,so as to push serv ice co mputatio n into application,a kind of technical fr amewo rk fo r Web Ser vices composition w as pr oposed.Some key issues w ithin this framew or k,such as ser vice discover y,ser vice composit ion methods and service ver ificatio n,w ere discussed.Its r esear ch prog ress w as also intr oduced.F inally,o pen issues and future dir ect ions wer e po int ed out. Key words:W eb Ser vices;serv ice or iented computing;ser vice discover y;ser vice composit ion;ser vice ver ification 1 问题的提出如何解决企业应用随需应变是当今软件产业的焦点问题,而面向服务的计算(Ser vice Oriented Co mputing ,SOC)正是为解决这一问题而提出来的一种新的计算方式,其核心思想在于以服务为基本单位,通过服务组合快速构建松耦合的分布式应用系统[1]。Web 服务的不断成熟和发展为SOC 提供了最佳支撑技术,在这一背景下,Web 服务组合的研究被提上日程,并迅速吸引了国内外学者的关注[2]。 Web 服务组合是将若干服务按照一定的业务逻辑进行组装形成组合服务,并通过执行该组合服务而达到业务目标的过程。该过程涉及了众多关键问题,本文将这些问题归纳成如图1所示的Web 服务组合技术框架。根据Web 服务组合的生命周期,该研究框架所覆盖的问题可被划分为两大类:服务组合建立时问题和服务组合运行时问题。前者主要包含了服务发现、服务合成、服务组合描述和服务组合验证等问题,后者包含了服务组合执行与监控、服务组合的安全与事务管理等问题。由于服务组合的执行监控与工作流相似,专门研究这一问题的文献并不多见。此外,Web 服务本身的安全与事务研究刚刚起步,也鲜见于国内外文献中。因此,本文重在探索服务组合建立时问题的研究现状。鉴于已有学者对Web 服务组合建模语言进行了综述[3],本文着重介绍服务发现方法、服务组合方法和服务验证方法的研究进展。

安全防护用具检验方法范本

工作行为规范系列安全防护用具检验方法（标准、完整、实用、可修改）

编号：FS-QG-13627安全防护用具检验方法 Inspection method of safety protective equipment 说明：为规范化、制度化和统一化作业行为，使人员管理工作有章可循，提高工作效率和责任感、归属感，特此编写。个人安全防护用品常用的安全护具安全鞋，劳保鞋，防静电鞋，绝缘鞋，防护服等等必须认真进行检查、试验。安全网是否有杂物，是否被坠物损坏或被吊装物撞坏。安全帽被物体击打后，是否有裂纹等。经常对安全护具的检查按要求进行一安全帽:检验周期为每年一次。3kg重的钢球，从5m 高处垂直自由坠落冲击下不被破坏，试验时应用木头做一个半圆人头模型，将试验的安全帽内缓冲弹性带系好放在模型上。各种材料制成的安全帽试验都可用此方法。二安全带:安全带的检验周期为:每次使用安全带之前，必须进行认真的检查。对新安全带使用两年后进行抽查试验，旧安全带每隔6个月进行一次抽检。国家规定，出厂试验是取荷重120kg的物体，从2~2.8m

高架上冲击安全带，各部件无损伤即为合格。一些施工单位经常使用的方法是:采用麻袋，由装木屑刨花等作填充物，再加铁块，以达到试验负荷的重的标准。用专作实验的架子，进行动、静荷重试验。施工单位可根据实际情况，在满足试验负荷重标准情况下，因地制宜采取一些切实可行的办法。锦纶安全带配件极限拉力指标为:腰带1200~1500kg，背带700~1000kg，安全绳1500kg，挂钩圆环1200kg，固定卡子60kg，腿带700kg。安全带的负荷试验要求是:施工单位对安全带应定期进行静负荷试验。试验荷重为225kg，吊挂5min，检查是否变形、破裂等情况，并做好记录。需要注意的是，凡是做过试验的安全护具，不准再用。三个人防护用品的检查还必须注意: 1产品是否有“生产许可证”单位生产的产品; 2产品是否有“产品合格证书”; 3产品是否满足该产品的有关质量要求; 4产品的规格及技术性能是否与作业的防护要求吻合。请输入您公司的名字 Foonshion Design Co., Ltd

几种信息安全评估模型知识讲解

1基于安全相似域的风险评估模型本文从评估实体安全属性的相似性出发,提出安全相似域的概念,并在此基础上建立起一种网络风险评估模型SSD-REM 风险评估模型主要分为评估操作模型和风险分析模型。评估操作模型着重为评估过程建立模型,以指导评估的操作规程,安全评估机构通常都有自己的操作模型以增强评估的可实施性和一致性。风险分析模型可概括为两大类:面向入侵的模型和面向对象的模型。面向入侵的风险分析模型受技术和规模方面的影响较大,不易规范,但操作性强。面向对象的分析模型规范性强,有利于持续评估的执行,但文档管理工作较多,不便于中小企业的执行。针对上述问题,本文从主机安全特征的相似性及网络主体安全的相关性视角出发,提出基于安全相似域的网络风险评估模型SSD-REM(security-similar-domain based riskevaluation model)。该模型将粗粒度与细粒度评估相结合,既注重宏观上的把握,又不失对网络实体安全状况的个别考察,有助于安全管理员发现保护的重点,提高安全保护策略的针对性和有效性。 SSD-REM模型 SSD-REM模型将静态评估与动态评估相结合,考虑到影响系统安全的三个主要因素,较全面地考察了系统的安全。定义1评估对象。从风险评估的视角出发, 评估对象是信息系统中信息载体的集合。根据抽象层次的不同,评估对象可分为评估实体、安全相似域和评估网络。定义2独立风险值。独立风险值是在不考虑评估对象之间相互影响的情形下,对某对象进行评定所得出的风险,记为RS。定义3综合风险值。综合风险值是在考虑同其发生关联的对象对其安全影响的情况下,对某对象进行评定所得出的风险,记为RI。独立域风险是在不考虑各评估实体安全关联的情况下,所得相似域的风险。独立网络风险是在不考虑外界威胁及各相似域之间安全关联的情况下,所得的网络风险评估实体是评估网络的基本组成元素,通常立的主机、服务器等。我们以下面的向量来描述{ID,Ai,RS,RI,P,μ} 式中ID是评估实体标识;Ai为安全相似识;RS为该实体的独立风险值;RI为该实体合风险值;P为该实体的信息保护等级,即信产的重要性度量;属性μ为该实体对其所属的域的隶属

用卡诺模型分析用户体验

用卡诺模型分析用户体验本文主要讨论的是如何以卡诺模型为基础去理解用户体验，并且给出一些实际的例子来加以说明。昨天和陈总等一干人等去吃以服务或者更加确切地说是用户体验出名的海底捞火锅，吃完之后，几位没吃过海底捞的海鳖那是“当场就震惊了”，以这个为引子，我想用顾客满意度的经典模型归纳一下我对用户体验的一些理解。卡诺模型是我很推崇的一个简单又优雅的模型，它由日本质量学家卡诺提出，用于评价和规划顾客满意度和产品质量。其大致含义是，一件产品的质量包括四个维度（dimension），如下：首先是必需质量，就是它傻逼产品就一定傻逼，它牛逼了产品也不牛逼。比如说火锅一定得有牛肉，手机一定得能打电话，要找老婆你得一定是个男银一样。满足用户在这个维度上的需求是必须的，无可逃避的。然后是一维质量，简单说一维质量就是它傻逼产品就傻逼，它牛逼产品就牛逼。比如火锅店羊肉越便宜越爽，上网的速度越快用户就越爽，硬盘越大也就越爽，男人越持久也就…… 然后是魅力质量，就是没有它产品不会变傻逼，但是有了它产品立马牛逼。比如海底捞等桌的时候居然可以做美甲下跳棋，ipod touch管理音乐专辑时居然可以cover flow，你刚买回来的硬盘居然存满了日本爱情动作片，单身滴那男人居然有个美西名校mba学位…… 最后是无差质量，就是有没有它对产品完全没影响。比如山寨机它可以刮胡子，火锅店厕所下水道管道的质量…… 卡诺模型可以用以下二维坐标图表示：

kano model 好，以上是文献综述阶段。必须指出的是，几个质量维度之间是可以相互转化的。举个例子，电视机刚发明的时候，没人想到需要个遥控器，这时候它是无差质量，随后有人觉得睡着看电视的时候老要从被子里面爬出来去按换台按钮很不爽，于是他拿一根棍去点按钮，更加聪明的人就发明了遥控器，作为一个新颖功能。这时遥控器就变成了魅力质量，随着大家都开始偷懒，越来越多的厂家加入遥控器，这时候有遥控器的电视是高端的，没有的是低端的，于是变成了一维质量。最后大家都觉得遥控器是理所当然的必需质量，要是你买的电视没遥控器你怎么想? 这里先提出实现伟大用户体验的公式：伟大用户体验 = 被满足的必须质量 + 好（但不必是伟大的）一维质量 + 一些闪光的魅力品质。一些这个公式的推论或者说支持这个公式的事实是：蹩脚的产品偏离用户需求，好的产品满足用户需求，伟大产品创造用户需求虽然这已经是老调重弹无数次了，不过用卡诺模型解释，用户表达出来的需求只是必须质量和一维质量，那么如果得不到满足，产品必然是失败的。然而魅力品质，恰恰是用户无法直接张口要求的那些未知需求。比如福特说“如果我去问消费者他们要什么，他们肯定说一匹跑得更快的马”。在iPhone出现之前，没有用户会告诉你想在手机上放大图片可以用两根手指直接展开，他们只会告诉你，喔，我要一个放大按钮和一个缩小按钮。

何为服务组合

服务组合综述近年来，随着Web服务相关标准的持续完善和支持Web 服务的企业级软件平台的不断成熟，越来越多的稳定易用Web服务共享在网络上。然而单个Web服务的功能有限，难以满足实际应用中的多种多样的需求，因此为了更加充分地利用共享的Web服务，有必要将共享的Web服务组合起来，提供功能更为强大的服务。Web服务组合的研究正是在这种背景下被提出来，并吸引了工业界和学术界的广泛关注。 1. 基本概念 1.1 Web服务 Web 服务是基于网络的、分布式的、自描述的、模块化的组件, 它执行特定的任务, 遵循一定的技术规范, 提供了面向Internet应用的统一服务发布、发现、调用和合成机制。现在它已经成为广域环境下实现互操作的一种主要机制, 得到产业界和学术界的广泛认可。1.2 Web服务组合由于目前尚未有统一的定义，不同的研究人员从不同的角度对Web 服务组合问题进行定义。我们对 Web服务组合提出一个更为通用和完整的定义：利用Internet上分布的现有Web服务，根据用户的应用需求，把相对简单的服务按照一定的逻辑方式组合起来，从而组合成更强大、更完整的服务的过程。Web服务组合可以利用较小的、较简单的、且易于执行的轻量级服务来创建功能更为丰富、更易于用户定制的复杂服务，从而能够将松散耦合的、分散在Internet上的各类相关 Web服务有机地组织成一个更为可用的系统，支持企业内、外部的企业应用集成和电子商务等网络应用。 Web 服务组合方法从组合方案生成方式来分有两大类：静态组合和动态组合。静态组合意味着请求者应在组合计划实施前就创建一个抽象的过程模型。抽象的过程模型包括任务的集合以及任务间的数据依赖关系, 每个任务包含一个查询的子句, 用来查找完成任务的真正的Web 服务。而动态组合不仅自动地选择、绑定Web 服务, 同时更重要的是自动地创建过程模型。 2. Web服务相关技术 Web服务的主要思想，就是未来的应用将由一组应用了网络的服务组合而成，只要求两个等同的服务使用统一标准和方法描述自己；Web服务另外一个重要的思想就是：所有东西

服务质量模型分析

对医疗行业的服务系统模型和服务场景模型分析 ——以重庆第七人民医院为案例作者：谭云升重庆理工大学市场营销一．服务系统模型阐述服务系统模型是关系营销中一个重要的知识内容，主要阐述了企业与顾客互动的重要性，并且在该模型中揭示了企业如何在实践中与顾客进行互动，互动需要企业内部的哪些支持，并分析了顾客期望的来源。首先，从企业方面讲，需要界定企业使命，然后以此来确定服务概念。有了如上两步，接着才规划支持部分和互动部分。 1.支持部分。（1）管理支持。这是最主要的，主要是指企业的管理者应该支持他们的员工，建立一种以顾客为导向的服务组织。（2）物质支持。这是一种有形的支持，与顾客直接接触的员工往往依赖于这些物质支持提供服务。（3）系统支持。这是指在技术、系统方面的支持，通过这些系统，保证员工方便的为顾客提供个性化的服务。 2.互动部分互动部分实际上是讲在互动接触中涉及的一切资源，包括人力、物力、系统资源。包括：（1）参与到服务中的顾客，企业必须将顾客作为一种重要的资源进行管理，而不是把他们视为被动的服务接收者。（2）与顾客接触员工。他们是服务提供者最关键的资源。（3）系统和运营资源。这包括由系统和规章构成的和所有的运营和行政体系，直接影响顾客感知，又约束员工有内在影响。（4）有形资源和设备。它们对功能质量产生影响。其次，从顾客方面说，由于顾客价值生成体系的存在，导致期望的产生，于是希望与服务企业产生互动。基于此，服务系统模型就构成了。服务提供者应该提供良好的支持服务和互动满足顾客期望，与顾客互动，解决顾客的问题。二．服务场景模型阐述众所周知，顾客实际经历的服务质量包括三个方面：what、how、where。那么，服务场景就是第三个因素where，服务场景的好坏会影响顾客感知服务质量。其模型如下：

2009 类比推理的认知过程与计算模型

类比推理的认知过程与计算模型Ξ 罗　蓉　胡竹菁 (江西师范大学心理学院,南昌330022) 摘　要:该文主要论述了类比推理的认知过程及其计算模型。文章对类比推理的概念进行了分析,论述了类比推理的主要成分和认知过程,并进一步围绕类比推理的重要成分介绍了当前类比推理的主要实证研究及研究成果,在此基础上文章进一步概括了类比推理的主要计算模型。关键词:类比;类比推理;认知过程;计算模型中图分类号:B842.5 文献标识码:A 文章编号:1003-5184(2009)06-0042-09 1　类比和类比推理的概念类比推理亦称类比或类推。“类”是中国古代逻辑思想中一个重要概念,有“本质”、“规律”等意义,具有相同本质、规律的事物为同类,反之为异类。类推,在中国古代,是逻辑推理的统称,指依据类的同异关系所进行的推理[1]。在逻辑学中,类比就是类比推理,或者可以把类比理解为类比推理的简称。在许多逻辑学著作中,类比推理被看成是一种特殊的归纳推理。类比推理在逻辑学中,通常被定义为:“它是根据两个(或两类)对象在一系列属性上是相同(相似)的,而且已知其中的一个对象还具有其他特定属性,由此推出另一个对象也具有同样的其他特定属性的结论”[2]。这一定义流传较广,但仔细分析,该定义侧重于物体表面属性的比较,强调属性的推移。有心理学者认为,逻辑学一般对类比的意义估计不足,对类比推理描述肤浅,一般认为自然科学比较重视类比推理的重要意义。在认知心理学领域,类比既可以被看作是推理的一种类型,也被认为是知觉的一种。把它看成是推理的一种类型的观点认为,类比存在于知识从一种情境(称为源或基础物)迁移至另一情境(称之为目标),迁移的依据是在两个情境间有着某种相似性,如关于手头任务的判断两种情境在本质上是同样的。这是当前关于类比的主导观点[3-5]。 G entner认为,类比就是关系结构从一个领域到另一个领域的复制[3]。她进一步阐述,类比即是1)在不同的领域或系统中相同的关系中存在相似;2)由此推论如果两物体在某些方面有着一致性,那么它们在其他方面也可能一致[6]。 H oly oak指出,类比是一种特殊的相似。记忆中已有的问题、概念或情境称为“源”,当前的问题、概念或情境称为“目标”。两个情境如果它们在其构成要素中享有关系的共同模式,它们就是类似的,尽管这些要素跨越了两个不同的情境而不同。典型地,一个类比物(“源”或“基础物”)比第二个类比物(“目标”或”靶”)更熟悉或更好理解。最初知识中的这种不对称性提供了类比迁移的基础,用源产生关于目标的推论[7]。类比也被认为是一种高水平知觉,在这种情况下,一种情境被知觉为另一个[8]。K okinov认为,这两方面的观点是相关的并且也是重要的,因而类比可以被认为是推理和知觉间的桥梁,在人类认知的核心中扮演着一个特殊的角色[9]。 G oswami认为,类比推理是人类认知发展的中心能力之一,它不仅在分类和学习中涉及到,而且为人类思维和解析提供了一种方法,它对科学发现和创造性思维都有十分重要的作用。在认知心理学中类比推理的基础地位已被广泛接受,在概念结构的本质、创造性问题的解决,以及人工智能等领域都成为研究的焦点[10]。 G enter指出[6,11],类比在认知科学中既普遍又重要。她认为:首先,在学习研究中,类比使得迁移跨越不同的概念、情境或领域,并被用来解释新主题。(先前知识)一旦被习得,它们就能被作为心智模型(mental m odels)以理解一个新的领域。比如,人们通常使用水流的类比来理解电流。第二,类比通常被用在问题解决和归纳推理中,因为它们能跨越第29卷总第114期心理学探新 PSY CH O LOGIC A L EXP LORATI ON 2009年第6期 Ξ基金项目:2008江西省高校人文社会科学研究一类项目《类比推理的发展理论研究》。通讯作者:胡竹菁,E2mail:huzjing@https://www.wendangku.net/doc/d814626218.html,。

模型认知和认知模型

模型认知和认知模型认知结构的激活扩散模型认知结构的激活扩散模型也是一个网络模型。但与层次网络模型不同，它放弃了概念的层次结构，而以语义联系或语义相似性将概念组织起来，如图2-5所示。概念之间的连线表示它们的联系，连线的长短表示联系的紧密程度，连线愈短，表明两个概念有愈多的共同特征。这样的语义记忆结构无疑不同于逻辑层次结构，但它本身并不排除概念的逻辑层次关系，如“机动车”是“小汽车”和“卡车”等的上级概念，有连线相通。然而，概念之间有更多的横向联系。“小汽车”还与“卡车”、“公共汽车”、“急救车”等机动车有联系。激活扩散模型的加工过程是很有特色的。当一个概念被加工或受到刺激，在该概念结点就产激活，然后激活沿该结点的各个连结，同时向四周扩散，先扩散到与之直接相连的结点，再扩散到其他结点。前面提到概念间的连线按语义联系的紧密程度而有长短之分，现在连线则又有强弱之别。连线的不同强度依赖于其使用频率的高低，使用频率高的连线有较高强度。由于激活是沿不同一的连线扩散的，当不同来源的激活在某一个结点交叉，而该结点从不同来源得到的激活的总和达到活动阈限时，产生这种交叉的网络通路就受到评价。例如，对野鸭是鸟”作出判断，就需要进行搜索，来收集足够的肯定和否定的证据。当在“野鸭”

和“鸭”之间找到上下级连线，又在“鸭”和“鸟”之间找到上下级连线，就得到足够的肯定证据对“野鸭是鸟”作出肯定判断。激活扩散模型的信息提取机制是相当复杂的。它与层次网络模型不同。层次网络模型只包含搜索过程，而激活扩散模型则包含两种过程，除搜索过程以外，还有决策过程。这种决策过程也可看作计算。从激活扩散模型我们可以看出，知识的保持不仅与知识的组织程度有关，而且还与知识的运用频率和信息加工过程的决策计算有关。认知心理学对知识的研究结果也表明，由于不同的识记方式导致对识记内容加工深度也有所不同，对新知识信息加工愈充分，识记效果越好。例如，博布罗和鲍尔曾要求被试记一些简单的“主一谓一宾”结构的句子。在第一条件下，被试记忆由实验者提供的现成的句子，在第二种条件下，被试自己用句子中的主语和宾语名词另造句子，测验要求是给被试提示主语，要求他们回忆出宾语名词。结果发现，第一种条件下的回忆率为29%，第二种为58%。这种显著的差异在于精心加工的水平不同。以上的认知心理学研究结果表明，将新知识纳入认知结构，不仅需要按逻辑层次进行组织，而且需要对知识进行必要的精心加工。这样的应用结束技能时应注意对新获得的知识进行应用。由于新知识的结论往往是通过几个典型事例得出的，还不够稳固，需要将它应用到所属类中的其他事例中，通过应用加强同类

认知语言学中的意象图式理论

认知语言学中的意象图式理论一、意象图式的含义与理论基础意象图式(ImageSchema)是认知模型理论中的一个非常重要的概念，研究意象图式对于研究人们如何建构范畴、形成概念、分析隐喻、理解意义、实行推理等过程具有重要意义。意象和图式原是两个独立的概念。18世纪时康德讨论了图式的哲学意义，他认为图式是“连接感知和概念的纽带，是建立概念与物体之间联系的手段，也是建构意象、制造意义的必要程序，个体共有的想象结构”(王寅，2007：172)。而意象常被视作是一个心理学的术语，指代一种心理表征，即人们在看不到某物时却仍然能够想象出该物体的形象和特点，而这正是在没有任何外界事物提示的情况下，人们仍然能在心智中猎取这个事物的印象的一种认知水平。 Lakoff和Johnson(1987)首次提出了意象图式这个概念。他们将它定义为：意象图式是感知互动和运动活动中的持续再现的动态模式，这个结构给我们的经验以连贯性和结构性。(Johnson，1987：xiv)Gibbs 和Colston(1995)描述意象图式为空间关系以及空间中运动的动态模拟表征，而Oakley(2004)认为它则是为了把空间结构映射到概念结构而对感性经验实行的压缩性的再描写。(李福印，2007：81)认知语言学家们赞同意象图式是基于人们的感知和体验的，并且先于人类语言。换言之，“现实—认知—语言”是认知语言学的一条基本原理，并且认知过程包括：互动体验、意象图式、范畴化、概念化、意义等过程。所以，意象图式只不过是认知过程中的一个细节。认知语言学的哲学基础是体验哲学，即“经验是在我们持续通过与变化的环境互动之中产生意义的体验性感知运动和认知结构的结果”(王寅，2007：37)，其心理学基础是皮亚杰的建构论和互动论。所以，意象图式也是基于体验，与现实世界互动，并抽象出来的一种形而上的结构。二、意象图式的类型

Web服务组合综述

Web服务组合综述【摘要】近年来，Web服务技术作为服务计算（SOC）和面向服务架构（SOA）的主要实现技术，已经得到广泛应用，工业界和学术界分别从不同的角度对Web 服务的相关技术展开研究。本文详细阐述了服务组合的概念、框架和分类，分析了几种常用的Web服务组合方法，并对这几种组合方法作了比较，最后，对Web 服务组合方法进行了总结。【关键词】Web服务；组合方法；服务组合；工作流 1.引言近年来，电子商务的迅速发展，使得基于网络的、分布式的、模块化的Web 服务技术得到快速发展和广泛应用，Web服务遵循一定的技术规范，执行一定的任务。随着Web服务标准的持续完善和支持Web服务的企业级软件平台的不断成熟，越来越多的企业和商业组织参与到软件服务化（SaaS）的行列中来，纷纷将其业务功能和组件包装成标准的Web服务发布出去，实现快速便捷地寻求合作伙伴，挖掘潜在的客户和达到业务增值的目的[1]。然而，目前网络上发布的服务大多数都存在结构简单、功能单一的缺陷，无法满足企业复杂应用的需求。如何有效地组合分布于网络中的各种服务，实现服务之间的无缝集成，形成功能强大的企业级服务流程以完成企业的商业目标，已经成为Web服务发展过程中的一个重要步骤，也是SOC与SOA能否成功应用和实施的关键[2]。 2.Web服务基本概念 Web服务组合源于软件重用.其基本思想是使用现有的Web服务，通过它们一定顺序的组合或组合顺序的改变，创建出新的或更高质量的服务满足用户的需求。 2.1 Web服务概念目前对Web服务组合尚无统一的定义，很多研究者从不同的角度和侧重点对Web服务组合给出了不同的定义。[3] 对Web服务组合定义是指由多个小粒度的Web服务相互之间通信和协作来实现大粒度的服务功能；通过有效地联合各种不同功能的Web服务，服务开发者可以借此解决较为复杂的问题，实现增值服务。 IBM对服务组合定义[4]是满足业务流程逻辑的一组Web服务，通过制定不同Web服务执行顺序和交互过程来实现新的业务功能。[5] 从两个不同的研究角度对Web服务组合进行了定义：（1）基于过程模型：从WSC内在因素的角度，将其定义为一个依赖于特定控制流和数据流结合起来的、能够完成一定任务的Web服务集合。（2）基于构件单元：从构件的角度，将WSC定义为一个由自治且能相互协作的自描述单元所组成的系统。文献[1]提出了一个更为通用和完整的Web服务组合定义：用现有的分散的、小粒度的原子服务，根据服务请求者的需求，在某一特定的Web服务组合框架下，自动地选择满足需要的若干服务，并使它们按照一定的组合规则协同工作完成服务请求。 2.2 Web服务组合架构典型的Web服务组合（WSC）的实现框架包括2种用户角色（服务请求者和服务提供者）和5个部件（翻译器、组合管理器、执行引擎、服务匹配器和服务库），可选部件本体库为服务描述提供本体定义和推理支持，如图1所示。WSC

模型检验(闵应骅)

模型检验（1）（091230）大家承认，计算机领域的ACM图灵奖相当于自然科学的诺贝尔奖。2007年图灵奖授予Edmund M. Clarke，E. Allen Emerson,和Joseph Sifakis。他们创立了模型检验---一种验证技术，用算法的方式确定一个硬件或软件设计是否满足用时态逻辑表述的形式规范。如果不能满足，则提供反例。他们在1981年提出这个方法，经过28年的发展，已经在VLSI电路、通信协议、软件设备驱动器、实时嵌入式系统和安全算法的验证方面得到了实际应用。相应的商业工具也已出现，估计今后将对未来的硬件和软件产业产生重大影响。 2009年11月CACM发表了三位对模型检验的新的诠释。本人将用几次对他们的诠释做一个通俗的介绍，对我自己也是一个学习的过程。 Edmund M. Clarke现在是美国卡内基梅隆大学（CMU）计算机科学系教授。E. Allen Emerson 是在美国奥斯汀的德州大学计算机科学系教授。Joseph Sifakis是法国国家科学研究中心研究员，Verimag实验室的创立者。模型检验（2）（091231）程序正确性的形式验证依靠数学逻辑的使用。程序是一个很好定义了的、可能很复杂、直观上不好理解的行为。而数学逻辑能精确地描述这些行为。过去，人们倾向于正确性的形式证明。而模型检验回避了这种证明。在上世纪60年代，流行的是佛洛伊德-霍尔式的演绎验证。这种办法像手动证明一样，使用公理和推论规则，比较困难，而且要求人的独创性。一个很短的程序也许需要很长的一个证明。不搞程序正确性证明，可以使用时态逻辑，一种按时间描述逻辑值变化的形式化。如果一个程序可以用时态逻辑来指定，那它就可以用有限自动机来实现。模型检验就是去检验一个有限状态图是否是一个时态逻辑规范的一个模型。对于正在运行的并发程序，它们一般是非确定性的，像硬件电路、微处理器、操作系统、银行网络、通信协议、汽车电子及近代医学设备。时态逻辑所用的基本算子是F（有时），G（总是），X（下一次），U（直到）。现在叫线性时间逻辑（LTL）。