Volume 10 : Number 2 : Paper 2
December 2007 Regular Issue and Special Issue of Best Papers presented at CLEI 2006, Santiago, Chile
Title:
Model Checking Techniques applied to the design of Web Services

Authors and Affiliations:
M. Emilia Cambronero,
Gregorio Diaz,
Juan J. Pardo, Department of Computer Science, Univ. of Castilla La Mancha, Spain
Fernando Cuartero,
Valentin Valero, Department of Computer Science, Univ. of Castilla La Mancha, Spain.

Abstract:
In previous work we have presented the generation of WS-CDL and WS-BPEL documents.
In this paper we show the unification of both generations. The aim is to generate correct
WS-BPEL skeleton documents from WS-CDL documents by using the Timed Automata as an
intermediary model in order to check the correctness of the generated Web Services with Model
Checking Techniques. The model checker used is UPPAAL, a well known tool in theoretical and
industrial cases that performs the verification and validation of Timed Automata. Note that
our interest is focused on Web services where the time constraints play a critical role.


Received May/07, Revised Aug/07 , Editor: Ernst Leiss, Diego Andrade, Jose Carlos Maldonado, Adenilso Simao, Marcello Visconti
Full paper, 13 pages [ PDF, 426 Kb ]