• 中国计算机学会会刊
  • 中国科技核心期刊
  • 中文核心期刊

计算机工程与科学

• 软件工程 • 上一篇    下一篇

服务组合的代数规约

陈颖1,刘冬梅1,朱鸿2,兰斌1,何娟娟1   

  1. (1.南京理工大学计算机科学与工程学院,江苏 南京 210094;
    2.英国Oxford Brookes大学计算与通信系,英国 牛津 OX33 1HX)
  • 收稿日期:2017-10-11 修回日期:2017-12-17 出版日期:2018-06-25 发布日期:2018-06-25
  • 基金资助:

    国家自然科学基金(61502233,61402229);江苏高校”青蓝工程”;中央高校基本科研业务费专项资金(30916011328);欧盟移动云计算FP7项目MONICA(PIRSESGA2011295222)

Algebraic specifications of service composition

CHEN Ying1,LIU Dongmei1,ZHU Hong2,LAN Bin1,HE Juanjuan1   

  1. (1.School of Computer Science and Engineering,Nanjing University of Science and Technology,Nanjing 210094,China;
    2.Department of Computing and Communication Technologies,Oxford Brookes University,Oxford OX33 1HX,UK)
  • Received:2017-10-11 Revised:2017-12-17 Online:2018-06-25 Published:2018-06-25

摘要:

现有的服务组合描述途径不能有效地验证和测试组合正确性,针对这一问题,提出了一个代数规约方法,引入规约包机制扩展面向服务代数规约语言SOFIA以支持该方法。用代数规约单元描述服务系统中的各种实体,其中基调部分定义实体的语法和结构,公理部分定义其功能和行为特性。与一个服务相关的规约单元封装在一个包中或拆分在几个相互引用的包中,每个包形成一个命名空间。当多个服务组合在一起时,以这些服务的代数规约包为基础,一方面抽象地定义组合服务的交互过程和语义,形成描述服务组合实现方式的实现规约包;另一方面抽象地定义组合服务对外接口及其功能语义,形成描述组合服务需求的抽象规约包。在实现规约和抽象规约的双元结构基础上,进一步定义了实现规约和抽象规约之间必须满足的“实现”关系,证明了满足实现关系可以保证实现的正确性,从而为服务组合的可验证性和可测试性奠定了理论基础。最后结合实例分析阐述了用代数规约描述服务组合的抽象性、可表达性和可验证性。
 
 

关键词: Web服务, 服务组合, 代数规约, 形式化方法

Abstract:

Existing methods for the specification and description of service compositions cannot ensure the correctness of the compositions to be verified and tested. Addressing this problem, we propose an algebraic specification method. A package facility is introduced into the serviceoriented formal specification language SOFIA to support the method. In this approach, various types of entities in a serviceoriented system are specified by a collection of algebraic specification units, and each specifies one type of entities in the system. When multiple services are composited together, based on the algebraic protocol package of these services, on the one hand, the interaction process and semantics of the composite service are abstractly defined so as to form the implementation specification that describes the implementation mode of the service composition. And on the other hand, the external interface and functional semantics of the composite service are abstractly defined so as to form the abstract specification that describes the requirements of the service composition. Based on the dual structure of the implementation specification and the abstract specification, the “implementation” relationship that must be satisfied between the implementation specification and the abstract specification is further defined, and it is proved that satisfying the “implementation” relationship can ensure the correctness of the implementation, thus laying the theoretical foundation of verification and testability of service composition. Finally, a case study demonstrates the abstractness, expressibility and verifiability of using algebraic specification to describe service composition.
 

Key words: web service, service composition, algebraic specification;formal method