Please use this identifier to cite or link to this item:
http://eir.zntu.edu.ua/handle/123456789/186
Title: | WS-BPEL-модифікація методу TLC-верифікації |
Other Titles: | WS-BPEL-modification of TLC-verification method WS-BPEL-модификация метода TLC-верификации |
Authors: | Шкарупило, Вадим Вікторович Shkarupylo, Vadym V. Шкарупило, Вадим Викторович |
Keywords: | композитний веб-сервіс WS-BPEL специфікація структура Кріпке TLC верифікація стратифікація Composite Web Service WS-BPEL Specification Kripke structure TLC Verification Stratification композитный веб-сервис WS-BPEL спецификация структура Крипке TLC верификация стратификация |
Issue Date: | 2013 |
Publisher: | ЧП "Технологический Центр" |
Abstract: | UK: Запропоновано модифікацію методу верифікації TLA Checker (TLC), напрямлену на зменшення часових витрат,обумовлених процесом перевірки WS-BPEL-описів композитних веб-сервісів на основі відповідних формальних TLA-моделей. Модифікація полягає у серії з BFS- та DFS-обходів. EN: To increase the confidence that Composite Web Service functional properties will correspond to our expectations the Formal Verification procedure can be conducted. In order to do that the appropriate specification formalism has to be chosen first. Temporal Logic of Actions TLA+ language usage represents the way to get compact and easily reconfigurable formal models. Broadly adopted WS-BPEL 2.0 OASIS standard can provide us with building blocks for such models retrieving. The aforementioned re-configurability is achievable by models stratification. As for transition system model the Kripke structure completely fits the domain. TLA Checker (TLC) as TLA Toolbox framework built-in component is a convenient way to get the job done. Despite that, comparing to UPPAAL tool performance for instance, the minor TLC tweaking has yet to be applied. To this end the modification of TLC-verification method has been proposed. Modification is based on TLA-models stratification coupled with the sequence of Breadth-first- (BFS) and Depth-first-searches (DFS). RU: Предложена модификация метода верификации TLA Checker (TLC), направленная на уменьшение временных издержек, обусловленных процессом проверки WS-BPEL-описаний веб-сервисов на основе соответствующих формальных TLA-моделей. Модификация заключается в серии из BFS- и DFS-обходов. |
Description: | Шкарупило В.В. WS-BPEL-модификация метода TLC-верификации / В.В. Шкарупило // Восточно-европейский журнал передовых технологий. – Харьков : ЧП "Технологический центр", 2013. – Том 4, № 2 (64). – С. 23 – 28. |
URI: | http://eir.zntu.edu.ua/handle/123456789/186 |
ISSN: | 1729-3774 |
Appears in Collections: | Наукові статті кафедри КС та М |
Files in This Item:
File | Description | Size | Format | |
---|---|---|---|---|
shkarupylo_art7.pdf | Статті | 1.06 MB | Adobe PDF | View/Open |
Items in DSpace are protected by copyright, with all rights reserved, unless otherwise indicated.