%0 Journal Article %1 Ding2009 %A Ding, Zuohua %A Jiang, Mingyue %A Liu, Jing %B Proceedings of the 2009 Eigth IEEE/ACIS International Conference on Computer and Information Science %D 2009 %I IEEE Computer Society %K %P 1029--1034 %T Model Checking Service Component Composition by SPIN %U http://portal.acm.org/citation.cfm?id=1605395.1606033 %X 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. %@ 978-0-7695-3641-5

@article{Ding2009, 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.}, added-at = {2010-03-22T14:17:10.000+0100}, author = {Ding, Zuohua and Jiang, Mingyue and Liu, Jing}, biburl = {https://www.bibsonomy.org/bibtex/27206de5b1de3556f7e0c5814dcbe6572/ramkumarrs}, booktitle = {Proceedings of the 2009 Eigth IEEE/ACIS International Conference on Computer and Information Science}, interhash = {9315b1e19d83aa96b492cc4b9f9d81f9}, intrahash = {7206de5b1de3556f7e0c5814dcbe6572}, isbn = {978-0-7695-3641-5}, keywords = {}, pages = {1029--1034}, publisher = {IEEE Computer Society}, timestamp = {2010-03-22T14:17:10.000+0100}, title = {Model Checking Service Component Composition by SPIN}, url = {http://portal.acm.org/citation.cfm?id=1605395.1606033}, year = 2009 }