Модель TLA-специфікації композитного веб-сервіса з множиною динамік
EIRZNTU - Electronic Institutional Repository of Zaporizhzhia National Technical University
Переглянути архів Інформація| Поле | Співвідношення | |
| Title |
Модель TLA-специфікації композитного веб-сервіса з множиною динамік
Модель TLA-спецификации композитного веб-сервиса с множеством динамик A model of multi-behavioral composite web service TLA-specification |
|
| Creator |
Шкарупило, Вадим Вікторович
Шкарупило, Вадим Викторович Shkarupylo, Vadym V. |
|
| Subject |
модель
композитний веб-сервіс формальна специфікація верифікація Model Checking TLC Model Composite Web Service Formal Specification TLA Verification Model Checking формальная спецификация верификация |
|
| Description |
Шкарупило В.В. Модель TLA-спецификации композитного веб-сервиса с множеством динамик / В.В. Шкарупило // Радіоелектроніка, інформатика, управління. – Запоріжжя : ЗНТУ, 2013. – Вип. 1 (28). – С. 94 – 100.
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. |
|
| Date |
2015-03-18T10:55:13Z
2015-03-18T10:55:13Z 2013 |
|
| Type |
Article
|
|
| Identifier |
http://eir.zntu.edu.ua/handle/123456789/79
|
|
| Language |
ru
|
|
| Publisher |
Запорізький національний технічний університет
|
|