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

Permanent URI for this collection

https://eir.zp.edu.ua/handle/123456789/24

Browse

Browsing Наукові статті кафедри КС та М by Subject "BFS"

Now showing 1 - 2 of 2
  • Thumbnail Image
    Item
    An approach to increase the effectiveness of TLC verification with respect to the concurrent structure of TLA+ specification
    (Faculty of Computer Systems & Software Engineering (FSKKP), 2018) Шкарупило, Вадим Вікторович; Томічич, Ігор; Касьян, Констянтин Миколайович; Альсаядех, Жаміль; Shkarupylo, Vadym V.; Tomičić, Igor; Kasyan, Konstantin M.; Alsayaydeh, Jamil; Шкарупило, Вадим Викторович; Томичич, Игорь; Касьян, Константин Николаевич; Альсаядех, Жамиль
    UK: Запропоновано підхід до підвищення ефективності 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+ спецификаций с параллельной структурой использована структура Крипке. Получены аналитические и экспериментальные оценки использования предложенного подхода.
  • Thumbnail Image
    Item
    The investigation of TLC model checker properties
    (University of Zagreb, Varaždin, Croatia, 2016) Шкарупило, Вадим Вікторович; Шкарупило, Вадим Викторович; Shkarupylo, Vadym V.; Томічич, Ігор; Томичич, Игорь; Tomičić, Igor; Касьян, Констянтин Миколайович; Касьян, Константин Николаевич; Kasyan, Konstantin M.
    UK: У роботі проведено дослідження і порівняння властивостей методу перевірки на моделі 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+ спецификаций.