Model Cheking Techniques applied to the design of Web Services
 
Gregorio Díaz, M. E. Cambronero, Juan J. Pardo,

Valentín Valero and Fernando Cuartero


Departament of Computer Science, Univ. Of Castilla La Mancha
EPSA, Avd. Espaa s/n, Albacete, Spain, 02071.
Email: [gregorio, emicp, jpardo, fernando]@info-ab.uclm.es
 
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 documentby 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.