Towards model-based verification of BPEL with model checking

Cao Honghua*, Ying Shi, Du Dehui

*Corresponding author for this work

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

29 Scopus citations

Abstract

BPEL is widely used to specify Web service composition and it's correctness is very important in B2B and B2C domains. However, the correctness of BPEL can only be verified at runtime. This paper presents a model-based verification framework, which can verify BPEL modeled by UML activity diagram with software model checking technology in the design phase. This approach can reduce the cost of systems development and improve the reliability of system models. A metamodel-based transformation framework is proposed to implement the mapping from UML activity diagram to PROMELA-the input language of model checker SPIN to verify BPEL models. To ensure that the transformation is correct and complete, we construct the homomorphic mappings between metamodel elements of activity diagram and PROMELA. The ticket order example illustrates the approach is reasonable and feasible.

Original languageEnglish
Title of host publicationProceedings - Sixth IEEE International Conference on Computer and Information Technology, CIT 2006
DOIs
StatePublished - 2006
Externally publishedYes
Event6th IEEE International Conference on Computer and Information Technology, CIT 2006 - Seoul, Korea, Republic of
Duration: 20 Sep 200622 Sep 2006

Publication series

NameProceedings - Sixth IEEE International Conference on Computer and Information Technology, CIT 2006

Conference

Conference6th IEEE International Conference on Computer and Information Technology, CIT 2006
Country/TerritoryKorea, Republic of
CitySeoul
Period20/09/0622/09/06

Fingerprint

Dive into the research topics of 'Towards model-based verification of BPEL with model checking'. Together they form a unique fingerprint.

Cite this