The investigation of TLC model checker properties

Simple item page
dc.contributor.authorШкарупило, Вадим Вікторович
dc.contributor.authorШкарупило, Вадим Викторович
dc.contributor.authorShkarupylo, Vadym V.
dc.contributor.authorТомічич, Ігор
dc.contributor.authorТомичич, Игорь
dc.contributor.authorTomičić, Igor
dc.contributor.authorКасьян, Констянтин Миколайович
dc.contributor.authorКасьян, Константин Николаевич
dc.contributor.authorKasyan, Konstantin M.
dc.date.accessioned2016-08-26T12:23:03Z
dc.date.available2016-08-26T12:23:03Z
dc.date.issued2016
dc.descriptionShkarupylo V. V. The investigation of TLC model checker properties / V. V. Shkarupylo, I. Tomičić, K. M. Kasian // Journal of Information and Organizational Sciences. – 2016. – Vol. 40, No. 1. – P. 145–152.uk
dc.description.abstractUK: У роботі проведено дослідження і порівняння властивостей методу перевірки на моделі TLC (TLA Checker). Розглянуто два підходи до використання методу. Перший підхід полягає в обході станів системи переходів методом обходу в ширину (BFS), другий – методом обходу в глибину (DFS). У якості моделі системи переходів використано структуру Кріпке. Проведено експериментальне дослідження, де в якості сценарію предметної області розглянуто використання композитного веб-сервісу. Одержані результати дослідження можуть бути використані для підвищення ефективності автоматизованої верифікації TLA+ специфікацій. EN: This paper presents the investigation and comparison of TLC model checking method (TLA Checker) properties. There are two different approaches to method usage which are considered. The first one consists of a transition system states attendance by breadth-first search (BFS), and the second one by depth-first search (DFS). The Kripke structure has been chosen as a transition system model. A case study has been conducted, where composite web service usage scenario has been considered. Obtained experimental results are aimed at increasing the effectiveness of TLA+ specifications automated verification. RU: В работе проведены исследование и сравнение свойств метода проверки на модели TLC (TLA Checker). Рассмотрены два подхода к использованию метода. Первый подход состоит в обходе состояний системы переходов методом обхода в ширину (BFS), второй подход – методом обхода в глубину (DFS). В качестве модели системы переходов использована структура Крипке. Проведено экспериментальное исследование, где в качестве сценария предметной области рассмотрено использование композитного веб-сервиса. Полученные результаты исследования могут быть использованы для повышения эффективности автоматизированной верификации TLA+ спецификаций.uk
dc.identifier.issn1846-3312
dc.identifier.urihttp://eir.zntu.edu.ua/handle/123456789/1130
dc.language.isoenuk
dc.publisherUniversity of Zagreb, Varaždin, Croatiauk
dc.subjectкомпозитний веб-сервісuk
dc.subjectперевірка на моделіuk
dc.subjectWS-BPELuk
dc.subjectBFSuk
dc.subjectDFSuk
dc.subjectTLA+uk
dc.subjectTLCuk
dc.subjectComposite Web Serviceuk
dc.subjectModel Checkinguk
dc.subjectкомпозитный веб-сервисuk
dc.subjectпроверка на моделиuk
dc.titleThe investigation of TLC model checker propertiesuk
dc.title.alternativeДослідження властивостей методу перевірки на моделі TLCuk
dc.title.alternativeИсследование свойств метода проверки на модели TLCuk
dc.typeArticleuk

Files

Original bundle
Now showing 1 - 1 of 1
Thumbnail Image
Name:
Shkarupylo_art_JIOS_2016.pdf
Size:
723.05 KB
Format:
Adobe Portable Document Format
Description:
Наукова стаття
Download
License bundle
Now showing 1 - 1 of 1
No Thumbnail Available
Name:
license.txt
Size:
1.71 KB
Format:
Item-specific license agreed upon to submission
Description:
Download

Collections

Наукові статті кафедри КС та М