跳到主要导航 跳到搜索 跳到主要内容

Towards model-based verification of BPEL with model checking

  • Cao Honghua*
  • , Ying Shi
  • , Du Dehui
  • *此作品的通讯作者
  • Wuhan University

科研成果: 书/报告/会议事项章节会议稿件同行评审

摘要

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.

源语言英语
主期刊名Proceedings - Sixth IEEE International Conference on Computer and Information Technology, CIT 2006
DOI
出版状态已出版 - 2006
已对外发布
活动6th IEEE International Conference on Computer and Information Technology, CIT 2006 - Seoul, 韩国
期限: 20 9月 200622 9月 2006

出版系列

姓名Proceedings - Sixth IEEE International Conference on Computer and Information Technology, CIT 2006

会议

会议6th IEEE International Conference on Computer and Information Technology, CIT 2006
国家/地区韩国
Seoul
时期20/09/0622/09/06

指纹

探究 'Towards model-based verification of BPEL with model checking' 的科研主题。它们共同构成独一无二的指纹。

引用此