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 SizeFormat 
shkarupylo_art7.pdfСтатті1.06 MBAdobe PDFView/Open


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