A MODEL OF MULTI-BEHAVIORAL COMPOSITE WEB SERVICE TLA-SPECIFICATION

V. V. Shkarupylo

Abstract


Разработана формальная модель специфицирования свойств композитных веб-сервисов на основе формализма темпоральной логики TLA. На отдельном примере выполнена верификация TLA-спецификации композитного веб-сервиса с множеством свойств в автоматизированном режиме с использованием реализации метода Model Checking в составе программного средства TLA Toolbox (TLC, TLA Checker). Проведена оценка сопутствующих временных издержек.

Keywords


модель, композитный веб-сервис, формальная спецификация, TLA, верификация, Model Checking, TLC

GOST Style Citations






DOI: http://dx.doi.org/10.15588/1607-3274-2013-1-15



Copyright (c) 2014 V. V. Shkarupylo

Creative Commons License
This work is licensed under a Creative Commons Attribution-ShareAlike 4.0 International License.

Address of the journal editorial office:
Editorial office of the journal «Radio Electronics, Computer Science, Control»,
Zaporizhzhya National Technical University, 
Zhukovskiy street, 64, Zaporizhzhya, 69063, Ukraine. 
Telephone: +38-061-769-82-96 – the Editing and Publishing Department.
E-mail: rvv@zntu.edu.ua

The reference to the journal is obligatory in the cases of complete or partial use of its materials.