Модель TLA-спецификации композитного веб-сервиса с множеством динамик — Електронна бібліотека НУ «Запорізька політехніка»

•

[На рівень вище] [Головна] [Результати пошуку]

Шкарупило В. В.
Модель TLA-спецификации композитного веб-сервиса с множеством динамик

УДК: 004.052.42
Автори: Шкарупило В. В.
Джерело: Радіоелектроніка. Інформатика. Управління
Номер журнала: № 1
Рік видання: 2013
Мова: Російська
Вид документа: Стаття періодики

Анотація:

Разработана формальная модель специфицирования свойств композитных веб-
сервисов на основе формализма темпоральной логики TLA. На отдельном примере выполнена верификация TLA-спецификации композитного веб-сервиса с множеством свойств в автоматизированном режиме с использованием реализации метода Model Checking в составе программного средства TLA Toolbox (TLC, TLA Checker). Проведена оценка сопутствующих временных издержек.

Ключові слова:

модель, композитный веб-сервис, формальная спецификация, TLA, верификация, Model Checking, TLC

Файл документа доступний читачам бібліотеки: увійдіть або зареєструйтесь.