• V. V. Shkarupylo Zaporizhzhya National Technical University, Zaporizhzhya
  • R. K. Kudermetov Zaporizhzhya National Technical University, Zaporizhzhya
  • O. V. Polska Zaporizhzhya National Technical University, Zaporizhzhya



SOA, WS-BPEL, Composite Web Service, Specification, Verification, Validation, TLA, DEVS.


A technique for Composite Web Services validity checking has been proposed. It is based on discrete-event DEVS-models synthesis, which
provides the ability to conduct the automated validation by way of simulation during the design process. Temporal Logic of Actions has been chosen as the basis for input data – formal specification of Composite Web Service. It allows to specify the functional properties of such systems mathematically strictly. Functional properties has been represented as computational processes. The Kripke structure has been used as TLA-specification analytical model. Our technique leans on the proposed rules, aimed at simulation DEVS-model synthesis from given
TLA-specification. The resulting coupled Composite Web Service DEVS-model consists of atomic web services models, model of client,
simulated as job-requests generator, and coordinator model. Coordinator represents the WS-BPEL-engine, functioning in accordance with centralized orchestration model. A case study has been conducted to verify the proposed technique. Its artifacts confirmed the adequacy of resulting DEVS-model. The technique verification is based on the proposed approach: simulation-driven validation results are compared with the ones, obtained with testdriven validation. Technique expediency has been grounded by Composite Web Services validity checking time costs reduction.


Service-Oriented Computing: State of the Art and Research Challenges / [M. P. Papazoglou, P. Traverso, S. Dustdar, F. Leymann] // IEEE Computer. – 2007. – Vol. 40, No. 11. – P. 38–45. DOI: 10.1109/MC.2007.400. 2. Vohra D. Java 7 JAX-WS Web Services: A practical, focused mini book for creating Web Services in Java 7 / D. Vohra. – Birmingham- Mumbai: Packt Publishing Ltd., 2012. – 64 p. 3. Freeman S. Growing Object-Oriented Software, Guided by Tests / S. Freeman, N. Pryce. – New York : Addison-Wesley, 2010. – 384 p. 4. Wainer G. A. Discrete-Event Modeling and Simulation: Theory and Applications / G. A. Wainer, P. J. Mosterman. – New York : CRC Press, 2010. – 534 p. 5. Kindermann R. Beyond Lassos: Complete SMT-Based Bounded Model Checking for Timed Automata / R. Kindermann, T. Junttila, I. Niemela // Lecture Notes in Computer Science. Formal Techniques for Distributed Systems. – 2012. – Vol. 7273. – P. 84–100. DOI: 10.1007/978-3-642-30793-5_6. 6. Системи управління якістю. Основні положення та словник термінів (ISO 9000:2005, IDT) : ДСТУ ISO 9000:2007. – [Чин- ний від 2008-01-01]. – К.: Держспоживстандарт України. – 29 с. – (Національний стандарт України). 7. Шкарупило В. В. Модель TLA-спецификации композитного веб-сервиса с множеством динамик / В. В. Шкарупило // Радіоелектроніка, інформатика, управління. –2013. – № 1. – С. 94–100. DOI: 10.15588/1607-3274-2013-1-15. 8. Карпов Ю. Г. MODEL CHECKING. Верификация параллельных и распределенных программных систем / Ю. Г. Карпов. – СПб. : БХВ-Петербург, 2010. – 560 с. 9. Шкарупило В. В. DEVS-модель как средство валидации композитных веб-сервисов распределенной системы / В. В. Шкарупило, С. Ю. Скрупський, Р. К. Кудерметов // Комп’ютерно- інтегровані технології: освіта, наука, виробництво. – 2011. – № 7. – С. 61–67. 10. Lamport L. Specifying Systems: The TLA+ Language and Tools for Hardware and Software Engineers / L. Lamport. – Boston: Addison-Wesley, 2002. – 364 p. 11. Шкарупило В. В. WS-BPEL-модификация метода TLC-верификации / В. В. Шкарупило // Східно-європейський журнал передових технологій. – Харків: НВП «Технологічний центр», 2013. – № 4/2 (64). – С. 23–28. 12. Cristia M. A TLA+ Encoding of DEVS Models / M. Cristia // Proc. Int. Modeling and Simulation Multiconference (Buenos Aires, Argentina, February 8–10, 2007). – P. 17–22. 13. Шкарупило В. В. Сравнительный анализ подходов к реализации процесса автоматизированного синтеза композитных веб- сервисов / В. В. Шкарупило, Р. К. Кудерметов // Науковий вісник Чернівецького національного університету імені Юрія Федьковича. Серія: комп’ютерні системи та компоненти. – Чернівці: ЧНУ, 2011. – Т. 2, № 4. – С. 80–85. 14. Web Services Business Process Execution Language Version 2.0 [Electronic resource] : OASIS Standard, April 11, 2007. – Access mode: – Title from screen. 15. Шкарупило В. В. Концептуальная модель процесса автоматизированного синтеза композитных веб-сервисов / В. В. Шкарупило, Р. К. Кудерметов, Т. А. Паромова // Наукові праці Донецького національного технічного університету. Серія: Інформатика, кібернетика та обчислювальна техніка. – Донецьк : ДонНТУ, 2012. – № 15 (203). – С. 231–238. 16. Шкарупило В. В. Методика автоматизированного синтеза композитных веб-сервисов / В. В. Шкарупило, Р. К. Кудерметов / / Інформатика і комп’ютерні технології : VІІ Міжнар. наук.- техн. конф. студентів, аспірантів та молодих учених, 22–23 листопада 2011 р. : тези доп. – Донецьк : ДонНТУ, 2011. – Т. 1. – С. 382–384.



How to Cite

Shkarupylo, V. V., Kudermetov, R. K., & Polska, O. V. (2015). DEVS-ORIENTED TECHNIQUE FOR COMPOSITE WEB SERVICES VALIDITY CHECKING. Radio Electronics, Computer Science, Control, (4).



Progressive information technologies