A Rigorous Model of Service Component Architecture

被引：15
作者：
Ding, Zuohua [1 ]
Chen, Zhenbang [2 ,3 ]
Liu, Jing [4 ]
机构：
[1] Zhejiang Sci Tech Univ, Ctr Math Comp & Software Engn, Hangzhou 310018, Peoples R China
[2] United Nations Univ, Int Inst Software Technol, Tokyo, Japan
[3] Natl Lab Parallel & Distributed Proc, Changsha 410073, Hunan, Peoples R China
[4] East China Normal Univ, Inst Theoret Comp, Shanghai 200062, Peoples R China
来源：
ELECTRONIC NOTES IN THEORETICAL COMPUTER SCIENCE | 2008年 / 207卷 / 33-48期
基金：
中国国家自然科学基金;
关键词：
Service Component Architecture; Formal Semantics; Service Composition; Petri nets; Verification;
D O I：
10.1016/j.entcs.2008.03.084
中图分类号：
TP301 [理论、方法];
学科分类号：
081202 ;
摘要：
The Service Component Architecture (SCA) provides a platform-independent component model for serviceoriented development. A service component with different communication mechanisms and implementation languages can be modeled in SCA. However, it lacks a formal foundation for SCA-based system specification and verification. This paper presents a formal service component signature model with respect to the specification of the SCA assembly model. Inspired by the idea of independence in SCA, a language-independent dynamic behaviour model is proposed for specifying the interface behaviour of the service component by port activities. Based on the dynamic behaviour model, the compatibility relation between components is discussed. A set of transition rules are given to map Business Process Execution Language for Web Services (BPEL) to dynamic behaviour expressions and then to Petri nets, thus the service component based system can be verified with existing tools. A case study is demonstrated to illustrate how to use our approach to constructing a web application in a rigorous way.
引用
收藏
页码：33 / 48
页数：16
相关论文
共 26 条
[1]  
Arkin F., 2005, WEB SERVICES BUSINES
[2]  
BEISIEGEL M, SERVICE COMPONENT AR
[3]  
Brogi A., 2004, ELECT NOTES THEORETI, V105, P73, DOI DOI 10.1016/J.ENTCS.2004.05.007
[4]   Component adaptation through flexible subservicing [J].
Brogi, Antonio ;
Canal, Carlos ;
Pimentel, Ernesto .
SCIENCE OF COMPUTER PROGRAMMING, 2006, 63 (01) :39-56
[5]  
Chen Z.B., 2007, 388 UNUIIST
[6]   A refinement driven component-based design [J].
Chen, Zhenbang ;
Liu, Zhiming ;
Stolz, Volker ;
Yang, Lu ;
Ravn, Anders P. .
12TH IEEE INTERNATIONAL CONFERENCE ON ENGINEERING COMPLEX COMPUTER SYSTEMS, PROCEEDINGS, 2007, :277-+
[7]  
Ding Z., 2007, TECHNICAL REPORT
[8]   A Contract-based Approach to Specifying and Verifying Safety Critical Systems [J].
Dong, Wei ;
Chen, Zhenbang ;
Wang, Ji .
ELECTRONIC NOTES IN THEORETICAL COMPUTER SCIENCE, 2007, 176 (02) :89-103
[9]  
Farahbod R, 2004, LECT NOTES COMPUT SC, V3052, P78
[10]  
Ferrara A., 2004, ICSOC 04, P242, DOI DOI 10.1145/1035167.1035202
123