Model Checking Techniques applied to the design of Web Services

Authors

  • Gregorio Dıaz Department of Computer Science, Univ. of Castilla La Mancha
  • Emilia M. Cambronero Department of Computer Science, Univ. of Castilla La Mancha
  • Juan J. Pardo Department of Computer Science, Univ. of Castilla La Mancha
  • Valentın Valero Department of Computer Science, Univ. of Castilla La Mancha
  • Fernando Cuartero Department of Computer Science, Univ. of Castilla La Mancha

DOI:

https://doi.org/10.19153/cleiej.10.2.2

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.

Downloads

Published

2007-12-01

Issue

Vol. 10 No. 2 (2007): Regular Issue and Special Issue of Best Papers presented at CLEI 2006, Santiago, Chile

Section

Articles

License

CLEIej is supported by its home institution, CLEI, and by the contribution of the Latin American and international researchers community, and it does not apply any author charges whatsoever for submitting and publishing. Since its creation in 1998, all contents are made publicly accesibly. The current license being applied is a (CC)-BY license (effective October 2015; between 2011 and 2015 a (CC)-BY-NC license was used).