Research Article
Modeling and Verifying WS-CDL Using Event-B
@INPROCEEDINGS{10.1007/978-3-642-36642-0_29, author={Hong Le and Ninh Truong}, title={Modeling and Verifying WS-CDL Using Event-B}, proceedings={Context-Aware Systems and Applications. First International Conference, ICCASA 2012, Ho Chi Minh City, Vietnam, November 26-27, 2012, Revised Selected Papers}, proceedings_a={ICCASA}, year={2013}, month={2}, keywords={WS-CDL composition verification Event-B}, doi={10.1007/978-3-642-36642-0_29} }- Hong Le
Ninh Truong
Year: 2013
Modeling and Verifying WS-CDL Using Event-B
ICCASA
Springer
DOI: 10.1007/978-3-642-36642-0_29
Abstract
The Web Services Choreography Description Language (WS-CDL) is an XML-based language that describes web service composition in the view point of choreography by defining their common and complementary observable behavior, where ordered message exchanges result in accomplishing a common business goal [3]. However, WS-CDL does not come with formal specification, nor with official vefication tools. In this paper, we present an approach to formalize and verify choreography composition described in WS-CDL. In the first phase, we propose to use Event-B as a formal method to model choreography interactions by transforming WS-CDL entities to Event-B elements. We use the Rodin platform, in the next phase, to verify some properties of the translated model. Finally, we run an example to illustrate our approach in detail.