Model Checking Service Component Composition by SPIN

Author

Ding, Zuohua ; Jiang, Mingyue ; Liu, Jing

Author_Institution

Center of Math Comput. & Software Eng., Zhejiang Sci-Tech Univ., Hangzhou, China

fYear

2009

fDate

1-3 June 2009

Firstpage

1029

Lastpage

1034

Abstract

Service Component Architecture (SCA) provides a language-independent way to define and compose service component. The SCA assembly model should be reliable. This target can be reached by translating a formal signature model and behavior model for SCA to Promela, and Promela specifications are then verified with the model checker SPIN. SCA complements some service composition languages (such as BPEL) for enabling the more convenient and efficient service-based development. Based on our method and by using IBM WID tool, we show how to build a reliable BPEL process.

Keywords

Web services; formal verification; software architecture; IBM WID tool; Promela specifications; formal signature model; model checking service component composition; service component architecture; service composition languages; service-based development; Assembly; Buildings; Calculus; Character generation; Component architectures; Information science; Service oriented architecture; Software engineering; Web services; Wire;

fLanguage

English

Publisher

ieee

Conference_Titel

Computer and Information Science, 2009. ICIS 2009. Eighth IEEE/ACIS International Conference on

Conference_Location

Shanghai

Print_ISBN

978-0-7695-3641-5

Type

conf

DOI

10.1109/ICIS.2009.212

Filename

5223242