In this paper we introduce a tool called the Web Service Translation tool (WST), which we are developing to implement a methodology for the design, validation and verification of Web Services with timed restrictions. This methodology works by making several translations, from phase to phase in the software development life cycle, where the system is represented at each phase by XML models. We use XSL Transformations (XSLT), which is a language for transforming XML documents. The purpose of these translations is to generate XML code automatically for a Web Service system and to obtain Web Services description models with Timed Automata for validating and verifying composite Web Services with time restrictions.
ArkinAAskarySBlochBCurberaFGolandYKarthaN. Web Services Business Process Execution Language Version 2.0, December2004. http://www.oasis-open.org
2.
KavantzasNBurdettDRitzingerGFletcherTLafonYBarretoC. Web Service Choreography Description Language (WSCDL) 1.0, 2005. http://www.w3.org/TR/ws-cdl-10/
3.
HamadiRBenatallahB. A Petri net-based model for Web Service composition. In Proceedings of the 14th Australasian Database Conference, Vol. 17, 2003, p.191–200.
AlurRDillDL. Automata for modeling real-time systems. In ICALP 1990: Proceedings of the 17th International Colloquium on Automata, Languages and Programming (Lecture Notes in Computer Science, Vol. 443). London: Springer-Verlag, 1990, p.322–335.
6.
BozgaMDawsCMalerOOliveroATripakisSYovineS. Kronos: a model-checking tool for real-time systems. In Proceedings 10th International Conference on Computer Aided Verification, Vancouver, Canada, (Lecture Notes in Computer Science, Vol. 1427). New York: Springer-Verlag, 1998, p.546–550.
7.
LarsenKGPetterssonPWangY. UPPAAL in a nutshell. Int J Softw Tools Technol Transfer1997; 1: 134–152.
8.
FosterHUchitelSMageeJKramerJ. WS-Engineer: a tool for model-based verification of Web Service compositions and choreography. In 29th IEEE/ACM International Conference on Software Engineering (ICSE). New York: IEEE Computer Society/ACM Press, 2006, p.771–774.
9.
Risco-MartínJLMittalS. eUDEVS: Executable UML with DEVS theory of modeling and simulation. SIMULATIONVol. 85, No. 11–12, 2009, p. 750–777.
10.
MateescuRRampacekS. Formal modeling and discrete-time analysis of BPEL Web Services. Int J Sim Process Modelling2008; 4: 183–194.
11.
FuXBultanTSuJ. Wsat: a tool for formal analysis of Web Services. In Proceedings of Computer-Aided Verification (CAV) (Lecture Notes in Computer Science, Vol. 3114). New York: Springer–Verlag, 2004, p.510–514.
12.
HolzmannGJ. Design and Validation of Protocols. Englewood Cliffs, NJ: Prentice-Hall, 1990.
13.
HolzmannGJ. The SPIN Model Checker: Primer and Reference Manual. Reading, MA: Addison-Wesley, 2003.
14.
GravelAFuXSuJ. An analysis tool for execution of BPEL Services. In IEEE Joint Conference on E-Commerce Technology (CEC) and Enterprise Computing, E-Commerce and E-Services (EEE), Tokyo, Japan, 2007. New York: IEEE Computer Society, 2007, p.429–432.
15.
KazhamiakinR. Formal Analysis of Web Service Compositions. PhD Dissertation, University of Trento, 2007.
16.
CimattiAClarkeEMGiunchigliaFRoveriM. NuSMV: A new symbolic model checker. Int J Softw Tools Technol Transfer2000; 2: 410–425.
17.
DongJSLiuYSunJZhangX. Verification of computation orchestration via timed automata. In Proceedings of the 8th International Conference on Formal Engineering Methods (Lecture Notes in Computer Science, Vol. 4260). New York: Springer-Verlag, 2006, p.226–245.
NakajimaS. Model-checking behavioral specification of BPEL applications. In Proceedings of the International Workshop on Web Languages and Formal Methods (Electronic Notes in Theoretical Computer Science, Vol. 151(2)), Newcastle, UK, 2005. Amsterdam: Elsevier, 2005, p.89–105.
20.
van der AalstWMPPesicM. Specifying and monitoring service flows: Making Web Services process-aware. In: BaresiLDi NittoE. Test and Analysis of Web Services. New York: Springer, 2007, 11–55.
21.
PesicMSchonenbergHvan der AalstWMP. DECLARE: full support for loosely-structured processes. In Proceedings of 11th International Enterprise Distributed Object Computing Conference (EDOC’07). Los Alamitos, CA: IEEE Computer Society Press, 2007, p.287.
22.
BaresiLGhezziCZanoliniL. Modeling and validation of publish/subscribe architectures. In: BeydedaSGruhnV. Testing Commercial-off-the-Shelf Components and Systems. New York: Springer-Verlag, 2005, 273–291.
23.
ZhouXTsaiWTWeiXChenYXiaoB. Pi4soa: a policy infrastructure for verification and control of service collaboration. In ICEBE 2006: Proceedings of the IEEE International Conference on e-Business Engineering, Washington, DC, 2006. New York: IEEE Computer Society, p.307–314.
24.
van LamsweerdeADardenneAFickasS. Goal-directed requirements acquisition. In Selected Papers of the Sixth International Workshop on Software Specification and Design. Sci Comput Programm1993; 20: 3–50.
25.
DiazGCambroneroMEValeroVCuarteroF. Analysis and verification of time requirements applied to the Web Services composition. In Proceedings of WS-FM 2006 (Lecture Notes in Computer Science, Vol. 4184). New York: Springer-Verlag, 2006, p.178–192.
26.
BehrmannGDavidAKLarsenKGHakanssonJPetterssonPYiWHendriksM. UPPAAL 4.0. In QEST 2006: Proceedings of the Third International Conference on the Quantitative Evaluation of Systems, Riverside, CA, 2006. New York: IEEE Computer Society, 2006, p.125–126.
CambroneroMEDiazGPardoJJValeroVPelayoF. RT-UML for modeling real-time Web Services. In Proceedings of Modeling, Design, and Analysis for Serviceoriented Architecture Workshop, mda4soa, SCC 2006, Chicago, IL, 2006. New York: IEEE Computer Society, 2006, p.131–139.
29.
CambroneroMEValeroVDiazG. Web Services Choreographies Verification. Report DIAB-09-04-1, University of Castilla-La Mancha, April2009.
