WS-BPEL-модифікація методу TLC-верифікації

Автор(и)

  • Вадим Викторович Шкарупило Запорізький національний технічний університет, вул. Жуковського, 64, м. Запоріжжя, Україна, 69063, Україна

DOI:

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

Ключові слова:

композитний веб-сервіс, WS-BPEL, специфікація, структура Кріпке, TLC, верифікація, стратифікація

Анотація

Запропоновано модифікацію методу верифікації TLA Checker (TLC), спрямовану на зменшення часових витрат, обумовлених процесом перевірки WS-BPEL-описів композитних веб-сервісів на основі відповідних формальних TLA-моделей. Модифікація полягає у серії з BFS- та DFS-обходів

Біографія автора

Вадим Викторович Шкарупило, Запорізький національний технічний університет, вул. Жуковського, 64, м. Запоріжжя, Україна, 69063

Аспірант

Кафедра комп’ютерних систем та мереж

Посилання

  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.

##submission.downloads##

Опубліковано

2013-07-30

Як цитувати

Шкарупило, В. В. (2013). WS-BPEL-модифікація методу TLC-верифікації. Eastern-European Journal of Enterprise Technologies, 4(2(64), 23–28. https://doi.org/10.15587/1729-4061.2013.16654

Номер

Том 4 № 2(64) (2013): Інформаційні технології і системи управління в промисловості

Розділ

Інформаційні технології

Ліцензія

Авторське право (c) 2014 Вадим Викторович Шкарупило

Creative Commons License

Ця робота ліцензується відповідно до Creative Commons Attribution 4.0 International License.

Закріплення та умови передачі авторських прав (ідентифікація авторства) здійснюється у Ліцензійному договорі. Зокрема, автори залишають за собою право на авторство свого рукопису та передають журналу право першої публікації цієї роботи на умовах ліцензії Creative Commons CC BY. При цьому вони мають право укладати самостійно додаткові угоди, що стосуються неексклюзивного поширення роботи у тому вигляді, в якому вона була опублікована цим журналом, але за умови збереження посилання на першу публікацію статті в цьому журналі.

Ліцензійний договір – це документ, в якому автор гарантує, що володіє усіма авторськими правами на твір (рукопис, статтю, тощо).
Автори, підписуючи Ліцензійний договір з ПП «ТЕХНОЛОГІЧНИЙ ЦЕНТР», мають усі права на подальше використання свого твору за умови посилання на наше видання, в якому твір опублікований. Відповідно до умов Ліцензійного договору, Видавець ПП «ТЕХНОЛОГІЧНИЙ ЦЕНТР» не забирає ваші авторські права та отримує від авторів дозвіл на використання та розповсюдження публікації через світові наукові ресурси (власні електронні ресурси, наукометричні бази даних, репозитарії, бібліотеки тощо).
За відсутності підписаного Ліцензійного договору або за відсутністю вказаних в цьому договорі ідентифікаторів, що дають змогу ідентифікувати особу автора, редакція не має права працювати з рукописом.
Важливо пам’ятати, що існує і інший тип угоди між авторами та видавцями – коли авторські права передаються від авторів до видавця. В такому разі автори втрачають права власності на свій твір та не можуть його використовувати в будь-який спосіб.