МОДЕЛЬ TLA-СПЕЦИФИКАЦИИ КОМПОЗИТНОГО ВЕБ-СЕРВИСА С МНОЖЕСТВОМ ДИНАМИК

V. V. Shkarupylo

Анотація


Разработана формальная модель специфицирования свойств композитных веб-сервисов на основе формализма темпоральной логики 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в посилання на журнал є обов’язковим.