WS-BPEL-модифікація методу TLC-верифікації
| dc.contributor.author | Шкарупило, Вадим Вікторович | |
| dc.contributor.author | Shkarupylo, Vadym V. | |
| dc.contributor.author | Шкарупило, Вадим Викторович | |
| dc.date.accessioned | 2015-03-23T11:24:31Z | |
| dc.date.available | 2015-03-23T11:24:31Z | |
| dc.date.issued | 2013 | |
| dc.description | Шкарупило В.В. WS-BPEL-модификация метода TLC-верификации / В.В. Шкарупило // Восточно-европейский журнал передовых технологий. – Харьков : ЧП "Технологический центр", 2013. – Том 4, № 2 (64). – С. 23 – 28. | uk |
| dc.description.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-обходов. | uk |
| dc.identifier.issn | 1729-3774 | |
| dc.identifier.uri | http://eir.zntu.edu.ua/handle/123456789/186 | |
| dc.language.iso | ru | uk |
| dc.publisher | ЧП "Технологический Центр" | uk |
| dc.subject | композитний веб-сервіс | uk |
| dc.subject | WS-BPEL | uk |
| dc.subject | специфікація | uk |
| dc.subject | структура Кріпке | uk |
| dc.subject | TLC | uk |
| dc.subject | верифікація | uk |
| dc.subject | стратифікація | uk |
| dc.subject | Composite Web Service | uk |
| dc.subject | WS-BPEL | uk |
| dc.subject | Specification | uk |
| dc.subject | Kripke structure | uk |
| dc.subject | TLC | uk |
| dc.subject | Verification | uk |
| dc.subject | Stratification | uk |
| dc.subject | композитный веб-сервис | uk |
| dc.subject | WS-BPEL | uk |
| dc.subject | спецификация | uk |
| dc.subject | структура Крипке | uk |
| dc.subject | TLC | uk |
| dc.subject | верификация | uk |
| dc.subject | стратификация | uk |
| dc.title | WS-BPEL-модифікація методу TLC-верифікації | uk |
| dc.title.alternative | WS-BPEL-modification of TLC-verification method | uk |
| dc.title.alternative | WS-BPEL-модификация метода TLC-верификации | uk |
| dc.type | Article | uk |