Please use this identifier to cite or link to this item: http://eir.zntu.edu.ua/handle/123456789/79
Title: Модель TLA-специфікації композитного веб-сервіса з множиною динамік
Other Titles: Модель TLA-спецификации композитного веб-сервиса с множеством динамик
A model of multi-behavioral composite web service TLA-specification
Authors: Шкарупило, Вадим Вікторович
Шкарупило, Вадим Викторович
Shkarupylo, Vadym V.
Keywords: модель
композитний веб-сервіс
формальна специфікація
верифікація
Model Checking
TLC
Model
Composite Web Service
Formal Specification
TLA
Verification
Model Checking
формальная спецификация
верификация
Issue Date: 2013
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.
URI: http://eir.zntu.edu.ua/handle/123456789/79
Appears in Collections:Наукові статті кафедри КС та М

Files in This Item:
File Description SizeFormat 
shkarupylo_art6.pdfСтаття921.02 kBAdobe PDFView/Open


Items in DSpace are protected by copyright, with all rights reserved, unless otherwise indicated.