Browsing by Author "Shkarupylo, Vadym V."
Now showing 1 - 20 of 23
Results Per Page
Sort Options
Item An approach to increase the effectiveness of TLC verification with respect to the concurrent structure of TLA+ specification(Faculty of Computer Systems & Software Engineering (FSKKP), 2018) Шкарупило, Вадим Вікторович; Томічич, Ігор; Касьян, Констянтин Миколайович; Альсаядех, Жаміль; Shkarupylo, Vadym V.; Tomičić, Igor; Kasyan, Konstantin M.; Alsayaydeh, Jamil; Шкарупило, Вадим Викторович; Томичич, Игорь; Касьян, Константин Николаевич; Альсаядех, ЖамильUK: Запропоновано підхід до підвищення ефективності TLC-верифікації стосовно TLA+ специфікації з паралельною структурою. Паралелізм представлено як чергування. Досліджено два різних підходи до перевірки на моделі методом TLC. Перший підхід ґрунтується на здійсненні перевірки на моделі шляхом обходу простору станів в ширину (BFS), другий – шляхом обходу в глибину (DFS). Для аналітичного представлення TLA+ специфікацій з паралельною структурою використано структуру Кріпке. Одержано аналітичні та експериментальні оцінки використання запропонованого підходу. EN: Modern approaches to distributed software systems engineering are tightly bounded with formal methods usage. The effective way of certain method application can leverage significant outcome, in terms of corresponding time costs reduction for instance. To this end the TLC model checker has been considered – with respect to TLA+ specifications with concurrent structure. The concurrency itself has been implemented as interleaving. Two different approaches to TLC model checking have been used. The first approach is based on model checking via breadth-first state space search (BFS), the second one – via depth-first search (DFS). The main result of a paper is the new approach to increasing the effectiveness of TLC verification with respect to the concurrent structure of TLA+ specification. To analytically represent synthesized TLA+ specifications with concurrent structure, the Kripke structure has been taken. To assess the measures of state space explosion problem, taking place during the experimentation, the appropriate estimations have been proposed. These estimations have been proved during the case study. The composite web service usage scenario has been considered as a case study. The results, obtained during the experimentation, can be used to increase the effectiveness of automated TLC verification with respect to the concurrent structure of TLA+ specification. RU: Предложен подход к повышению эффективности TLC-верификации применительно к TLA+ спецификации с параллельной структурой. Параллелизм представлен как чередование. Исследованы два различных подхода к проверке на модели методом TLC. Первый подход основывается на осуществлении проверки на модели путем обхода пространства состояний в ширину (BFS), второй – путем обхода в глубину (DFS). Для аналитического представления TLA+ спецификаций с параллельной структурой использована структура Крипке. Получены аналитические и экспериментальные оценки использования предложенного подхода.Item Development of stratified approach to software defined networks simulation(Приватне підприємство "Технологічний Центр", 2017) Шкарупило, Вадим Вікторович; Скрупський, Степан Юрійович; Олійник, Андрій Олександрович; Колпакова, Тетяна Олексіївна; Shkarupylo, Vadym V.; Skrupsky, Stepan Y.; Oliinyk, Andriy O.; Kolpakova, Tetiana O.; Шкарупило, Вадим Викторович; Скрупский, Степан Юрьевич; Олейник, Андрей Александрович; Колпакова, Татьяна АлексеевнаUK: Запропоновано стратифікований підхід до імітаційного моделювання програмно-конфігурованих мереж. Запропоновано імітаційні моделі мережі, активних і пасивних компонентів – контролера, комутатора, хоста та комунікаційних каналів. Придатність підходу до цільового використання підтверджено шляхом співставлення одержаних результатів імітаційного моделювання із результатами емуляції мережі у середовищі Mininet EN: The stratified approach to software defined networks simulation has been proposed. It is based on Discrete Event System Specification formalism, atomic and coupled models concepts usage. The approach is aimed at simulation within the Windows environment, with an accent on the easiness of model reconfiguration. The proposed approach is also devoted to simulation-related overheads decrease. The atomic models of active (controller, switch, host) and passive (link) network components have been proposed. The coupled model of a software defined network comprising atomic models of active and passive components has been proposed. The estimations of the resulting coupled model complexity, with respect to the number of components basic atomic models, have been given. During experimentation, the pingall command usage scenario has been considered. For this purpose, the emulation via Mininet environment and the simulation on a basis of the proposed approach have been conducted. It has been shown that discrete-event simulation on a basis of the proposed approach is significantly less time-consuming. During the approach usage within the Windows environment, the absence of the need to utilize the Xming X Server and PuTTY utility for the purpose of visualization has been faced. The validity of the approach has been proven on a basis of the obtained experimental data. The adequacy of the resulting coupled simulation model of the network has been proven with t-criterion. The proposed approach can be used for the purpose of software defined networks validation with an accent on non-functional properties. RU: Предложен стратифицированный подход к имитационному моделированию программно-конфигурируемых сетей. Предложены имитационные модели сети, активных и пассивных компонентов – контроллера, коммутатора, хоста и коммуникационных каналов. Пригодность подхода к целевому использованию подтверждена путем сопоставления полученных результатов имитационного моделирования с результатами эмулирования сети в среде MininetItem DEVS-орієнтована методика валідації композитних веб-сервісів(Запорізький національний технічний університет, 2015) Шкарупило, Вадим Вікторович; Шкарупило, Вадим Викторович; Shkarupylo, Vadym V.; Кудерметов, Равіль Камілович; Кудерметов, Равиль Камилович; Kudermetov, Ravil K.; Польська, Ольга Володимирівна; Польская, Ольга Владимировна; Polska, Olga V.UK: Запропоновано методику валідації композитних веб-сервісів за рахунок синтезу імітаційних дискретно-подійних моделей на основі формалізму DEVS. Це дозволяє виконувати автоматизовану перевірку придатності таких систем до цільового використання при проектуванні шляхом імітаційного моделювання. В якості вхідних даних використано формальну специфікацію на основі темпоральної логіки TLA, що дозволяє математично строго представляти функціональні характеристики композитних сервісів у форматі обчислювальних процесів. За аналітичну модель в основі TLA-специфікації взято структуру Кріпке. У межах методики запропоновано правила синтезу із вихідної TLA-специфікації DEVS-моделі композитного сервісу, призначеної бути засобом валідації. Результуюча DEVS-модель складається із моделей атомарних сервісів, моделі клієнта композитного сервісу та моделі координатора атомарних сервісів, що функціонує згідно специфікації WS-BPEL. Для перевірки методики проведено експериментальні дослідження, що підтвердили адекватність результуючої DEVS-моделі. Перевірку здійснено згідно запропонованого підходу, що полягає у порівнянні результатів валідації шляхом імітаційного моделювання із результатами валідації шляхом тестування. За результатами проведених досліджень обґрунтовано доцільність використання запропонованої методики при проектуванні композитних сервісів, що базується на зменшенні часових витрат на валідацію. Наголошено на доречності використання методики при ітераційній розробці. EN: A technique for Composite Web Services validity checking has been proposed. It is based on discrete-event DEVS-models synthesis, which provides the ability to conduct the automated validation by way of simulation during the design process. Temporal Logic of Actions has been chosen as the basis for input data – formal specification of Composite Web Service. It allows to specify the functional properties of such systems mathematically strictly. Functional properties has been represented as computational processes. The Kripke structure has been used as TLA-specification analytical model. Our technique leans on the proposed rules, aimed at simulation DEVS-model synthesis from given TLA-specification. The resulting coupled Composite Web Service DEVS-model consists of atomic web services models, model of client, simulated as job-requests generator, and coordinator model. Coordinator represents the WS-BPEL-engine, functioning in accordance with centralized orchestration model. A case study has been conducted to verify the proposed technique. Its artifacts confirmed the adequacy of resulting DEVS-model. The technique verification is based on the proposed approach: simulation-driven validation results are compared with the ones, obtained with test-driven validation. Technique expediency has been grounded by Composite Web Services validity checking time costs reduction. RU: Предложена методика валидации композитных веб-сервисов путем синтеза имитационных дискретно-событийных моделей на основе формализма DEVS. Это позволяет осуществлять автоматизированную проверку пригодности таких систем к целевому использованию при проектировании путем имитационного моделирования. В качестве входных данных использована формальная спецификация на основе темпоральной логики TLA, что позволяет математически строго представлять функциональные характеристики композитных сервисов в формате вычислительных процессов. В качестве аналитической модели в основе TLA-спецификации взята структура Крипке. В рамках методики предложены правила синтеза из исходной TLA-спецификации DEVS-модели композитного сервиса, предназначенной быть средством валидации. Результирующая DEVS-модель состоит из моделей атомарных сервисов, модели клиента композитного сервиса и модели координатора атомарных сервисов, функционирующего согласно спецификации WS-BPEL. Для проверки методики проведены экспериментальные исследования, подтвердившие адекватность результирующей DEVS-модели. Проверка выполнена согласно предложенному подходу, состоящему в сравнении результатов валидации путем имитационного моделирования с результатами валидации путем тестирования. По результатам проведенных исследований обоснована целесообразность использования предложенной методики при проектировании композитных сервисов, которая заключается в уменьшении временных затрат на валидацию. Акцентировано внимание на уместности использования методики при итерационной разработке.Item The investigation of TLC model checker properties(University of Zagreb, Varaždin, Croatia, 2016) Шкарупило, Вадим Вікторович; Шкарупило, Вадим Викторович; Shkarupylo, Vadym V.; Томічич, Ігор; Томичич, Игорь; Tomičić, Igor; Касьян, Констянтин Миколайович; Касьян, Константин Николаевич; Kasyan, Konstantin M.UK: У роботі проведено дослідження і порівняння властивостей методу перевірки на моделі TLC (TLA Checker). Розглянуто два підходи до використання методу. Перший підхід полягає в обході станів системи переходів методом обходу в ширину (BFS), другий – методом обходу в глибину (DFS). У якості моделі системи переходів використано структуру Кріпке. Проведено експериментальне дослідження, де в якості сценарію предметної області розглянуто використання композитного веб-сервісу. Одержані результати дослідження можуть бути використані для підвищення ефективності автоматизованої верифікації TLA+ специфікацій. EN: This paper presents the investigation and comparison of TLC model checking method (TLA Checker) properties. There are two different approaches to method usage which are considered. The first one consists of a transition system states attendance by breadth-first search (BFS), and the second one by depth-first search (DFS). The Kripke structure has been chosen as a transition system model. A case study has been conducted, where composite web service usage scenario has been considered. Obtained experimental results are aimed at increasing the effectiveness of TLA+ specifications automated verification. RU: В работе проведены исследование и сравнение свойств метода проверки на модели TLC (TLA Checker). Рассмотрены два подхода к использованию метода. Первый подход состоит в обходе состояний системы переходов методом обхода в ширину (BFS), второй подход – методом обхода в глубину (DFS). В качестве модели системы переходов использована структура Крипке. Проведено экспериментальное исследование, где в качестве сценария предметной области рассмотрено использование композитного веб-сервиса. Полученные результаты исследования могут быть использованы для повышения эффективности автоматизированной верификации TLA+ спецификаций.Item The system for control and accounting of working time(Faculty of Management Science and Informatics University of Zilina, 2017) Плахтій, Анастасія Михайлівна; Шкарупило, Вадим Вікторович; Бєліков, Сергій Борисович; Plakhtii, Anastasiia M.; Shkarupylo, Vadym V.; Byelikov, Sergey B.; Плахтий, Анастасия Михайловна; Шкарупило, Вадим Викторович; Беликов, Сергей БорисовичUK: Проведено порівняльний аналіз існуючих систем обліку робочого часу для висування вимог до власної системи. Створено специфікацію вимог програмного забезпечення системи контролю і обліку робочого часу. Проаналізовано залежності між компонентами запропонованого рішення. Для цього було використано інструментарій Electron. На основі результатів проведеного аналізу розроблено систему контролю і обліку робочого часу. Запропонована система є кросплатформним рішенням, що дозволяє контролювати та вести облік діяльності співробітника упродовж робочого часу. EN: The comparative analysis of existing timesheet systems for creating a number of requirements to own solution has been conducted. Software requirements specification for working time control and accounting system (time tracking) has been created. The dependencies between the components of proposed solution have been analyzed. For this purpose, the Electron framework has been used. Basing on the results of the analysis conducted the system for working time control and accounting has been proposed. The proposed system is a cross-platform solution that allows to control and account the activity of employee during the working time. RU: Проведен сравнительный анализ существующих систем учета рабочего времени для выдвижения требований к собственной системе. Создано спецификацию требований программного обеспечения системы контроля и учета рабочего времени. Проанализированы зависимости между компонентами предложенного решения. Для этого был использован инструментарий Electron. На основе результатов проведенного анализа разработана система контроля и учета рабочего времени. Предложенная система является кроссплатформенным решением, которое позволяет контролировать и вести учет деятельности сотрудника в течении рабочего времени.Item WS-BPEL-модифікація методу TLC-верифікації(ЧП "Технологический Центр", 2013) Шкарупило, Вадим Вікторович; Shkarupylo, Vadym V.; Шкарупило, Вадим Викторович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-обходов.Item Комплексный подход к автоматизации композиции веб-сервисов(ЧНУ ім. Ю. Федьковича, 2011) Шкарупило, Вадим Вікторович; Shkarupylo, Vadym V.; Шкарупило, Вадим Викторович; Кудерметов, Равіль Камілович; Kudermetov, Ravil K.; Кудерметов, Равиль КамиловичUK: Проведено аналіз проблеми автоматизації композиції веб-сервісів. Запропоновано критерії аналізу під-ходів до автоматизації композиції веб-сервісів. На основі запропонованих критеріїв розроблено підхід, що передбачає виконання формальної специфікації композиції на мові темпоральної логіки TLA та акцентуєть-ся на аспектах верифікації, валідації та планування. EN: The analysis of Web Service Composition automation challenge has been conducted. The criterions for the analysis of approaches to Web Service Composition automation have been proposed. The approach based on these criterions has been developed. The approach envisages composition formal specification by using TLA temporal logic and covers the aspects of verification, validation and planning. RU: Проведен анализ проблемы автоматизации композиции сервисов. Предложены критерии анализа подходов к автоматизации композиции сервисов. На основе предложенных критериев разработан подход, предполагающий выполнение формальной спецификации композиции на языке темпоральной логики TLA и акценти-рующийся на аспектах верификации, валида-ции и планирования.Item Концептуальна модель процесу автоматизованого синтезу композитних веб-сервісів(Донецький національний технічний університет, 2012) Шкарупило, Вадим Вікторович; Shkarupylo, Vadym V.; Шкарупило, Вадим Викторович; Кудерметов, Равіль Камілович; Kudermetov, Ravil K.; Кудерметов, Равиль Камилович; Паромова, Тетяна Олександрівна; Paromova, Tetyana O.; Паромова, Татьяна АлександровнаUK: Запропоновано концептуальну модель процесу автоматизованого синтезу композитних веб-сервісів. Модель процесу представлена як послідовність етапів концептуалізації, специфікації, верифікації та валідації. Модель композитного веб-сервіса представлена як ієрархічна система з функціональними та нефункціональними характеристиками. EN: The conceptual model of automated Composite Web Services synthesis process has been proposed. Process model has been represented as the sequence of steps: Conceptualizing, Specification, Verification & Validation. Composite Web Service model has been represented as hierarchical system with functional and nonfunctional properties. RU: Предложена концептуальная модель процесса автоматизированного синтеза композитных веб-сервисов. Модель процесса представлена как последовательность этапов концептуализации, специфицирования, верификации и валидации. Модель композитного веб-сервиса представлена как иерархическая система с функциональными и нефункциональными характеристиками.Item Лабораторні роботи з дисципліни "Алгоритми та методи обчислень"(Запорізький національний технічний університет, 2017) Шкарупило, Вадим Вікторович; Голуб, Тетяна Василівна; Щербак, Наталія Володимирівна; Shkarupylo, Vadym V.; Golub, Tatiyna V.; Shcherbak, Natalya V.; Шкарупило, Вадим Викторович; Голуб, Татьяна Васильевна; Щербак, Наталья ВладимировнаUK: Наведено методичні рекомендації та вказівки до виконання лабораторних робіт з дисципліни "Алгоритми та методи обчислень" EN: The methodical recommendations and instructions for laboratory works on "Algorithms and computational methods" discipline are given RU: Приведены методические рекомендации и указания по выполнению лабораторных работ по дисциплине "Алгоритмы и методы вычислений"Item Лабораторні роботи з паралельних та розподілених обчислень. Багатопоточне програмування у С++ та Java. Потоки у паралельних та векторних обчисленнях(2018) Кудерметов, Равіль Камілович; Шкарупило, Вадим Вікторович; Польська, Ольга Володимирівна; Kudermetov, Ravil K.; Shkarupylo, Vadym V.; Polska, Olga V.; Кудерметов, Равиль Камилович; Шкарупило, Вадим Викторович; Польская, Ольга ВладимировнаUK: Наведені методичні матеріали та вказівки до виконання лабораторних робіт з дисципліни " Паралельні та розподілені обчислення ". EN: The methodical materials and instructions for implementation of laboratory work on discipline "Parallel and distributed computing ". RU: Приведены методические материалы и указания к выполнению лабораторных работ по дисциплине "Параллельные и распределенные вычисления".Item Лабораторні роботи з паралельних та розподілених обчислень. Паралельні обчислення з використанням технології MPI. Паралельні обчислення з використанням технології OpenMP.(Запорізький національний технічний університет, 2020) Кудерметов, Равіль Камілович; Шкарупило, Вадим Вікторович; Польська, Ольга Володимирівна; Kudermetov, Ravil K.; Shkarupylo, Vadym V.; Polska, Olga V.; Кудерметов, Равиль Камилович; Шкарупило, Вадим Викторович; Польская, Ольга ВладимировнаUK: Наведені методичні матеріали та вказівки до виконання лабораторних робіт з дисципліни «Паралельні та розподілені обчислення». EN: The methodical materials and instructions for implementation of laboratory work on discipline «Parallel and distributed computing». RU: Приведены методические материалы и указания к выполнению лабораторных работ по дисциплине «Параллельные и распределенные вычисления».Item Методичні вказівки до виконання лабораторних робіт з дисципліни "WEB-програмування" для студентів спеціальності 122 "Комп'ютерні науки" всіх форм навчання(Національний університет «Запорізька політехніка», 2019) Скрупський, Степан Юрійович; Шкарупило, Вадим Вікторович; Skrupsky, Stepan Y.; Shkarupylo, Vadym V.; Скрупский, Степан Юрьевич; Шкарупило, Вадим ВикторовичUK: Наведено методичні вказівки до виконання лабораторних робіт для ознайомлення з підходами та технологіями, що використовуються для розмітки сучасних веб-сторiнок, зі специфікаціями SOAP та XML-RPC, отримання базових навичок роботи з бібліотекою REACT, а також ознайомлення з архітектурним стилем REST і технологією GRAPHQL. EN: Methodical instructions for laboratory works to familiarize with the approaches and technologies used for marking up modern web pages, with SOAP and XML-RPC specifications, obtaining basic skills for working with the REACT library, as well as familiarization with the REST architectural style and GRAPHQL technology have been proposed RU: Приведены методические указания к лабораторным работам для ознакомления с подходами и технологиями, используемыми для разметки современных веб-страниц, со спецификациями SOAP и XML-RPC, получение базовых навыков работы с библиотекой REACT, а также ознакомление с архитектурным стилем REST и технологии GRAPHQL.Item Методичні вказівки до виконання лабораторних робіт з дисципліни "Інженерія програмного забезпечення" (I частина)(Запорізький національний технічний університет, 2015) Шкарупило, Вадим Вікторович; Шкарупило, Вадим Викторович; Shkarupylo, Vadym V.; Ільяшенко, Матвій Борисович; Ильяшенко, Матвей Борисович; Iliashenko, Matvii B.; Польська, Ольга Володимирівна; Польская, Ольга Владимировна; Polska, Olga V.UK: Методичні вказівки присвячені роботі із бібліотекою модульного тестування JUnit, системою контролю версій Subversion (SVN) та технологією JAX-WS. EN: Methodical instructions are aimed at work with JUnit library, Subversion control system (SVN) and JAX-WS technology. RU: Методические указания посвящены работе с библиотекой модульного тестирования JUnit, системой контроля версий Subversion (SVN) и технологией JAX-WS.Item Методичні вказівки до лабораторних робіт з дисципліни "Грід обчислення та хмарні технології" для студентів спеціальності 123 "Комп'ютерна інженерія" всіх форм навчання(Запорізький національний технічний університет, 2018) Скрупський, Степан Юрійович; Skrupsky, Stepan Y.; Скрупский, Степан Юрьевич; Шкарупило, Вадим Вікторович; Shkarupylo, Vadym V.; Шкарупило, Вадим ВикторовичUK: Наведено методичні вказівки до виконання лабораторних робіт з дисципліни "Грід обчислення та хмарні технології" EN: Methodical instructions to the performance of laboratory works on discipline "Grid computing and cloud technologies" have been proposed RU: Приведены методические указания к выполнению лабораторных работ по дисциплине "Грид вычисления и облачные технологии"Item Методичні вказівки до лабораторних робіт з дисципліни «Основи теорії інтелектуальних систем». I частина.(Запорізький національний технічний університет, 2018) Тягунова, Марія Юріївна; Зеленьова, Ірина Яківна; Шкарупило, Вадим Вікторович; Tyagunova, Mary Y.; Zeleneva, Irina Ya.; Shkarupylo, Vadym V.; Тягунова, Мария Юрьевна; Зеленева, Ирина Яковлевна; Шкарупило, Вадим ВикторовичUK: Наведено методичні рекомендації щодо виконання лабораторних робіт з дисципліни «Основи теорії інтелектуальних систем» EN: The methodical recommendations for laboratory work on discipline "Intellectual systems’ fundamentals of the theory". RU: Приведены методические рекомендации по выполнению лабораторных работ по дисциплине «Основы теории интеллектуальных систем»Item Методичні вказівки до лабораторних робіт з дисципліни «Основи теорії інтелектуальних систем». II частина.(Запорізький національний технічний університет, 2018) Тягунова, Марія Юріївна; Зеленьова, Ірина Яківна; Шкарупило, Вадим Вікторович; Tyagunova, Mary Y.; Zeleneva, Irina Ya.; Shkarupylo, Vadym V.; Тягунова, Мария Юрьевна; Зеленева, Ирина Яковлевна; Шкарупило, Вадим ВикторовичUK: Наведено методичні рекомендації щодо виконання лабораторних робіт з дисципліни «Основи теорії інтелектуальних систем» EN: The methodical recommendations for laboratory work on discipline "Intellectual systems’ fundamentals of the theory". RU: Приведены методические рекомендации по выполнению лабораторных работ по дисциплине «Основы теории интеллектуальных систем»Item Методичні вказівки до лабораторних робіт з дисципліни «Основи Інтернету речей» Частина 1(Запорізький національний технічний університет, 2019) Тіменко, Артур Валентинович; Timenko, Artur V.; Тіменко, Артур Валентинович; Тягунова, Марія Юріївна; Tiahunova, Mariia Yu.; Тягунова, Мария Юрьевна; Кудерметов, Равіль Камілович; Kudermetov, Ravil K.; Кудерметов, Равиль Камилович; Шкарупило, Вадим Вікторович; Shkarupylo, Vadym V.; Шкарупило, Вадим ВикторовичUK: Наведено рекомендації та завдання для виконання лабораторних робіт з дисципліни «Основи Інтернету речей» EN: The methodical recommendations for test on discipline " Basics Internet of things ". RU: Приведены методические рекомендации по выполнению контрольных работ по дисциплине «Основы Интернета вещей»Item Методичні вказівки до лабораторних робіт з дисципліни «Основи Інтернету речей» Частина 2(Запорізький національний технічний університет, 2019) Тіменко, Артур Валентинович; Timenko, Artur V.; Тіменко, Артур Валентинович; Тягунова, Марія Юріївна; Tiahunova, Mariia Yu.; Тягунова, Мария Юрьевна; Кудерметов, Равіль Камілович; Kudermetov, Ravil K.; Кудерметов, Равиль Камилович; Шкарупило, Вадим Вікторович; Shkarupylo, Vadym V.; Шкарупило, Вадим ВикторовичUK: Наведено рекомендації та завдання для виконання лабораторних робіт з дисципліни «Основи Інтернету речей» EN: The methodical recommendations for test on discipline " Basics Internet of things ". RU: Приведены методические рекомендации по выполнению контрольных работ по дисциплине «Основы Интернета вещей»Item Модель TLA-специфікації композитного веб-сервіса з множиною динамік(Запорізький національний технічний університет, 2013) Шкарупило, Вадим Вікторович; Шкарупило, Вадим Викторович; Shkarupylo, Vadym V.UK: Розроблено формальну модель специфікування властивостей композитних веб-сервісів на основі формалізму темпоральної логіки TLA. На окремому прикладі виконано верифікацію TLA-специфікації композитного веб-сервіса із множиною властивостей в автоматизованому режимі з використанням реалізації методу Model Checking у складі програмного засобу TLA Toolbox (TLC, TLA Checker). Проведено оцінювання супутніх витрат часу. RU: Разработана формальная модель специфицирования свойств композитных веб-сервисов на основе формализма темпоральной логики TLA. На отдельном примере выполнена верификация TLA-спецификации композитного веб-сервиса с множеством свойств в автоматизированном режиме с использованием реализации метода Model Checking в составе программного средства TLA Toolbox (TLC, TLA Checker). Проведена оценка сопутствующих временных издержек. EN: Despite the fact that today we have plenty of formal methods to be used during engineering process, the question of automation is still open and there is still the need to reduce Validation costs. In order to specify the behaviors of Composite Web Service the TLA-formalism has been chosen and, as a consequence, the TLA-verification problem definition has been given. TLA-based Model for the Composite Web Services functional properties formal specification has been proposed: Kripke structure has been chosen as the basis. As a Case Study the Verification of Multi-behavioral Composite Web Service TLA-specification has been conducted. It has been done in an automated manner by TLA Toolbox Model Checking method implementation (TLC, TLA Checker) usage. The associated time costs estimation has been conducted.Item Модифицированый метод распознавания текста на стандартизированном изображении(ЧП "Технологический Центр", 2015) Касьян, Констянтин Миколайович; Касьян, Константин Николаевич; Kasyan, Konstantin M.; Братчиков, Володимир Володимирович; Братчиков, Владимир Владимирович; Bratchykov, Volodymyr V.; Шкарупило, Вадим Вікторович; Шкарупило, Вадим Викторович; Shkarupylo, Vadym V.UK: Розроблено модифікований метод розпізнавання стандартизованого тексту на зображенні. Виділені етапи обробки зображення перед використанням методу: перетворення зображення в чорно-біле, виправлення спотворень символів, детектування окремих символів. Розпізнавання символів здійснено нейронною мережею за допомогою методу шаблонів. Представлені два варіанти рішення поставленої задачі – перший типовий, другий модифікований. В результаті проведених експериментів підтверджується ефективність модифікованого методу. EN: OCR images of very topical problem of modern search engines. There are many different methods and techniques for OCR. This article presents a method for recognizing text in a standardized image. Standardized image has a single font, same size characters, a certain order of their writing, such as the serial number. In this paper we developed an improved method for recognizing text from the image. This improvement is in the preliminary finding of the same characters. First, the image area highlighted with symbols. Individual characters are compared with each other. Identical symbols are recognized only once. After recognizing characters collocate in their places. Image processing and used as borders by JavaCV. This method was compared to the standard method of OCR template method. Both methods were implemented in Java. To create a program was constructed neural network. This neural network consists of a single layer perceptron. According to the results of the tests showed the superiority of this method over the original. In the best case, the modified method is faster than 300%. In the worst case it is only slowly at 5 to 10%. Also, the modified algorithm requires less time to three iterations. RU: Разработан модифицированный метод распознавания текста на изображении. Выделены этапы обработки изображения перед применением метода: преобразование изображения, исправление искажений, детектирование символов. Распознавание символов осуществлено нейронной сетью с помощью метода шаблонов. Представлены два варианта решения поставленной задачи – первый реализован по известному алгоритму, второй модифицированный. В результате проведенных экспериментов подтверждается эффективность модифицированного метода.