出版社：Centro Latinoamericano de Estudios en Informática
摘要：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.
