WS-BPEL-modification of TLC-verification method

Authors

  • Вадим Викторович Шкарупило Zaporizhzhya National Technical University, Zhukovskoho St 64, Zaporizhzhya, Ukraine, 69063, Ukraine

DOI:

https://doi.org/10.15587/1729-4061.2013.16654

Keywords:

Composite Web Service, WS-BPEL, Specification, Kripke structure, TLC, Verification, Stratification

Abstract

To increase the confidence that Composite Web Service functional properties will correspond to our expectations the Formal Verification procedure can be conducted. In order to do that the appropriate specification formalism has to be chosen first. Temporal Logic of Actions TLA+ language usage represents the way to get compact and easily reconfigurable formal models. Broadly adopted WS-BPEL 2.0 OASIS standard can provide us with building blocks for such models retrieving. The aforementioned re-configurability is achievable by models stratification.

As for transition system model the Kripke structure completely fits the domain. TLA Checker (TLC) as TLA Toolbox framework built-in component is a convenient way to get the job done. Despite that, comparing to UPPAAL tool performance for instance, the minor TLC tweaking has yet to be applied.

To this end the modification of TLC-verification method has been proposed. Modification is based on TLA-models stratification coupled with the sequence of Breadth-first- (BFS) and Depth-firstsearches (DFS)

Author Biography

Вадим Викторович Шкарупило, Zaporizhzhya National Technical University, Zhukovskoho St 64, Zaporizhzhya, Ukraine, 69063

Postgraduate

Department of Computer Systems and Networks

References

  1. Grumberg, O. 25 Years of Model Checking: History, Achievements, Perspectives [Text] / O. Grumberg, H. Veith. – Berlin: Springer, 2008. – 231 p. – ISBN 10 3-540-69849-3.
  2. Тарасюк, О. М. Формальные методы разработки критического программного обеспечения [Текст] : лекционный материал / О. М. Тарасюк, А. В. Горбенко; под ред. В. С. Харченко – МОН Украины, Национальный аэрокосмический университет им. Н. Е. Жуковского «ХАИ», 2009. – 214 с. – ISBN 978-966-96770-8-2.
  3. Vorobyov, K. Comparing Model Checking and Static Program Analysis: A Case Study in Error Detection Approaches [Текст] /
  4. K. Vorobyov, P. Krishnan // Proc. 5th Int. Workshop on Systems Software Verification, SSV 2010 (Vancouver, Canada, October 6 – 7, 2010). – P. 1 – 7.
  5. Web Services Business Process Execution Language, Version 2.0 [Электронный ресурс] // OASIS Standard, April 11, 2007. – Режим доступа : http://docs.oasis-open.org/wsbpel/2.0/wsbpel-v2.0.pdf. – Заголовок с экрана.
  6. Cao, T-D. An Approach to Automated Runtime Verification for Timed Systems: Applications to Web Services [Текст] / T-D. Cao, R. Castanet, P. Felix, K. Chiew // Journal of Software. – 2012. – Vol. 7, No. 6. – P. 1338 – 1350.
  7. Dhore, S. R. QoS Based Web Services Composition using Ant Colony Optimization: Mobile Agent Approach [Текст] /
  8. S. R. Dhore, M. U. Kharat // International Journal of Advanced Research in Computer and Communication Engineering. – 2012. – Vol. 1, No. 7. – P. 519 – 527.
  9. Кормен, Т. Х. Алгоритмы: построение и анализ [Текст] : пер. с англ. / Т. Х. Кормен, Ч. И. Лейзерсон, Р. Л. Ривест, К. Штайн. – 2-е изд. – М.: Вильямс, 2005. – 1296 с. – ISBN 5-8459-0857-4.
  10. Zheng, L. Improving SAT using 2-SAT / L. Zheng, P. J. Stuckey [Текст] // Australian Computer Science Communications. – 2002. – Vol. 24, No. 1. – P. 331 – 340.
  11. Larsen, K. Model-based Verification and Analysis for Real-Time Systems [Текст] / K. Larsen // Proc. NATO Advanced Study Institute – Int. Summer School MOD 2012 on Engineering Dependable Software Systems (Marktoberdorf, Germany, July 31 – August 12, 2012). – 155 p.
  12. Lamport, L. Specifying Systems: The TLA+ Language and Tools for Hardware and Software Engineers [Текст] / L. Lamport. – Boston.: Addison-Wesley, 2002. – 364 p. – ISBN 0-321-14306-X.
  13. Шкарупило, В. В. Концептуальная модель процесса автоматизированного синтеза композитных веб-сервисов [Текст] / В. В. Шкарупило, Р. К. Кудерметов, Т. А. Паромова // Сборник научных трудов ДонНТУ. Серия : Информатика, кибернетика и вычислительная техника. – Донецк : ДонНТУ, 2012. – Вып. 15 (203). – С. 231 – 238.
  14. Shkarupylo, V. V. An Approach to Composite Web Services Formal Verification [Текст] / V. V. Shkarupylo, R. K. Kudermetov // Сборник научных трудов ДонНТУ. Серия : Информатика, кибернетика и вычислительная техника. – Донецк : ДонНТУ, 2012. – Вып. 16 (204). – С. 129 – 133.
  15. Ravn, A. P. A formal analysis of the web services atomic transaction protocol with UPPAAL [Текст] / A. P. Ravn, J. Srba, S. Vighio // Proc. 4th Int. Conf. on Leveraging Applications of Formal Methods, Verification and Validation, ISoLA 2010 (Heraklion, Crete, October 18 – 20, 2010). – P. 579 – 593.
  16. Шкарупило, В. В. Модель TLA-спецификации композитного веб-сервиса с множеством динамик [Текст] / В. В. Шкарупило // Радіоелектроніка, інформатика, управління. – Запорожье: ЗНТУ, 2013. – Вып. 1 (28). – С. 94 – 100.
  17. Хоар, Ч. Взаимодействующие последовательные процессы [Текст] : пер. с англ. / Ч. Хоар. – М.: Мир, 1989. – 264 с. – ISBN 5-03-001043-2.
  18. Семенов, А. А. Двоичные диаграммы решений в параллельных алгоритмах обращения дискретных функций [Текст] / А. А. Семенов, А. С. Игнатьев, Д. В. Беспалов // Параллельные вычислительные технологии, ПаВТ 2009 : III междунар. науч. конф., 30 марта – 3 апр. 2009 г. : тезисы докл. – Нижний Новгород : ННГУ им. Н. И. Лобачевского, 2009. – С. 688–696.
  19. Grumberg, O., & Veith, H. (2008). 25 Years of Model Checking: History, Achievements, Perspectives. Berlin: Springer, 231.
  20. Tarasyuk, O. M., & Gorbenko, A. V. (2009). Formal’nye metody razrabotki kriticheskogo programmnogo obespecheniya. Nacional’nyj ae’rokosmicheskij universitet im. N. E. Zhukovskogo, 214.
  21. Vorobyov, K., & Krishnan, P. (2010, October 6 – 7). Comparing Model Checking and Static Program Analysis: A Case Study in Error Detection Approaches. Paper presented at the Proc. 5th Int. Workshop on Systems Software Verification (pp. 1 – 7). Canada: Vancouver.
  22. Web Services Business Process Execution Language. (2007, April 11). OASIS Standard, Version 2.0 [standard]. Retrieved from http:// docs.oasis-open.org/wsbpel/2.0/wsbpel-v2.0.pdf.
  23. Cao, T-D., Castanet, R., Felix, P., & Chiew, K. (2012). An Approach to Automated Runtime Verification for Timed Systems: Applications to Web Services. Journal of Software, 7 (6), 1338 – 1350.
  24. Dhore, S. R., & Kharat, M. U. (2012). QoS Based Web Services Composition using Ant Colony Optimization: Mobile Agent Approach. International Journal of Advanced Research in Computer and Communication Engineering, 1 (7), 519 – 527.
  25. Cormen, T. H., Stein, C., Rivest, R. L., & Leiserson, C. E. (2001). Introduction to Algorithms (2nd ed.). Boston: The MIT Press, 1296.
  26. Zheng L., Stuckey, P. J. (2002). Improving SAT using 2-SAT. Australian Computer Science Communications, 24 (1), 331 – 340.
  27. Larsen, K. (2012, July 31 – August 12). Model-based Verification and Analysis for Real-Time Systems. Paper presented at the Proc. NATO Advanced Study Institute – Int. Summer School MOD 2012 on Engineering Dependable Software Systems. Germany: Marktoberdorf, 155.
  28. Lamport, L. (2002). Specifying Systems: The TLA+ Language and Tools for Hardware and Software Engineers. Boston: Addison-Wesley, 364.
  29. Shkarupylo, V. V., Kudermetov, R. K., & Paromova, T. A. (2012). Konceptual’naya model’ processa avtomatizirovannogo sinteza kompozitnyx veb-servisov. Sbornik nauchnyx trudov DonNTU. Seriya : Informatika, kibernetika i vychislitel’naya texnika, 15 (203), 231–238.
  30. Shkarupylo, V. V., & Kudermetov, R. K. (2012). An Approach to Composite Web Services Formal Verification. Sbornik nauchnyx trudov DonNTU. Seriya : Informatika, kibernetika i vychislitel’naya texnika, 16 (204), 129 – 133.
  31. Ravn, A. P., Srba, J., & Vighio, S. (2010, October 18 – 20). A formal analysis of the web services atomic transaction protocol with UP PAAL. Paper presented at the Proc. 4th Int. Conf. on Leveraging Applications of Formal Methods, Verification and Validation (pp. 579–593). Crete: Heraklion.
  32. Shkarupylo, V. V. (2013). A model of multi-behavioral Composite Web Service TLA-specification. Radio Electronics, Computer Science, Control, 1 (28), 94 – 100.
  33. Hoare, C. A. R. (1989). Communicating Sequential Processes. London: Prentice-Hall, 264.
  34. Semenov, A. A., Ignat’ev A. S., & Bespalov, D. V. (2009, March 30 – April 3). Dvoichnye diagrammy reshenij v parallel’nyx algoritmax obrashheniya diskretnyx funkcij. Paper presented at the Proc. 3rd Int. Conf. on Parallel Computing Technologies in Science and Education (pp. 688 – 696). Nizhnij Novgorod: NNGU im. N. I. Lobachevskogo.

Downloads

Published

2013-07-30

How to Cite

Шкарупило, В. В. (2013). WS-BPEL-modification of TLC-verification method. Eastern-European Journal of Enterprise Technologies, 4(2(64), 23–28. https://doi.org/10.15587/1729-4061.2013.16654

Issue

Vol. 4 No. 2(64) (2013): Industry control systems

Section

Information technology

License

Copyright (c) 2014 Вадим Викторович Шкарупило

Creative Commons License

This work is licensed under a Creative Commons Attribution 4.0 International License.

The consolidation and conditions for the transfer of copyright (identification of authorship) is carried out in the License Agreement. In particular, the authors reserve the right to the authorship of their manuscript and transfer the first publication of this work to the journal under the terms of the Creative Commons CC BY license. At the same time, they have the right to conclude on their own additional agreements concerning the non-exclusive distribution of the work in the form in which it was published by this journal, but provided that the link to the first publication of the article in this journal is preserved.

A license agreement is a document in which the author warrants that he/she owns all copyright for the work (manuscript, article, etc.).
The authors, signing the License Agreement with TECHNOLOGY CENTER PC, have all rights to the further use of their work, provided that they link to our edition in which the work was published.
According to the terms of the License Agreement, the Publisher TECHNOLOGY CENTER PC does not take away your copyrights and receives permission from the authors to use and dissemination of the publication through the world's scientific resources (own electronic resources, scientometric databases, repositories, libraries, etc.).
In the absence of a signed License Agreement or in the absence of this agreement of identifiers allowing to identify the identity of the author, the editors have no right to work with the manuscript.
It is important to remember that there is another type of agreement between authors and publishers – when copyright is transferred from the authors to the publisher. In this case, the authors lose ownership of their work and may not use it in any way.