Модель TLA-специфікації композитного веб-сервіса з множиною динамік

Simple item page
dc.contributor.authorШкарупило, Вадим Вікторович
dc.contributor.authorШкарупило, Вадим Викторович
dc.contributor.authorShkarupylo, Vadym V.
dc.date.accessioned2015-03-18T10:55:13Z
dc.date.available2015-03-18T10:55:13Z
dc.date.issued2013
dc.descriptionШкарупило В.В. Модель TLA-спецификации композитного веб-сервиса с множеством динамик / В.В. Шкарупило // Радіоелектроніка, інформатика, управління. – Запоріжжя : ЗНТУ, 2013. – Вип. 1 (28). – С. 94 – 100.uk
dc.description.abstractUK: Розроблено формальну модель специфікування властивостей композитних веб-сервісів на основі формалізму темпоральної логіки 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.uk
dc.identifier.urihttp://eir.zntu.edu.ua/handle/123456789/79
dc.language.isoruuk
dc.publisherЗапорізький національний технічний університетuk
dc.subjectмодельuk
dc.subjectкомпозитний веб-сервісuk
dc.subjectформальна специфікаціяuk
dc.subjectверифікаціяuk
dc.subjectModel Checkinguk
dc.subjectTLCuk
dc.subjectModeluk
dc.subjectComposite Web Serviceuk
dc.subjectFormal Specificationuk
dc.subjectTLAuk
dc.subjectVerificationuk
dc.subjectModel Checkinguk
dc.subjectформальная спецификацияuk
dc.subjectверификацияuk
dc.titleМодель TLA-специфікації композитного веб-сервіса з множиною динамікuk
dc.title.alternativeМодель TLA-спецификации композитного веб-сервиса с множеством динамикuk
dc.title.alternativeA model of multi-behavioral composite web service TLA-specificationuk
dc.typeArticleuk

Files

Original bundle
Now showing 1 - 1 of 1
Thumbnail Image
Name:
shkarupylo_art6.pdf
Size:
921.02 KB
Format:
Adobe Portable Document Format
Description:
Стаття
Download
License bundle
Now showing 1 - 1 of 1
No Thumbnail Available
Name:
license.txt
Size:
1.71 KB
Format:
Item-specific license agreed upon to submission
Description:
Download

Collections

Наукові статті кафедри КС та М