Journal of shanghai Jiaotong University (Science) ›› 2014, Vol. 19 ›› Issue (1): 17-27.doi: 10.1007/s12204-014-1472-z

Previous Articles     Next Articles

Behavior-Consistent Service Substitutions in Dynamic Environments

Behavior-Consistent Service Substitutions in Dynamic Environments

CHEN Jun-qing* (陈俊清), HUANG Lin-peng (黄林鹏), YU Cheng-yuan (于程远)   

  1. (Department of Computer Science and Engineering, Shanghai Jiaotong University, Shanghai 200240, China)
  2. (Department of Computer Science and Engineering, Shanghai Jiaotong University, Shanghai 200240, China)
  • Online:2014-01-15 Published:2014-01-15
  • Contact: CHEN Jun-qing (陈俊清) E-mail:junqing2004@163.com

Abstract: In this paper, a novel approach for service substitutions based on the service type in terms of its interface type and behavior semantics is proposed. In order to analyze and verify behavior-consistent service substitutions in dynamic environments, we first present a formal language to describe services from control-flow perspective, then introduce a type and effect system to infer conservative approximations of all possible behaviors of these services. The service behaviors are represented by concurrent behavior expressions (CBEs). Built upon the interpretation of CBEs, behavior-consistent service substitutions are defined and analyzed by subtyping technology. The correctness of the analysis approach is guaranteed by type safety theorem, which is mechanically proved in the Coq proof assistant. Finally, applications in web services show that our method is effective and feasible.

Key words: behavior consistency| concurrent regular expressions| subtyping technology| type and effect systems|service substitutions

摘要: In this paper, a novel approach for service substitutions based on the service type in terms of its interface type and behavior semantics is proposed. In order to analyze and verify behavior-consistent service substitutions in dynamic environments, we first present a formal language to describe services from control-flow perspective, then introduce a type and effect system to infer conservative approximations of all possible behaviors of these services. The service behaviors are represented by concurrent behavior expressions (CBEs). Built upon the interpretation of CBEs, behavior-consistent service substitutions are defined and analyzed by subtyping technology. The correctness of the analysis approach is guaranteed by type safety theorem, which is mechanically proved in the Coq proof assistant. Finally, applications in web services show that our method is effective and feasible.

关键词: behavior consistency| concurrent regular expressions| subtyping technology| type and effect systems|service substitutions

CLC Number: