WS-BPEL-модифікація методу TLC-верифікації
EIRZNTU - Electronic Institutional Repository of Zaporizhzhia National Technical University
Переглянути архів Інформація| Поле | Співвідношення | |
| Title |
WS-BPEL-модифікація методу TLC-верифікації
WS-BPEL-modification of TLC-verification method WS-BPEL-модификация метода TLC-верификации |
|
| Creator |
Шкарупило, Вадим Вікторович
Shkarupylo, Vadym V. Шкарупило, Вадим Викторович |
|
| Subject |
композитний веб-сервіс
WS-BPEL специфікація структура Кріпке TLC верифікація стратифікація Composite Web Service WS-BPEL Specification Kripke structure TLC Verification Stratification композитный веб-сервис WS-BPEL спецификация структура Крипке TLC верификация стратификация |
|
| Description |
Шкарупило В.В. WS-BPEL-модификация метода TLC-верификации / В.В. Шкарупило // Восточно-европейский журнал передовых технологий. – Харьков : ЧП "Технологический центр", 2013. – Том 4, № 2 (64). – С. 23 – 28.
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-обходов. |
|
| Date |
2015-03-23T11:24:31Z
2015-03-23T11:24:31Z 2013 |
|
| Type |
Article
|
|
| Identifier |
1729-3774
http://eir.zntu.edu.ua/handle/123456789/186 |
|
| Language |
ru
|
|
| Publisher |
ЧП "Технологический Центр"
|
|