МОДЕЛЬ TLA-СПЕЦИФИКАЦИИ КОМПОЗИТНОГО ВЕБ-СЕРВИСА С МНОЖЕСТВОМ ДИНАМИК
Анотація
Разработана формальная модель специфицирования свойств композитных веб-сервисов на основе формализма темпоральной логики TLA. На отдельном примере выполнена верификация TLA-спецификации композитного веб-сервиса с множеством свойств в автоматизированном режиме с использованием реализации метода Model Checking в составе программного средства TLA Toolbox (TLC, TLA Checker). Проведена оценка сопутствующих временных издержек.
Ключові слова
модель, композитный веб-сервис, формальная спецификация, TLA, верификация, Model Checking, TLC
Повний текст:
PDF (Russian)
Адреса редакції журналу:
Редакція журналу «РІУ», Запорізький національний технічний університет,
вул. Жуковського, 64, м. Запоріжжя, 69063, Україна.
Телефон: 0 (61) 769-82-96 – редакційно-видавничий відділ
E-mail: rvv@zntu.edu.ua
При повному або частковому використаннi матерiалiв посилання на журнал є обов’язковим.