Model checking service component composition by SPIN

  • Zuohua Ding
  • , Mingyue Jiang
  • , Jing Liu*
  • *Corresponding author for this work

Research output: Chapter in Book/Report/Conference proceedingConference contributionpeer-review

1 Scopus citations

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.

Original languageEnglish
Title of host publicationProceedings of the 2009 8th IEEE/ACIS International Conference on Computer and Information Science, ICIS 2009
PublisherIEEE Computer Society
Pages1029-1034
Number of pages6
ISBN (Print)9780769536415
DOIs
StatePublished - 2009
Event8th IEEE/ACIS International Conference on Computer and Information Science, ICIS 2009 - Shanghai, China
Duration: 1 Jun 20093 Jun 2009

Publication series

NameProceedings of the 2009 8th IEEE/ACIS International Conference on Computer and Information Science, ICIS 2009

Conference

Conference8th IEEE/ACIS International Conference on Computer and Information Science, ICIS 2009
Country/TerritoryChina
CityShanghai
Period1/06/093/06/09

Fingerprint

Dive into the research topics of 'Model checking service component composition by SPIN'. Together they form a unique fingerprint.

Cite this