loading...
 This Article 
   
 Share 
   
 Bibliographic References 
   
 Add to: 
 
Digg
Furl
Spurl
Blink
Simpy
Google
Del.icio.us
Y!MyWeb
 
 Search 
   
Sixth IEEE International Conference on Computer and Information Technology (CIT'06)
Towards Model-based Verification of BPEL with Model Checking
Seoul, Korea
September 20-September 22
ISBN: 0-7695-2687-X
ASCII Text
x 
 
Honghua Cao, Shi Ying, Dehui Du, "Towards Model-based Verification of BPEL with Model Checking," Computer and Information Technology, International Conference on, pp. 190, Sixth IEEE International Conference on Computer and Information Technology (CIT'06), 2006.
 
 
BibTex
x
 
@article{ 10.1109/CIT.2006.185,
author = {Honghua Cao and Shi Ying and Dehui Du},
title = {Towards Model-based Verification of BPEL with Model Checking},
journal ={Computer and Information Technology, International Conference on},
volume = {0},
year = {2006},
isbn = {0-7695-2687-X},
pages = {190},
doi = {http://doi.ieeecomputersociety.org/10.1109/CIT.2006.185},
publisher = {IEEE Computer Society},
address = {Los Alamitos, CA, USA},
}
 
 
RefWorks Procite/RefMan/Endnote
x 
 
TY - CONF
JO - Computer and Information Technology, International Conference on
TI - Towards Model-based Verification of BPEL with Model Checking
SN - 0-7695-2687-X
SP
EP
A1 - Honghua Cao,
A1 - Shi Ying,
A1 - Dehui Du,
PY - 2006
KW - null
VL - 0
JA - Computer and Information Technology, International Conference on
ER -
 
Honghua Cao, Wuhan University, China
Shi Ying, Wuhan University, China
Dehui Du, Wuhan University, China
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.
Citation:
Honghua Cao, Shi Ying, Dehui Du, "Towards Model-based Verification of BPEL with Model Checking," cit, pp.190, Sixth IEEE International Conference on Computer and Information Technology (CIT'06), 2006
Usage of this product signifies your acceptance of the Terms of Use.