WS-BPEL-модифікація методу TLC-верифікації
Loading...
Date
2013
Journal Title
Journal ISSN
Volume Title
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.
Keywords
композитний веб-сервіс, WS-BPEL, специфікація, структура Кріпке, TLC, верифікація, стратифікація, Composite Web Service, WS-BPEL, Specification, Kripke structure, TLC, Verification, Stratification, композитный веб-сервис, WS-BPEL, спецификация, структура Крипке, TLC, верификация, стратификация