一种基于余代数单子的web服务形式化模型-许碧欢.pdf

《一种基于余代数单子的web服务形式化模型-许碧欢.pdf》由会员分享，可在线阅读，更多相关《一种基于余代数单子的web服务形式化模型-许碧欢.pdf（9页珍藏版）》请在淘文阁 - 分享文档赚钱的网站上搜索。

1、第48卷第5期2016年10月南京航空航天 大学学报Journal of Nanj ing University of Aeronautics&AstronauticsV0148 No50ct2016DOI：1016356j10052615201605009一种基于余代数单子的Web服务形式化模型许碧欢1 钱俊彦2 张迎周3 陈 蕾(1南京邮电大学理学院，南京，210023；2桂林电子科技大学广西可信软件重点实验室，桂林，541004；3南京邮电大学计算机学院，南京，210023)摘要：为拓展服务计算的形式化研究视野、手段和方法，建立并实现了一种针对Web服务的服务计算形式化模型。鉴于开放环境

2、下的服务实体主要来源于不同的第三方提供者，将软件实体抽象成余代数单子，从而以一种黑盒方式给出软件服务的语义模型。给出了余代数单子的一般性定义，在此基础上对软件服务进行单子描述，进而提出一种基于余代数方法和单子技术的Web服务参考模型。最后，实现了一个基于单子的web服务计算平台原型系统，可支持从遗留系统中进行服务抽取、发布、发现和度量等。关键词：服务计算；web服务；单子技术；余代数方法中图分类号：TP311 文献标志码：A 文章编号：10052615(2016)05066809Formal Method of Web Service Based on Coalgebraic MonadsXu

3、 Bihuan 1，Qian Junyan 2，Zhang Yingzhou 3，Chen Lei 3(1College of Science，Nanjing University of Posts and Telecommunications，Nanjing，210023，China；2Guangxi Key Laboratory of Trusted Software，Guilin University of Electronic Technology，Guilin，541004，China；3College of Computer，Nanjing University of Posts

4、and Telecommunications，Nanjing，210023，China)Abstract：To expand the horizons，means and methods of formal studying on service computing，a formalservice computing model for Web service is builtSince a great number of service entities are from different thirdparty providers in open network，software enti

5、ties are abstracted as coalgebraic monads，then a semantic model is given for services in the blackbox methodBased on coalgebraic monads，aformal framework is put forward for serviceoriented computing(SOC)with its applications as wellFinally，a prototype system is implemented for service computing base

6、d on monads，which supports service abstraction，publishing，discovery and metrics from legacy systemsKey words：service computing；Web services；monad technique；coalgebraic method面向服务计算(Serviceoriented computing，SOC)是在现有技术(如面向对象、基于构件的开发、分布式对象计算及Web技术等)基础上，建立了一种基于Internet的软件开发、部署和集成的新模式17|。软件服务的分布性、动态性和自主

7、性等特点，使得面向服务的系统分析、设计、建模和运行等技术仍为目前国内外学者研究热点6。81。关于面向服务计算建模方面，文献9提出了基金项目：国家自然科学基金(61562015)资助项目；广西高等学校高水平创新团队及卓越学者计划资助项目；江苏省“青蓝工程”中青年学术带头人项目资助项目。收稿日期：2016一Ol一01；修订日期：2016-0830通信作者：张迎周，男，教授，E-mail：zhangyznjupteducn。引用格式：许碧欢，钱俊彦，张迎周，等一种基于余代数单子的Web服务形式化模型J南京航空航天大学学报，2016。48(5)：668676Xu Bihuan，Qian Junyan，

8、Zhang Yingzhou，et a1Formal method of web service based on coalgebraic monadsJJournal of Nanjing University of Aeronautics&Astronautics，201 6，48(5)：668676万方数据第5期 许碧欢，等：一种基于余代数单子的Web服务形式化模型 669一种用于设计面向服务体系结构的参考模型，叙述了参考模型的结构以及其中的服务总线和服务合约的元模型。文献10对SOC模型中的约束问题进行了讨论，讨论了约束在服务生成方面的作用。文献11，12充分考虑扭斗对于网络体系结构研

9、究的影响，总结和归纳了在扭斗环境下设计新一代网络体系结构模型的若干原则，在这些设计原则的指导下提出了一种结构分层、功能分面、基于交互、面向服务的新一代网络体系结构模型。文献13基于面向服务的体系结构(Serviceoriented architeture，SOA)给出了一个以企业服务总线为中心的面向服务软件体系架构参考模型。为实现互联网上异种异构的复杂信息资源有序化组织和互操作性服务与共享的目标，文献14研究了语义服务的元计算问题，提出了本体元建模理论和方法，定义了本体UML承诺、提倡本体UML表达，给出了本体的元机制。针对在动态、跨组织的网格环境中如何进行适应组织重构、业务变化等动态性要求，

10、文献E15提出了服务网格动态信息聚合模型，从组织模型、数据模型、协作模型3个维度描述信息聚合中变化的因素。文献16利用代数方法(进程代数)对SOA进行形式化建模，并提出多种SOA可信范式，为基于SOA的可信软件开发提供理论支持。本文将单子17。1钉概念引入服务计算中，从另外一个形式化角度为服务计算建模。基于Web服务的服务计算是面向服务计算的特例，目前Web服务的使用主要是将企业原有信息系统(也称遗留系统)进行封装，通过SOAP、WSDL和UDDI等序列标准发布出来让用户通过网络使用。本文将立足于服务计算的“服务”本质，利用单子技术研究基于Web服务的服务计算形式化模型及其实现：以服务化思想和

11、服务交互观点作为建模基础，以余代数方法和单子技术作为理论基础，建立Web服务的形式化模型，以期大大拓展面向服务计算的形式化研究视野、手段和方法。本文先简介一些基本理论知识，包括余代数方法和单子技术；然后设计和定义一般余代数单子和相应的单子转换器，并给出一种基于单子技术的Web服务参考模型；最后给出Web服务计算平台系统原型的实现。1 余代数方法和单子技术11余代数方法不同于从“构造”角度研究数据结构的代数理论，余代数(coalgebras)20-zz方法从“观察”角度考察系统及其性质，故其对研究诸如对象、进程和服务等基于状态的系统有独特的优越性。使用余代数理论作为工具，可以对系统的行为等价、不

12、确定性等从数学上进行深入探讨，从而为这些系统建立良好的形式理论基础模型，并方便对其性质进行描述与验证2 3|。一般地，对于自函子(endofunctor)T，T-余代数是一个二元组(U，户)，其中对象U称为P的载体，P为UT己，的映射。如果将T-余代数(己，p)看成是一个具有内部状态的系统，则U是其所有可能的状态，映射P：UT【，表示从外部可观察的系统行为，该行为可能会影响系统内部的状态。此外，射P常可分解成几个射，每个射代表系统可观测的一个行为或系统对外部观测的一种响应。更多的有关余代数的基本概念、性质、应用情况参见相关文献(如文献2023等)。Barbosa及其合作者24281曾理论上深入

13、研究了基于余代数的软件构件形式化建模，给出构件的余代数语义表示。他们指出，软件构件的“黑盒特性”比较适合采用观测语义模型：只要通过观察难以区分的任何两个构件(含配置环境)认为是相同的。这样基于状态的任一构件可由以下形式表示：f：UT U其中?U为配置环境中所有可能的状态；T为观测行为、计算结构或构件接口。12单子技术单子技术是一种根据相关类型值及使用这些值的系列计算来构建新计算的方法，其中重要概念包括单子和单子转换器。单子(monad)概念最初是在1950年代作为范畴论里一种函子而被提出的。在1989年由Moggi173将之引入到语义框架中。随后，Wadler1 92鲴将Moggi单子方法广泛

14、推广到函数式程序设计中(尤其是Haskell语言)。采用单子这种更加规则的表示法替代A表示法，可避免定义语义结构时对无关语义成分的引用，从而加强了语义描述的模块性和扩展性。一般地，单子可表示成三元组(M，r，肚)，其中M为某范畴C上的自函子；r：IdM和“：肝一M为其两个基本自然转换函数，且满足如下等式(或称图1是可交换的)：肛。M弘一缈。彬zid胁：MxMx衅o M牲zH工o uMz ：N登IMx其中：z为范畴C中任意对象，id为恒等函数，。为函数复合运算。单子是一种抽象技术，它可隐藏计算时所需的万方数据670 南京航空航天大学学报 第48卷尬!生M1x o丝胁纽一+一胁nluxMx一tx

15、lt图1单子中自然转换函数的可交换图Fig1 Commute diagram of natural transformations基本信息，并提供一些(操作)函数允许外界访问这些信息2 9|。直观上，对于类型a，类型Ma则表示所有能得到口类型结果的计算，这些计算在范畴理论的同态概念下是一致的1 8|。因此，给定一个单子实际上就相当于给定了能够得到某种类型结果的计算类型。目前人们已抽象设计出不少单子，如描述Pi演算的Pi单子3、并发单子口1|、Agent单子3 2|、描述增量计算的可变单子m3等。Ghania等学者3461曾理论说明，余代数演算可以被抽象成一个单子，即余代数单子。Jacobs也曾

16、致力于余代数与单子间关系的理论研究，包括从具体的Java语义表示模型中实例说明余代数表示方法与单子描述方法间的等价性3 7。单子技术中，为了将两个单子结合成一个新单子，引入了单子转换器(monad transformers)383，它将给定单子转换成新单子，并增加新操作运算。目前人们已设计了不少单子转换器，如统一描述与程序环境交互计算的环境单子转换器EnvT，表示与状态相关计算的状态单子转换器StateT等29383 9|。单子具有高度的抽象性、反射性、重用性和模块化，又具有易于自动实现扩充和修改的特点，这些特性对软件体系结构和软件服务技术带来了积极的影响1 9404引。现在，单子已是独立的概

17、念，掌握它不再需要范畴论的知识，而且大量的研究和实践已证实单子系统具有很强的功能，结合单子表示法的简洁性和易读性，因此将为越来越多的人所接受和应用。现已有不少程序设计语言支持实现单子技术，如Haskell、C+4 3|、Java441等。本文采用易于原型开发的函数式语言Haskell作为支持单子相关方法的实现语言。Haskell是一门高级纯函数式编程语言，致力于快速开发可扩展的、可靠的和易维护的软件，并能很好地与其他编程语言集成，具有内建并发性和并行性、调试器、优化器、丰富的类库以及活跃的社区等。在Haskell语言的基本模块Monad中，关于函子、单子和单子转换器分别被定义为：class F

18、unetor f wherefmap：(a一b)一(f a一f b)class Monad m wherereturn：a一m a(一)：m a一(a一m b)一m bclass MonadTrans t wherelift：Monad m一m a一t m a其中单子的类定义中，return和一两个操作函数分别对应于前面提及的两个自然转换函数叩和1。对应于图1，return和一需要满足如下等式(左幺元、右幺元和结合律)2 9|：(return z)一，一f zm一returnm(m=f)一gm一(Axfz一g)这里，Haskell本身不保证单子的两个函数所必须满足的上述3个规律，需其设计者事先

19、保证。2余代数单子在上节所列述的学者研究成果上，尤其是结合Barbosa等基于余代数的构件形式化模型和Ghania等余代数演算的单子抽象表示，本节将这些理论的形式化表示进一步扩展，给出具体程序语言(如Haskell)表示形式，增加交互操作函数，还进一步提升成余代数单子类和余代数单子转换器，进而方便第3节中将之应用到Web服务实际模型描述上。给出如下的一般余代数类型CoAlg：newtype CoAlg f=UnIn UnOut(f(CoAlg f)out：CoAlg f一f(CoAlg f)out(Un0Ut t)一tin：CoAlg f a一ain(UnIn x)一x其中：f为一个表示观测操

20、作的函子；a为任意数据类型；UnIn和UnOut为类型构造函子，分别为CoAlg余代数中映射in和out的逆。即一个余代数类型CoAlg要么是所观测到的内部数据信息(包括初始状态情况)，要么是对系统的进一步观测行为，该行为可能会影响到系统内部数据或状态等。其实，上述定义的余代数(CoAlg f，out)中的CoAlg f也可成为函子和单子。下面的两个Haskell实例声明就使得CoAlg f也是函子，且为单子，其所须满足的单子规律可类似文献4547万方数据第5期 许碧欢，等：一种基于余代数单子的Web服务形式化模型 671中证明方法进行保证。instance Functor f=Functor

21、(CoAlg f)wherefmap f。UnInUnlnffmap fUnout=UnOutfmap(fmap f)instance Functor f=Monad(CoAlg f)wherereturn：=UnInUnln a=k=k aUnout t一kUn0Ut(fmap(一k)t)于是，上述定义的CoAlg f也可称为余代数单子。进一步地，可给出余代数单子类CoAlgMonad，以便对余代数单子与其他单子进行交互转换等。class(Functor f，Monad m)一CoAlgMonad f m whereprj：f(m a)一m ainstance Functor f一CoAlg

22、Monad f(CoAlg f)whereprjUnOut为了与前面所述一致，这里也给出余代数类CoAlgC，并说明上述所定义的类型CoAlg f也是属于余代数类的。class Functor f一CoAlgC f m wherefrom：m一f minstance Functor f=CoAlgC f(CoAlg fa)wherefrom=out为便于余代数单子与其他单子组合的需要，给出如下的余代数单子转换器CoAlgT定义：newtype CoAlgT f m a=CoAlgT(m(Either a(f(CoAlgT f m a)instance(Functor f)一MonadTrans

23、(CoAlgT f)wherelift=CoAlgT1iftM Left其中：Either为“可区分并”联合类型声明，Left为Either类型的投影函数，“”为函数的复合操作，liftM为一般单子间的提升映射函数。有了上述的一般余代数单子和单子转换器定义后，任意的服务可抽象描述成其实例，就可自然表示成该服务的单子和单子转换器，以便进行软件服务单子的描述等。3服务的单子描述为了更好地体现服务的封装性、松散耦合性、可复用性、高度可集成性和开放性等特性，本节试着利用单子技术形式化研究Web服务中服务实体：将服务抽象成余代数单子(服务单子)，通过单子转换器，多个单子可组合成一个新单子，故服务组合可由

24、若干服务单子组合表示。利用上述的一般余代数单子CoAlg f定义，只要具体化服务相关的函子f定义，就可自然描述该服务单子；类似地可利用CoAlgT方便描述该服务的单子转换器。进一步地，利用单子技术，可自然根据服务单子和单子转换器进行相应服务的合成，以便描述相应功能更强的新单子，如增值服务。一般地，对于输入类型为ti输出类型为t。的服务函数serv：tit。，其对应的构件单子(余代数单子)Mserv可定义如下：newtype FservFUN(tin一tout)type MservCoAlg Fservinstance Functor Fserv wherefmap h(FUN f)一FUN(h

25、f)Mserv定义中的Fserv为与服务serv对应的函子，也可简称为serv的服务函子。由前节知，任一余代数单子都属于CoAlgMonad类，故可借助于其prj函数，将serv函数转换到Mserv单子统一描述中：servM：Mserv toutservMprj(fmap returnFUN serv)进一步地，根据上小节的一般余代数单子转换器定义，可定义serv的服务单子转换器MTserv：type MTserv mCoAlgT Fserv m关于上述表示的正确性，主要是要验证上述描述是否满足单子和单子转换器所需规律，因篇幅限制，可借鉴文献4547中证明方法进行验证。为了将系统中各个服务的最

26、后结果再统一描述，给出其统一结果类型ShowOut及其相关的服务调用函数runServ定义：data ShowOut a b=Finished b Result a(ShowOut a b)runServ：M serv tout一tin一Show0Ut tin toutrunServ(UnIn a)b=Finished arunServ(UnOut(FUN f)bResult b(runServ(f b)b)利用runServ调用服务的结果可同时显示输入和输出信息，假设某个服务调用结果为：Result 3(Finished 12)，这表示服务输入为3，服务产生结果为12。万方数据672 南京航

27、空航天大学学报 第48卷4 Web服务的单子模型及其应用通过前一节的服务单子表示方法，服务被抽象成单子(即服务单子)，它可由若干构件单子组合而成。单子技术中的单子转换器不仅可用来组合服务，而且还允许向现有服务单子组合中加入新元素来调整服务以实现相应的Web服务操作。于是，单子转换器可很好描述和处理服务间的交互关系，以此研究Web服务交互行为。根据单子转换器，可方便进行服务间交互操作，如下面的简单例子给出一种servl：t。一。和serv2：t。一t。z两个服务函数组合生成的新服务serv3：t。一。，其操作均在余代数单子统一框架下进行。serv3：tinl一MTservl Mserv2(Sho

28、wOut tinl toutl)serv3 a=dolet b一3c一lift(serv2M b)let d一一一d由a与c相关计算而得e：=runServl servlM dreturn e实际中，服务发布前，可对遗留系统进行服务抽取并进而对其单子描述；而对已发布的Web服务来说，可直接从其WSDL文档中服务操作的类型信息生成相应的单子库，只是其单子框架下服务的实际操作需通过SOAP远程调用完成。例如上述的serv3服务在其发布后的WSDL文档可能的类型为：Int-+IO Int，即serv3操作的结果需要通过SOAP返回，这可由基本输入输出单子IO描述，但最终的Mserv3和MTserv3

29、描述在形式上还是与上述余代数统一定义一致的。由单子的可组合性，服务单子可与表示其他计算特性的单子组合起来，以期最终表示服务实体的某类复杂计算。如服务单子与并发单子组合，所形成的新单子可用来描述建模服务软件的并发行为等。利用余代数方法对研究基于状态系统(如不确定、分布式系统等)的独特优势，可对开放网络环境下的软件服务进行较好的形式化描述。又由单子的抽象性，服务单子可隐藏其计算所需的基本信息，并提供公用接I：1允许外部有限访问服务的内部状态。因单子具有反射性H 0。，故服务单子可以在运行时获知实体内部具体的运行信息，并可访问、修改这些信息，从而使得服务单子本身就具有一定应变调节能力。图2给出了一种

30、基于单子技术的面向服务计算参考模型，主要是针对基于Web服务的服务计算。本文将重点研究图2模型的中间部分，尤其是Web服务实体的形式化表示等。由于单子的抽象性和可扩展性，该参考模型具有较强的可扩展性，现有的有关服务理论分析技术很容易融人到基于单子的软件服务模型中：先将其相关理论抽象成为单子，然后由单子组合理论安全方便地加入到现有的服务实体中，从而可对现有软件服务进行相关理论分析操作。如要利用现有的描述和验证服务组合的Pi演算技术4 8|，可先将其抽象成Pi单子3 0|，再将其组合入所要分析的服务单子中，这样在改动很小的情况下就可对所关注的服务实体进行相应的Pi演算分析操作等。网络通信图2一种基

31、于单子技术的Web服务参考模型Fig2 Web service model based on monads上述所提的Web服务的单子框架模型可直接应用的领域包括：(1)Web服务的形式化语义描述；(2)Web服务自动组合与形式化验证；(3)遗留系统的服务化切分与封装；(4)Web服务自动测试；(5)Web服务的发现等。其优势主要体现在：(1)可在统一的形式化描述框架下进行上述相关工作研究，方便其结果的集成融合；(2)文中所提Web服务的形式化框架模型，可以一种黑盒方式考察研究Web服务操作及其协作行为。利用余代数方法对研究基于状态系统(如不确定、并发系统等)的独特优势，以及单子的抽象性、反射性

32、和可组合性，可很好地对开放网络环境下的构件和服务进行形式化描述和深入研究。关于其在Web服务测试中的应用，文献E49，503中利用单子技术开发了一个Web服务自动测试工具，给出了一个Web服务测试单子，这可融人本文的服务计算单子框架中，以便深入研究Web万方数据第5期 许碧欢，等：一种基于余代数单子的Web服务形式化模型 673服务的自动测试。此外，文献51通过程序切片技术52，提出一种基于函数依赖图的构件抽取方法，进而将之用到服务的抽取、发布和度量等535。又因程序切片这类计算也可被抽象成单子45。475657，结合本文的服务计算单子框架，从而能方便对遗留系统进行服务化切片与封装。上述已有工

33、作虽然没有提及服务的单子模型，但这很容易融入到文中单子框架中(如图2上层所示)，即本文的服务单子模型能为这些相关的服务活动提供相应的单子接口。由于篇幅限制，本文中不再赘述。5 web服务计算平台原型系统针对前面所建立的服务计算单子模型，以及文献sz，5355中对构件抽取、服务生成发布发现度量等方法，文中实现了一个基于Web服务技术的服务计算平台原型系统WS Toolkit，其系统框架图和部分截图分别见图3，4。WS Toolkit是用Haskell58开发的一个实现Web服务框架的原型系统，其中，由HXml来解析ws m，etrics WS discovering图3 Web服务计算平台的系统

34、框架Fig3 System framework of computing platformfor Web service舯a$0LnHlll1)拂靓Fy峨tH图4平台系统原型WSToolkit部分截图Fig4 Some screenshots of platform prototype WToolkit所有的XMI，格式文档，用GTK-广来实现GUI界面。系统功能包括Web服务的生成、组合、发布、发现以及度量。在系统启动时，用户需要选择一个服务的源文件(C、Java或者Haskell)，WS Toolkit会先自动调用gcc和元编译环境ASF+SDF分别对其中C和Java源码分析并生成中间表示

35、结构。然后系统对中间表示信息进行分析，列出源文件中的主要函数(或类等)，此时用户需要指定这些函数中哪些需要被发布成为服务并给出服务的作者，所属公司以及服务描述等信息，再根据这些信息生成WSPD文件。根据WSPD文件中记录的信息，系统接着对源文件进行构件抽取，将要发布成为服务的构件抽取出来，生成切片后的服务代码。同时为每个构件产生相应的单子和单子转换器，并为每个服务生成相应WSDL文档，实现服务的生成。WSDL文档中记录了服务的接口，参数等信息，通过分析WSDL文档，可以对某些服务进行适当的组合并生成新的服务。接着根据WSDL文档可以为每个服务生成tModel和UDDI文档，实现服务的发布。发布

36、服务的同时对服务注册表进行更新，并根据tModel文档记录的依赖关系为服务注册表中的服务生成服务依赖图，根据服务发现的要求对服务依赖图进行切片生成服务依赖子图，对子图进行分析，列出万方数据674 南京航空航天大学学报 第48卷服务发现的结果。系统还可根据服务依赖图和服务依赖子图对发现的服务进行度量。6 结束语由于开放环境下的Web服务实体主要来源于不同的第三方提供者，并且其形成与运行过程常处在一种演化的状态之中，故难以采取传统的过程监控、可控测试、白盒分析等方式保障其可靠性。本文将Web服务系统的服务抽象成余代数单子(称为服务单子)，从而以一种黑盒方式给出服务的语义模型。利用余代数方法对研究基

37、于状态系统(如不确定、并发系统等)的独特优势，以及单子的抽象性、反射性和可组合性，对开放网络环境下的构件和服务进行形式化描述和深入研究，建立并实现了一种服务计算形式化模型框架。上述研究中一个重要观点是将服务和服务的交互行为分别抽象描述成单子技术中的单子和单子转换器，由此可在单子框架下方便形式化研究服务相关性质和活动。与本文形式化研究相似工作有文献16，该文给出了服务的代数定义，并将服务组合解释成服务运算的实现，由此可用进程代数进一步讨论可信SOA的建模问题。不同点在于，文献16从代数语义角度研究服务进而用代数运算解释服务组合等，其抽象层次比较高，有利于服务相关属性的验证等；而本文从另一语义(单

38、子语义)角度探讨服务及其交互组合等，由单子的相关性质可对服务及其相关活动进行较好描述，此外因为单子语义描述具有清晰的操作解释，所以其易于执行实现。例如，本文的服务计算平台原型系统就是利用单子的易于执行性实现的，这便于后续进行服务的生成、发布与发现、组合、服务质量评价、运行等。未来工作包括：进一步完善服务计算的单子模型，并重点关注服务组合的测试和验证、基于QoS的服务质量评测等。参考文献：1Singh M P，Huhns M NServiceoriented computingMChichester：John Wiley&Sons，20052Zoran S，Aiantha DServiceori

39、ented software systern engineering：Challenges and practicesMHershey：Ideal Group Publishing，20053Papazoglou M，Traverso P，Dustdar SServiceoriented computing：State of the art and research ehallengesJIEEE Computer，2007，12(7)：38454Kreger HWeb services conceptual architecture(WSCA 1o)口Ibm Software Group，2

40、001，5：675喻坚，韩燕波面向服务的计算原理和应用M北京：清华大学出版社，2006Yu Jian，Han YanboService-oriented computing-Theory and applicationsMBeijing：Tsinghua University Press，20066蔡维德，白晓颖，陈以农浅谈深析面向服务的软件工程VM北京：清华大学出版社，2008Cai Weide，Bai Xiaoying，Cheng YinongDeep analysis of serviceoriented software engineeringMBeijing：Tsinghua Uni

41、versity Press，200871 白晓颖，赵冲冲，戴桂兰Web服务测试研究J计算机科学，2006，33(2)：252256Bai Xiaoying，Zhao Chongchong，Dai GuilanResearch on web service testingJComputer Science，2006，33(2)：2522568廖军面向服务的计算(SOC)中服务组合的研究D成都：电子科技大学，2006Liao JunThe research on service composition inserviceoriented computingDChengdu：Universityof

42、 Electronic Science and Technology，20069麻志毅，陈泓婕一种面向服务的体系结构参考模型口计算机学报，2006，29(7)：101卜1019Ma Zhiyi，Chen HongjieA serviceoriented architecture reference modelJChinese Journal of Computers，2006，29(7)：1011-1019r 1 OCurbera FComponent contracts in serviceorientedarchitecturesJIEEE Computer，2007，12(7)：7480

43、11杨鹏面向服务的新一代网络体系结构及其形式化建模的研究D，南京：东南大学，2006Yang Peng Research on serviceoriented new generation network architecture and its formal modelingDNanjing：Southeast University，200612杨鹏，吴家皋，网络服务体系结构及其形式化模型研究J计算机研究与发展，2005，42(7)：1115-1122Yang Peng，Wu JiagaoResearch on network servicearchitecture and its form

44、al modelJJournal ofComputer Research and Development，2005，42(7)：1115112213张广胜，蒋昌俊，汤宪飞，等面向服务的企业应用集成系统描述与验证J软件学报，2007，18(12)：30153030Zhang Guangsheng，Jiang Changjun，Tang Xianfei，et a1Specification and verification of service-orientedenterprise application integration systemJJournalof Software，2007，18(

45、12)：3015-303014何克清，何非，李兵，等面向服务的本体元建模理论万方数据第5期 许碧欢，等：一种基于余代数单子的Web服务形式化模型 675与方法研究J计算机学报，2005，28(4)：524533He Keqing，He Fei，Li Bing，et a1Research onserviceoriented ontology&metamodeling theoryand methodologyJChinese Journal of Computers，2005，28(4)：52453315王桂玲，李玉顺，姜进磊，等一种服务网格动态信息聚合模型及其应用J计算机学报，2005，28(

46、4)：541-548Wang Guilin，Li Yushun，Jiang Jinlei，et a1A dynamic information aggregation model and its application in service grid environmentJChinese Journalof Computers，2005，28(4)：54154816赵会群，孙晶面向服务的可信软件体系结构代数模型J2010，33(5)：890899Zhao Huiqun。Sun JingAn algebraic model of service oriented trustworthy sof

47、tware architectureJChinese Journal of Computers，2010，33(5)：8908991 7Moggi EAn abstract view of programming languagesRLFCS Report，ECS-LFCS-90113，198918袁琦Monad理论及其应用研究D吉林：吉林大学，2000Yuan QiResearch on Monad theory and its applicationDJilin：Jilin University，200019Wadler PComprehending monadsJMathematical

48、Structures in Computer Science，1992，2(3)：46149320Rutten JUniversal coalgebra：A theory of systemsJ 1Theoretical Computer Science，2000，249(1)：38021Gumm H PFunctors for coalgebrasJAlgebraUniversalis，2000，45(2-3)：13514722Jacobs BComprehension for coalgebrasJElectronic Notes in Theoretical Computer Science，2002，65(1)：11213423