Модель TLA-специфікації композитного веб-сервіса з множиною динамік
Loading...
Date
2013
Journal Title
Journal ISSN
Volume Title
Publisher
Запорізький національний технічний університет
Abstract
UK: Розроблено формальну модель специфікування властивостей композитних веб-сервісів на основі формалізму темпоральної логіки TLA. На окремому прикладі виконано верифікацію TLA-специфікації композитного веб-сервіса із множиною властивостей в автоматизованому режимі з використанням реалізації методу Model Checking у складі програмного засобу TLA Toolbox (TLC, TLA Checker). Проведено оцінювання супутніх витрат часу.
RU: Разработана формальная модель специфицирования свойств композитных веб-сервисов на основе формализма темпоральной логики TLA. На отдельном примере выполнена верификация TLA-спецификации композитного веб-сервиса с множеством свойств в автоматизированном режиме с использованием реализации метода Model Checking в составе программного средства TLA Toolbox (TLC, TLA Checker). Проведена оценка сопутствующих временных издержек.
EN: Despite the fact that today we have plenty of formal methods to be used during engineering process, the question of automation is still open and there is still the need to reduce Validation costs. In order to specify the behaviors of Composite Web Service the TLA-formalism has been chosen and, as a consequence, the TLA-verification problem definition has been given. TLA-based Model for the Composite Web Services functional properties formal specification has been proposed: Kripke structure has been chosen as the basis. As a Case Study the Verification of Multi-behavioral Composite Web Service TLA-specification has been conducted. It has been done in an automated manner by TLA Toolbox Model Checking method implementation (TLC, TLA Checker) usage. The associated time costs estimation has been conducted.
Description
Шкарупило В.В. Модель TLA-спецификации композитного веб-сервиса с множеством динамик / В.В. Шкарупило // Радіоелектроніка, інформатика, управління. – Запоріжжя : ЗНТУ, 2013. – Вип. 1 (28). – С. 94 – 100.
Keywords
модель, композитний веб-сервіс, формальна специфікація, верифікація, Model Checking, TLC, Model, Composite Web Service, Formal Specification, TLA, Verification, Model Checking, формальная спецификация, верификация