Title :
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
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;
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
DOI :
10.1109/ICIS.2009.212
