An approach to increase the effectiveness of TLC verification with respect to the concurrent structure of TLA+ specification

Simple item page
dc.contributor.authorШкарупило, Вадим Вікторович
dc.contributor.authorТомічич, Ігор
dc.contributor.authorКасьян, Констянтин Миколайович
dc.contributor.authorАльсаядех, Жаміль
dc.contributor.authorShkarupylo, Vadym V.
dc.contributor.authorTomičić, Igor
dc.contributor.authorKasyan, Konstantin M.
dc.contributor.authorAlsayaydeh, Jamil
dc.contributor.authorШкарупило, Вадим Викторович
dc.contributor.authorТомичич, Игорь
dc.contributor.authorКасьян, Константин Николаевич
dc.contributor.authorАльсаядех, Жамиль
dc.date.accessioned2018-03-15T08:55:15Z
dc.date.available2018-03-15T08:55:15Z
dc.date.issued2018
dc.descriptionShkarupylo V. V. An Approach to increase the Effectiveness of TLC Verification with Respect to the Concurrent Structure of TLA+ Specification / V. V. Shkarupylo, I. Tomičić, K. M. Kasian, J. A. J. Alsayaydeh // International Journal of Software Engineering and Computer Systems. – 2018. – Vol. 4, No. 1. – P. 48–60. doi: 10.15282/ijsecs.4.1.2018.4.0037.uk
dc.description.abstractUK: Запропоновано підхід до підвищення ефективності TLC-верифікації стосовно TLA+ специфікації з паралельною структурою. Паралелізм представлено як чергування. Досліджено два різних підходи до перевірки на моделі методом TLC. Перший підхід ґрунтується на здійсненні перевірки на моделі шляхом обходу простору станів в ширину (BFS), другий – шляхом обходу в глибину (DFS). Для аналітичного представлення TLA+ специфікацій з паралельною структурою використано структуру Кріпке. Одержано аналітичні та експериментальні оцінки використання запропонованого підходу. EN: Modern approaches to distributed software systems engineering are tightly bounded with formal methods usage. The effective way of certain method application can leverage significant outcome, in terms of corresponding time costs reduction for instance. To this end the TLC model checker has been considered – with respect to TLA+ specifications with concurrent structure. The concurrency itself has been implemented as interleaving. Two different approaches to TLC model checking have been used. The first approach is based on model checking via breadth-first state space search (BFS), the second one – via depth-first search (DFS). The main result of a paper is the new approach to increasing the effectiveness of TLC verification with respect to the concurrent structure of TLA+ specification. To analytically represent synthesized TLA+ specifications with concurrent structure, the Kripke structure has been taken. To assess the measures of state space explosion problem, taking place during the experimentation, the appropriate estimations have been proposed. These estimations have been proved during the case study. The composite web service usage scenario has been considered as a case study. The results, obtained during the experimentation, can be used to increase the effectiveness of automated TLC verification with respect to the concurrent structure of TLA+ specification. RU: Предложен подход к повышению эффективности TLC-верификации применительно к TLA+ спецификации с параллельной структурой. Параллелизм представлен как чередование. Исследованы два различных подхода к проверке на модели методом TLC. Первый подход основывается на осуществлении проверки на модели путем обхода пространства состояний в ширину (BFS), второй – путем обхода в глубину (DFS). Для аналитического представления TLA+ спецификаций с параллельной структурой использована структура Крипке. Получены аналитические и экспериментальные оценки использования предложенного подхода.uk
dc.identifier.urihttp://eir.zntu.edu.ua/handle/123456789/2938
dc.language.isoenuk
dc.publisherFaculty of Computer Systems & Software Engineering (FSKKP)uk
dc.subjectTLCuk
dc.subjectTLA+uk
dc.subjectперевірка на моделіuk
dc.subjectBFSuk
dc.subjectDFSuk
dc.subjectTLCuk
dc.subjectTLA+uk
dc.subjectModel Checkinguk
dc.subjectBFSuk
dc.subjectDFSuk
dc.subjectTLCuk
dc.subjectTLA+uk
dc.subjectпроверка на моделиuk
dc.subjectBFSuk
dc.subjectDFSuk
dc.titleAn approach to increase the effectiveness of TLC verification with respect to the concurrent structure of TLA+ specificationuk
dc.title.alternativeПідхід до підвищення ефективності TLC верифікації стосовно паралельної структури TLA+ специфікаціїuk
dc.title.alternativeПодход к повышению эффективности TLC верификации применительно к параллельной структуре TLA+ спецификацииuk
dc.typeArticleuk

Files

Original bundle
Now showing 1 - 1 of 1
Thumbnail Image
Name:
Shkarupylo_An_approach_to_increase.pdf
Size:
576.76 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

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