Алгебраїчне моделювання в системах міжнародної та місцевої обслуговуючої логістики

Міжнародна та внутрішня обслуговуюча логістика розвиваються неймовірними темпами в сучасному житті, а прогнози розвитку для цієї галузі вкрай оптимістичні. З цих причин ми зіштовхнулись з задачею контролю, оптимізації та безпечної і надійної перевірки комплексних логістичних систем з великою кількіс...

Повний опис

Збережено в:
Бібліографічні деталі
Дата:2020
Автори: Летичевський, О.О., Горбатюк, С.О., Горбатюк, В.О.
Формат: Стаття
Мова:Ukrainian
Опубліковано: Інститут програмних систем НАН України 2020
Назва видання:Проблеми програмування
Теми:
Онлайн доступ:http://dspace.nbuv.gov.ua/handle/123456789/180497
Теги: Додати тег
Немає тегів, Будьте першим, хто поставить тег для цього запису!
Назва журналу:Digital Library of Periodicals of National Academy of Sciences of Ukraine
Цитувати:Алгебраїчне моделювання в системах міжнародної та місцевої обслуговуючої логістики / О.О. Летичевський, С.О. Горбатюк, В.О. Горбатюк // Проблеми програмування. — 2020. — № 4. — С. 88-97. — Бібліогр.: 9 назв. — укр.

Репозитарії

Digital Library of Periodicals of National Academy of Sciences of Ukraine
id irk-123456789-180497
record_format dspace
spelling irk-123456789-1804972021-10-01T01:25:50Z Алгебраїчне моделювання в системах міжнародної та місцевої обслуговуючої логістики Летичевський, О.О. Горбатюк, С.О. Горбатюк, В.О. Теоретичні та методологічні основи програмування Міжнародна та внутрішня обслуговуюча логістика розвиваються неймовірними темпами в сучасному житті, а прогнози розвитку для цієї галузі вкрай оптимістичні. З цих причин ми зіштовхнулись з задачею контролю, оптимізації та безпечної і надійної перевірки комплексних логістичних систем з великою кількістю внутрішніх агентів, які діють у мінливому та нестабільному середовищі. Ця робота має за мету показати як математичне моделювання, зокрема, алгебра поведінок, дає можливість передбачити поведінку та стабільність логістичних середовищ, перевірити їх властивості безпеки та надійність. Основними властивостями безпеки комплексних систем логістики різної складності та рівнів є стабільність функціонування, стійкість до зовнішніх загроз, виявлення та усунення вразливостей. При розробці програмних систем доцільно використовувати модельний підхід. Він передбачає створення моделей як інструментів на кожному етапі розробки програмного забезпечення для застосування методів верифікації, тестування та валідації. Алгебраїчні моделі логістичних систем можуть бути використані для аналізу поведінки всіх залучених агентів і доведення їх здатності виконувати свої цілі та здатності всієї системи постійно існувати та залишатися стабільною. Як приклади практичного використання розглянуто застосування на практиці алгебри поведінок на прикладі діючої закритої логістичної системи фермерського господарства. International and internal service logistics are advancing at a tremendous pace in our modern life, and future forecasts for this area are optimistic. For this reason, we face a task in the control, optimization and safety and security checking of complex logistical systems with many internal agents working in a changing environment. Our paper aims to show how mathematical modeling, especially behavior algebra, can provide an opportunity for predicting the behavior and stability of logistics environments and checking their safety and security properties. The main security properties of complex logistics systems of different capacities and levels are stability of operation, resistance to external threats and detection and elimination of vulnerabilities. During the development of software systems, it is advisable to use a model approach. It involves the creation of models as tools at every stage of software development for the application of verification, testing and validation methods. Algebraic models of logistics systems can be used to analyze the behavior of all agents involved and to prove their ability to fulfill their goals and the ability of the whole system to constantly exist and remain stable. As examples of practical use the application in practice of algebra of behaviors on an example of the operating closed logistic system of a farm is considered. 2020 Article Алгебраїчне моделювання в системах міжнародної та місцевої обслуговуючої логістики / О.О. Летичевський, С.О. Горбатюк, В.О. Горбатюк // Проблеми програмування. — 2020. — № 4. — С. 88-97. — Бібліогр.: 9 назв. — укр. 1727-4907 DOI: https://doi.org/10.15407/pp2020.04.088 http://dspace.nbuv.gov.ua/handle/123456789/180497 004.05 uk Проблеми програмування Інститут програмних систем НАН України
institution Digital Library of Periodicals of National Academy of Sciences of Ukraine
collection DSpace DC
language Ukrainian
topic Теоретичні та методологічні основи програмування
Теоретичні та методологічні основи програмування
spellingShingle Теоретичні та методологічні основи програмування
Теоретичні та методологічні основи програмування
Летичевський, О.О.
Горбатюк, С.О.
Горбатюк, В.О.
Алгебраїчне моделювання в системах міжнародної та місцевої обслуговуючої логістики
Проблеми програмування
description Міжнародна та внутрішня обслуговуюча логістика розвиваються неймовірними темпами в сучасному житті, а прогнози розвитку для цієї галузі вкрай оптимістичні. З цих причин ми зіштовхнулись з задачею контролю, оптимізації та безпечної і надійної перевірки комплексних логістичних систем з великою кількістю внутрішніх агентів, які діють у мінливому та нестабільному середовищі. Ця робота має за мету показати як математичне моделювання, зокрема, алгебра поведінок, дає можливість передбачити поведінку та стабільність логістичних середовищ, перевірити їх властивості безпеки та надійність. Основними властивостями безпеки комплексних систем логістики різної складності та рівнів є стабільність функціонування, стійкість до зовнішніх загроз, виявлення та усунення вразливостей. При розробці програмних систем доцільно використовувати модельний підхід. Він передбачає створення моделей як інструментів на кожному етапі розробки програмного забезпечення для застосування методів верифікації, тестування та валідації. Алгебраїчні моделі логістичних систем можуть бути використані для аналізу поведінки всіх залучених агентів і доведення їх здатності виконувати свої цілі та здатності всієї системи постійно існувати та залишатися стабільною. Як приклади практичного використання розглянуто застосування на практиці алгебри поведінок на прикладі діючої закритої логістичної системи фермерського господарства.
format Article
author Летичевський, О.О.
Горбатюк, С.О.
Горбатюк, В.О.
author_facet Летичевський, О.О.
Горбатюк, С.О.
Горбатюк, В.О.
author_sort Летичевський, О.О.
title Алгебраїчне моделювання в системах міжнародної та місцевої обслуговуючої логістики
title_short Алгебраїчне моделювання в системах міжнародної та місцевої обслуговуючої логістики
title_full Алгебраїчне моделювання в системах міжнародної та місцевої обслуговуючої логістики
title_fullStr Алгебраїчне моделювання в системах міжнародної та місцевої обслуговуючої логістики
title_full_unstemmed Алгебраїчне моделювання в системах міжнародної та місцевої обслуговуючої логістики
title_sort алгебраїчне моделювання в системах міжнародної та місцевої обслуговуючої логістики
publisher Інститут програмних систем НАН України
publishDate 2020
topic_facet Теоретичні та методологічні основи програмування
url http://dspace.nbuv.gov.ua/handle/123456789/180497
citation_txt Алгебраїчне моделювання в системах міжнародної та місцевої обслуговуючої логістики / О.О. Летичевський, С.О. Горбатюк, В.О. Горбатюк // Проблеми програмування. — 2020. — № 4. — С. 88-97. — Бібліогр.: 9 назв. — укр.
series Проблеми програмування
work_keys_str_mv AT letičevsʹkijoo algebraíčnemodelûvannâvsistemahmížnarodnoítamíscevoíobslugovuûčoílogístiki
AT gorbatûkso algebraíčnemodelûvannâvsistemahmížnarodnoítamíscevoíobslugovuûčoílogístiki
AT gorbatûkvo algebraíčnemodelûvannâvsistemahmížnarodnoítamíscevoíobslugovuûčoílogístiki
first_indexed 2025-07-15T20:35:45Z
last_indexed 2025-07-15T20:35:45Z
_version_ 1837746623019483136
fulltext Теоретичні і методологічні основи програмування © О.О. Летичевський, С.О. Горбатюк, В.О. Горбатюк, 2020 88 ISSN 1727-4907. Проблеми програмування. 2020. № 4 УДК004.05 https://doi.org/10.15407/pp2020.04.088 О.О. Летичевський, С.О. Горбатюк, В.О. Горбатюк АЛГЕБРАЇЧНЕ МОДЕЛЮВАННЯ В СИСТЕМАХ МІЖНАРОДНОЇ ТА МІСЦЕВОЇ ОБСЛУГОВУЮЧОЇ ЛОГІСТИКИ Міжнародна та внутрішня обслуговуюча логістика розвивається шаленими темпами у сучасному житті, а прогнози на майбутнє для цієї галузі оптимістичні. З цих причин ми постали перед задачею контро- лю, оптимізації, безпечної та надійної перевірки комплексних логістичних систем з багатьма внутріш- німи агентами, які працюють у середовищі, що змінюється. Дана робота має на меті показати як математичне моделювання, зокрема, алгебра поведінок, надає можливість передбачувати поведінку, стабільність логістичних середовищ та перевіряти їх властивості безпеки, та надійності. Ці процедури є модельно-орієнтованими розробками комплексних систем програмного забезпечення, таких як логісти- чні системи. Ключові слова: алгебра поведінок, інсерційне моделювання, формальна верифікація, ланцюг постачан- ня, модельно-орієнтовані розробки, властивості безпеки. 1. Загальна інформація Стабільність функціонування, стій- кість до зовнішніх загроз, виявлення та усунення вразливостей є необхідними вла- стивостями комплексних систем міжнаро- дної та внутрішньої обслуговуючої логіс- тики. Такі системи програмного забезпе- чення є критично важливими до безпеки та вимагають розробок з модельно-орієнтова- ним підходом для надійності. Модельний підхід до розробки передбачає створення моделей як інструментів на кожному етапі розробки програмного забезпечення для застосування методів верифікації, тесту- вання та валідації. Методи математичного моделюван- ня з такими інструментами, як алгебра по- ведінок, дають можливість керувати логіс- тичними системами та забезпечувати їх безпеку та захищеність за допомогою фо- рмальної верифікації та формалізації за допомогою тестування на основі моделей. Алгебраїчні моделі логістичних систем можуть бути використані для аналізу по- ведінки всіх залучених агентів і доведення їх здатності виконувати свої цілі та здат- ності всієї системи постійно існувати та залишатися стабільною. Формальна верифікація використо- вується в аналізі та верифікації бізнес- логістики вже декілька десятирічь. Форма- льні мови такі як: BPMN [1], UML [2], SysML [3] використовуються для опису логістичних бізнес процесів, а досить ве- лика кількість методів такі як: VDM [4], SPIN [5] та інші застосовується для пере- вірки властивостей безпеки. Ускладнення специфіки та збільшення інформаційного навантаження обумовило використання більш новітні методики та відповідні ма- тематичних теорії. У цьому дослідженні ми демон- струємо, як алгебраїчний підхід, основа- ний на алгебрі поведінок, може бути ефек- тивно використаний для перевірки власти- востей безпеки складних систем. Як прик- лади ми застосовуємо її до реальної закри- тої логістичної системи місцевого обслу- говування (фермерське господарство) та відкритої міжнародної логістичної системи (експортні поставки виробництва вищезга- даного фермерського домогосподарства). 2. Алгебра поведінок На початку 1970-х, В.М. Глушков, директор Інституту кібернетики Націона- льної академії наук України, заснував комп’ютерну наукову школу, яка сфокусу- валась на алгебраїчних методах. Тематика дослідження варіювалась від автоматизо- ваних доведень теорем до алгебраїчного моделювання та від наукових концепцій до промислових прикладних програм. Пізні- ше в 2000 Система Алгебраїчного Програ- мування (APS) [1] як складова частина цієї Теоретичні і методологічні основи програмування 89 програми досліджень розширилась за до- помогою включення в себе концепції вза- ємодії перехідних систем у деяких алгеб- раїчних середовищах. Ключова ідея – інсерційне функціонування, яке визначає поведінку взаємодії перехідних систем в алгебраїчному середовищі. Ця концепція розроблена в контексті IMS [2]. Алгебра поведінок та основні специфікації прото- колу використовується для формального опису моделі. Такі алгебраїчні інструмен- ти, як теореми та абстрактні алгоритми, служать основою для формальних методів верифікації. Алгебраїчний підхід та інсер- ційне моделювання дозволяють довести або спростувати властивості, подавши контр-приклади для системи з довільною кількістю агентів. Використовуючи фор- мальну модель програми на якомусь рівні абстракції, ми можемо генерувати різні сценарії поведінки агентів або груп аген- тів. Ці сценарії є символічними і можуть бути проілюстровані конкретними прикла- дами за допомогою формальних методів. Генерація символічних сценаріїв забезпе- чує гарне висвітлення поведінки, а отже, отримані конкретні сценарії можуть розг- лядатися як тестовий набір для створеного програмного забезпечення. Інсерційне моделювання фокусу- ється на моделях побудови та вивченні взаємодії агентів та середовищ у складних розподілених мультиагентних системах. Загальні концепції інерційного моделю- вання – це ієрархія середовищ та агентів, занурених у ці середовища, взаємодія цих агентів, середовищ та середовищ вищого рівня, двосторонній вплив агентів та сере- довищ один на одного, зміна поведінки набору агентів під час занурення в нові середовища. Середовище – це агент, який має функцію занурення. Агенти розгляда- ються як системи переходу атрибутів. У таких системах стани визначаються зна- ченнями атрибутів. Агенти мають набір атрибутів, які визначають тип агента. Ат- рибути середовища пов'язані з глобальни- ми атрибутами, які відомі всім агентам. В 1997 Гілберт та Летичевський вве- ли поняття алгебри поведінок [3] як ін- струмент та невід’ємна частина інсерційно- го моделювання. Алгебра поведінок – це універсальна алгебра двох видів. Основний різновид – це набір поведінок, а другий – сукупність дій. Ця алгебра має дві операції, три термінальні константи та відношення наближення. Операції позна- чаються префіксами a.u (де «a» – дія, а «u» – поведінка) та недетермінований вибір поведінки u + v (асоціативні, комутативні та ідемпотентні операції на множині пове- дінок). Кінцевими константами є успішно визначене ∆, заключення 0, та дивергентна поведінка ⊥. Знаходження наближеного зв’язку ⊑ є частковим порядком у наборі поведінок з мінімальним елементом ⊥. Алгебра поведінок також наповнена двома операціями: паралельними (||) та послідов- ними (;) композиціями поведінок. Одним з прикладів вираження по- ведінок є: B0 = a1.a2.B1 + a3.B2, B1 = a4, B2 =… Мається на увазі, що поведінка B0 може бути представлена, як послідовність дій а1 та а2 та поведінки В1, або як послі- довність дії а3 та поведінки В2. Поведінка В1 закінчується після дії а4 [4]. 3. Приклад формалізації системи взаємодії агентів закритої логістичної системи Розглянемо застосування на практи- ці алгебри поведінок на прикладі діючої закритої логістичної системи фермерсько- го господарства. Закрите середовище міс- тить у собі набір агентів, що мають певні атрибути, властивості та список дій, які вони виконують за певних передумов. Ко- нтроль та взаємодія агентів даної системи здійснюється за допомогою Централізова- ної бази даних (сервера), яка збирає інфор- мацію про стан кожного агента та коорди- нує їх взаємодію за допомогою команд. Централізована база даних є одним із аген- тів системи, функція якого є безперервне отримання, накопичення та обробка інфо- рмації від агентів. За умови виконання пе- вної передумови Централізована база да- них надсилає агенту сповіщення-команду (коротке сервісне повідомлення) про початок виконання певної дії. Активність Теоретичні і методологічні основи програмування 90 кожного агенту описана математичною моделлю поведінок, яка передбачає хід усіх можливих дій такого агенту. Моделю- вання поведінок усіх агентів дає змогу проаналізувати цілісну комплексну логіс- тичну систему в роботі та виявити її враз- ливості. Список основних агентів та їх дій наведено в табл. 1. Таблиця 1. Список агентів та їх дій Агент Список дій Агроном - дає команду про готовність сої для збору урожаю Комбайн (один або більше) - простій (або зупинка) - збір урожаю та вивантаження на ходу у вантажівку - технічне обслуговування - заправка - заміна водія при цілодобовій роботі позмінно Бензовоз - простій (або зупинка) - забір пального на базі - заправка транспортних засобів та механізмів у разі отримання сигналу від централізованої бази даних про низькі об’єми палива, отримані від датчиків палива цих засобів та механізмів - заміна водія при цілодобовій роботі позмінно - технічне обслуговування - заправка Вантажівка (одна або більше) - простій (або зупинка) - супровід комбайна під час збору урожаю та приймання сої на ходу - транспортування на склад та вивантаження - технічне обслуговування - заправка - заміна водія при цілодобовій роботі позмінно Склад та лінія переробки - простій (або зупинка) - приймання сої та зважування - контроль показників якості - контроль вологості та досушка, провіювання - переробка сої на соєву олію - зважування готової продукції - відвантаження готової продукції - заміна працівників при цілодобовій роботі позмінно - передача отриманої інформації на всіх етапах до ЦБД Фура - простій (або зупинка) - очікування завантажування на складі - завантажування та зважування - доставка кінцевому споживачеві (по Україні або за кордон) Сервісна слу- жба (механік) - простій (або зупинка) - виконання технічного обслуговування - заправка - заміна водія при цілодобовій роботі позмінно Централізована база даних (ЦБД) - безперервний збір та обробка інформації від GPS та інших датчиків від всіх агентів на всіх етапах - передача команд та інформації відповідним агентам - формування бази даних - опрацювання отриманої інформації на всіх етапах від агенту Склад та лінія переробки, внесення до операційної бази даних - надання інформації зацікавленим сторонам та агентам Теоретичні і методологічні основи програмування 91 Приклади запису моделей поведі- нок агентів за допомогою алгебри поведі- нок, розглянемо поведінки декількох базо- вих агентів: 1. Комбайн Cstart Conway Cwork Creturn Cstop Crepair Crepair Crepair Crefuel Crefuel Crefuel Рис. 1. Схема математичної моделі комбайну Математична поведінкова модель: C = Cstart.Conway.Cwork.Creturn.Cstop Conway = Cmove.Conway + Cmove.Crepair.Conway + Cmove.Crefuel.Conway Creturn = Cmove.Creturn + Cmove.Crepair.Creturn + Cmove.Crefuel.Creturn Cmove = (PdX.Cmove + PdY.Cmove) + Conplace. Поведінка переміщення комбайна до робочого місця Conway та назад до бази Creturn складається з поведінки циклу Cmove, що закінчується Conplace та пове- дінок ремонту Crepair та заправки Crefuel. Cwork = Cgath.Cwork + Cgath.Crepair.Cwork + + Cgath.Crefuel.Cwork Cgath = SdX.Cgath + Sdy.Cchdir.Cgath) + Send. Поведінка роботи комбайна Cwork складається з поведінки циклу Cgath, що закінчується Send та поведінок ремонту Crepair та заправки Crefuel. Crepair = Cstop.Cdamage, Поведінка ремонту комбайна Crepair є дії Cstop та Cdamage. Crefuel = Cstop.Cfuel. Поведінка заправки комбайна Crefuel є дії Cstop та Cfuel. 2. Бензовоз Fstart Fstop FonwayFready Fwork Freturn Frefill Frepair Frefuel Рис. 2. Схема математичної моделі бензовозу Математична модель поведінки: F = Fstart.Fcycle.Fstop, Fcycle = Fready.Fcycle + Fready.Fonway.Fwork.Freturn.Frefill.F cycle + Fready.Fonway.Freturn.Fcycle. Поведінка робочого циклу бензово- за Fcycle – цикл зміни дій: Fonway = Fmove.Fonway + Fmove.Frepair + Fmove.Frefuel.Fonway, Freturn = Fmove.Freturn + Fmove.Frepair.Freturn + Fmove.Frefuel.Freturn. Поведінка переміщення бензовоза до робочого місця Fonway та назад до бази Freturn складається з поведінок ремонту Frepair, заправки Frefuel та поведінки цик- лу Fmove. Fmove = (SdX.Fmove + SdY.Fmove) + Fonplace. Поведінка переміщення бензовоза до робочого місця Fmove є циклом зміни положення, що закінчується Fonplace або поведінками ремонту Frepair та заправки Frefuel. Frepair = Fstop.Fdamage, Теоретичні і методологічні основи програмування 92 Поведінка ремонту бензовоза Frepair є дії Fstop та Fdamage. Frefuel = Fstop.Ffuel.Fwork. Поведінка заправки бензовоза Frefuel є дії Fstop, Ffuel та Fwork. 3. Механік Mstart Mstop Monwa y Mready Mwork Mreturn Mrefuel Mrepair Рис. 3. Схема математичної моделі механіка. Математична модель: M = Mstart.Mcycle.Mstop Mcycle = Mready.Mcycle + Mready.Monwa y.Mwork.Mreturn.Mcycle + Mready.Monwa y.Mreturn.Mcycle Поведінка робочого циклу механіка Mcycle – цикл зміни дій Monway = Mmove.Monway + Mmove.Mrefuel+ + Mmove.Mrepair.Monway Mreturn = Mmove.Mreturn + Mmove.Mrepair.Mreturn + Mmove.Mrefuel.Mreturn Поведінка переміщення механіка до робочого місця Monway та назад до бази Mreturn складається з поведінок ремонту Mrepair, заправки Mrefuel та поведінки циклу Mmove Mmove = (SdX.Mmove + SdY.Mmove)+ + Monplace Поведінка переміщення механіка до робочого місця Mmove – цикл зміни поло- ження, що закінчується Monplace або поведінками ремонту Mrepair та заправки Mrefuel Mrepair = Mstop.Mdamage.Mwork Поведінка ремонту механіка Mrepai – дія Mstop та Mdamage Mrefuel = Mstop.Mfuel Поведінка заправки механіка Mrefuel – діяї Mstop, Mfuel та Mwork. 4. Вантажівка Рис. 4. Схема математичної моделі вантажівки. Математична модель: T = Tstart.Tonway.Twork.Treturn.Tstop Tonway = Tmove.Tonway + Tmove.Trepair.Tonway + Tmove.Trefuel.Tonway Treturn = Tmove.Treturn + Tmove.Trepair.Treturn + Tmove.Trefuel.Treturn Tmove = (PdX.Tmove + PdY.Tmove) + Tonplace Поведінка переміщення вантажівки до робочого місця Tonway та назад до ба- зи Treturn складається з поведінки циклу Tmove, що закінчується Tonplace та пове- дінок ремонту Trepair та заправки Trefuel Twork = Tgath.Twork + + Tgath.Trepair.Twork + Теоретичні і методологічні основи програмування 93 + Tgath.Trefuel.Twork + + Tgath.Tunload.Twork Tgath = (SdX.Tgath + Sdy.Tchdir.Tgath) + Send Поведінка роботи вантажівки Twork складається з поведінки цик- лу Tgath, що закінчується Send та поведі- нок ремонту Trepair та заправки Trefuel Trepair = Tstop.Tdamage Поведінка ремонту вантажівки Trepair є дії Tstop та Tdamage Trefuel = Tstop.Tfuel Поведінка заправки вантажів- ки Trefuel є дії Tstop та Tfuel Tunload = Treturn.Treload.Tonway Поведінка вигрузки вантажівки Tunload є дії Treturn, Treload та Tonway. Крім поведінок ми маємо також список дій, що можуть бути представле- ними перед- та післяумовою. Ми наводимо як приклад дії комбайну з описом відпові- дної семантики. Ми не наводимо поведін- ку інших агентів таких як склад, фура, ме- ханіка, вантажівки, централізована база даних у зв’язку з великою кількістю фор- малізації (табл. 2). Таблиця 2. Список дій та їх передумов та післяумов Наза дії Передумова Післяумова І-ція пере- ходу Коментар Cstart 1 (безумовна дія) (X==Xs) && (Y ==Ys) Початок роботи Cdamage 1<=i<=combineQuantity combine(i).state= DAMAGE send help(i) Якщо трапилась поломка відіслати сигнал про до- помогу та перейти в ста- дію DAMAGE Cstop 1<=i <= combineQuantity combine(i).state= STOP Зупинитися та перейти в стадію STOP Cfuel 1<=i<=combineQuantity) && (combine(i).fuelLevel <= 0.2 * combine(i).fuelVolume) combine(i).state = FUEL send help(i) Якщо рівень пального менше норми відіслати сигнал про допомогу та перейти в стадію FUEL PdX X < Xp X = X + deltaX Якщо не на місці приз- начення, то рухатись на якусь deltaX PdY Y < Yp Y = Y + deltaY Якщо не на місці приз- начення, то рухатись на якусь deltaY SdX ((dir > 0) && (X < XLe)) || ((dir < 0) && (X > XLs)) X = X + deltaX * dir Якщо не кінець довжини ділянки, то рухатись на якусь deltaX SdY (((dir > 0) && (X > XLe)) || ((dir < 0) && (X < XLs))) && (Y < YWe) Y = Y + deltaY Якщо кінець довжини ділянки, але не кінець ширини поля, то почина- ємо нову смугу на полі Cchdir (((dir > 0) && (X > XLe)) || ((dir < 0) && (X < XLs))) && (Y < YWe) dir = -dir Якщо кінець довжини ділянки, але не кінець ширини поля, то зміню- ємо напрямок Conplace (X == Xp) &&(Y == Yp) 1 Якщо комбайн на місці призначення Теоретичні і методологічні основи програмування 94 4. Формальна верифікація моделей Дана методика формалізації дозво- ляє застосувати далі формальні методи верифікації, таких як перевірка властивос- тей безпеки та випадки загрози для без- перервної життєдіяльності системи. Над- звичайно важливо перевіряти деякі ключо- ві фактори, які впливають на можливість виконання злагоджених дій усіх агентів системи, що в результаті і відображається в безперервній та продуктивній діяльності системи. Розглянемо основні властивості безпеки, що перевіряються в логістичній системі фермерського господарства. 1. Терміни збору врожаю. Дана вла- стивість може бути виражена формулою у базовій логічній мові, що вибрана для фо- рмалізації дій (T <= 90 днів). При розгляді довільної кількості комбайнів та обслуго- вуючого транспорту така ситуація може бути при нераціональній кількості транс- портних та стану техніки. Для перевірки властивості використовуються методи мо- делювання такі як символьне, конкретне та змішане моделювання системи. На почат- ку враховуються такі умови, як кількість допустимих несправностей техніки (як арифметична нерівність), конкретна кіль- кість одиниць техніки та відстані до місця роботи. Для визначених початкових даних проводиться конкретне моделювання та визначається властивість порушення тер- мінів збору врожаю. При використанні зворотного символьного моделювання від стану, що відповідає дотримання термінів та гіпотетичних можливих кількостей оди- ниць, несправностей та відстаней до місця роботи, можливо визначити початкові умови при яких ця властивість не буде по- рушена. Слід відмітити, що дана технологія не вирішує задачу оптимізації, а лише пе- ревіряє можливість її реалізації. Методи символьного моделювання розглянуті в [9]. 2. Достатність кількості обслугову- ючих агентів (типу бензовоз чи механік) для обслуговування життєдіяльності голо- вних агентів системи, здатність вчасно прибути до заданої точки призначення для виконання заданих Центральною базою даних дій. Дані властивості перевіряються аналогічно при висуванні деяких гіпотез при проектуванні задачі або реальної ная- вності техніки. Такі властивості також представляються за допомогою нерівнос- тей (або рівностей). 3. Перевірка злагодженості та узго- дженості алгоритмів дій агентів (напри- клад, дії бензовоза при одночасному ви- клику обслуговування декількох агентів). Дана властивість може бути виражена за допомогою алгебри поведінок. Наприклад, чи встигне бензовоз заправити всі комбай- ни, якщо вони одночасно зупиняться, за встановлений термін.Маємо властивість безпеки (T<=2 год) та саму поведінку: Cdamage.Cdamage.Cdamage.Cdamage .X;(Trepair.Trepair.Trepair.Trepair). Розглянутий приклад ілюструє по- ведінку чотирьох комбайнів, які мали не- справність та були полагоджені за деякий час. Чи відповідає цей час встановленому- визначає конкретне або змішане моделю- вання. Зауважимо, що при символьному моделюванні можливо оцінити властивість для довільної кількості комбайнів. 4. Вплив непередбачуваних факто- рів типу погоди, рельєфу та інше. Дана властивість вивчається за допомогою встановлення можливих дій, що моделю- ють дані фактори та відповідними видами моделювання. 5. Дотримання умов перевезення вантажу (в нашому випадку зібраного урожаю) при передачі від одного агента іншому. При перевезенні розглядаються додаткові фактори середовища, які моде- люються в процесі верифікації. Це час пе- ревезення, вологість, температура, які бе- руться до уваги в моделі, як додаткові ат- рибути системи. 5. Верифікація і формалізації системи міжнародної логістики Відкрита система міжнародної логі- стики є продовженням описаної закритої логістичної обслуговуючої системи фер- мерського господарства. Вихідний про- дукт фермерського господарства (напри- клад, соя) є вхідним продуктом для відк- ритої міжнародної логістичної системи (переробка сої на соєву олію та її експорт). Істотною відмінністю цієї системи є теоре- Теоретичні і методологічні основи програмування 95 тично нескінченна кількість не пов’язаних між собою незалежних агентів кожного типу, і, як наслідок, постійна зміна середо- вищ існування. Аналогічно з закритою логістичною системою, де функцію збору інформації та контролю виконує Централі- зована база даних, в даній відкритій сис- темі існує подібний агент – Система. Од- нак на відміну від закритої системи, де агенти діють злагоджено та в спільних інтересах, вимоги надійності та безпеки до відкритої системи значно вищі, так як ко- жен з незалежних агентів діє в своїх осо- бистих інтересах. Тому для даних цілей доцільно застосовувати технологію розпо- ділених децентралізованих систем (блок- чейн) замість стаціонарного серверу. Спи- сок типових основних агентів, їх функції та інформацію, яку вони надають розподі- леній системі, наведено в табл. 3. Таблиця 3. Список агентів, їх функцій та інформації, яку вони надають централізованій системі Agent Функції Інформація, яку надає для системи Виробник (він же експортер) товару - виробництво товару - пошук покупця - аналіз цін (пропозицій) та вибір оптимального покупця - відвантаження товару - пошук оптимальних логістичних агентів – портових операторів та морських перевізників наявний об’єм товару до відвантаження - базові характеристики та якість товару (за- мовляється експортером) - узгоджена ціна - узгоджений покупець - узгоджені з Покупцем умови відвантажен- ня та оплати всіх дій (хто оплачує послуги посередників та на яких етапах здійснення) - дата готовності до відвантаження - узгоджені логістичні агенти – портовий оператор та морський перевізник Портовий опе- ратор - здійснення внутрішньої обслуговуючої логісти- ки від виробника до за- вантаження на морське судно - дата подачі контейнера виробнику згідно дати готовності до відвантаження, надану виробником (пізніше або в день його дати) - підтвердження здійснення та дата проміж- них етапів: відвантаження у виробника, прибуття в порт, завантаження на судно та інші можливі етапи Морський пе- ревізник - приймає на борт судна контейнер від Портово- го оператора та здійс- нення перевезення - факт та дата прийняття контейнера на борт судна Покупець то- вару - пошук продавця - аналіз цін (пропозицій) та вибір оптимального продавця - оплата за товар - бажаний об’єм товару для відвантаження - мінімальні характеристики та якість товару (підтверджується продавцем) - узгоджена ціна - узгоджений продавець - узгоджені з продавцем умови відвантажен- ня та оплати всіх дій (хто оплачує послуги посередників та на яких етапах здійснення) - підтвердження наданих продавцем логіс- тичних агентів – портовий оператор та морський перевізник Банк кожного з агентів - здійснює оплату за то- вар чи послуги згідно інформації, отриманої від свого агенту - інформація про суму та дату здійснення оплати, кому з агентів та за яку роботу Теоретичні і методологічні основи програмування 96 Поведінка та дії агентів описуються аналогічно моделі фермерського господар- ства. До моделі включаються відстані та географічна інформація про точки в яких діють агенти. Як властивості які можуть бути перевірені такі: - своєчасна доставка; - дотримання температурного режиму; - дотримання режиму вологості; - здатність протистояти зовніш- нім факторам. Властивості перевіряються такими методами алгебри поведінок, як алгебраїч- не зіставлення, символьне моделювання системи із довільною кількістю агентів та статичні методи доведення. Специфіка системи – використання децентралізова- них систем, які є однотипними, але збері- гають всі атрибути, які стосуються всього ланцюга постачання, дані про перевозку, транзакції з оплатою тощо. Кожен агент зберігає файл з інформацією про ланцюг постачання або транзакції. Ми розглядає- мо два типи використання формальних методів в даній моделі. 1. Моделювання ланцюга постачан- ня для перевірки властивостей. В даній процедурі ми перевіряємо чи відповідає вибраний ланцюг постачання вимогам пе- ревезення. Перевіряються також властиво- сті супротиву до зовнішніх небажаних дій – погоди, шахрайства, кібератаки. 2. Моніторинг перевезення згідно вибраної моделі безпеки. Дана процедура призначена для виявлення порушення вла- стивостей безпеки заздалегідь при вивчен- ні сценарію поведінки. При моніторингу разом із моделлю безпеки може бути вико- ристана модель класифікації, що створена за допомогою машинного навчання. Висновки У цій роботі ми дослідили можливі підходи до застосування математичного моделювання та застосування алгебри по- ведінок для прогнозування безпеки та на- дійності логістичних систем відкритого та закритого типів. Наші експериментальні результати підтвердили велику значущість використання математичного моделюван- ня та використання алгебри поведінок для застосування в реальних логістичних системах. Для складних комплексних систем, такі як логістичні, вкрай важливе значення має перевірка властивостей безпеки та зда- тності функціонувати тривалий час без втрати результативності. Дана методика є одним з вагомих інструментів при вико- нанні цих задач. Моделювання поведінки кожного агента системи дає змогу проана- лізувати властивості всієї системи загалом. На даний час перспектива цієї робо- ти вбачається у поєднанні описаної мето- дики з розподіленими системами (зокрема блокчейн). Вже розроблена платформа- клієнт, що виступає незалежним агентом, що контролює дії усіх учасників, та най- ближчим часом планується експеримент з використання даного проекту при реаль- них експортних відправках. Література 1. BPMN (Business Process Model and Notation). www.bpmn.org 2. UML (Unified Modelling Language). www.uml.org 3. SysML (Systems Modelling Language). www.sysml.org 4. VDM (Vienna Development Method). www.vienna.cc/e/evdm.htm 5. SPIN. http://spinroot.com/spin/whatispin.html 6. APS (Algebraic Programming System).www.apsystem.org.ua 7. Letichevsky A., Letychevskyi O., and Peschanenko V. Insertion Modeling and Its Applications. Computer Science Journal of Moldova. 2016. vol. 24. N. 3. P. 357–370. 8. Letichevsky A. and Gilbert D. Interaction of agents and environments. In Recent Trends in Algebraic Development Technique. LNCS 1827. Springer-Verlag. 1999. 9. Letychevskyi O,, Letichevsky A., Peschanenko V., Weigert T., Insertion modeling and symbolic verification of large systems,”I LNCS 9369 SDL 2015: Model- Driven Engineering for Smart Cities. Spring- er. 2015. P. 3–18. Теоретичні і методологічні основи програмування 97 References 1. 1 BPMN (Business Process Model and Notation). www.bpmn.org 2. UML (Unified Modelling Language). www.uml.org 3. SysML (Systems Modelling Language). www.sysml.org 4. VDM (Vienna Development Method). www.vienna.cc/e/evdm.htm 5. SPIN. http://spinroot.com/spin/whatispin.html 6. APS (Algebraic Programming System).www.apsystem.org.ua 7. Letichevsky A., Letychevskyi O., and Peschanenko V. Insertion Modeling and Its Applications. Computer Science Journal of Moldova. 2016. vol. 24. N. 3. P. 357–370. 8. Letichevsky A. and Gilbert D. Interaction of agents and environments. In Recent Trends in Algebraic Development Technique. LNCS 1827. Springer-Verlag. 1999. 9. Letychevskyi O,, Letichevsky A., Peschanenko V., Weigert T., Insertion modeling and symbolic verification of large systems,”I LNCS 9369 SDL 2015: Model- Driven Engineering for Smart Cities. Spring- er. 2015. P. 3–18. Одержано 23.10.2020 Про авторів: Летичевський Олександр Олександрович, доктор фізико-математичних наук, завідувач відділу теорії цифрових автоматів Кількість наукових публікацій в українських виданнях – 32. Кількість наукових публікацій в зарубіжних виданнях – 37. Індекс Гірша – 4, Горбатюк Сергій Олександрович, аспірант кафедри Комп’ютерних наук та інформаційних технологій. https://orcid.org/0000-0001-6834-4211, Горбатюк Віктор Олександрович, аспірант кафедри Комп’ютерних наук та інформаційних технологій. https://orcid.org/0000-0001-7544-0260. Місце роботи авторів: Інститут кібернетики імені В.М. Глушкова Національної академії наук України. 03187, м. Київ проспект Академіка Глушкова, 40. Тел.: (044) 526-20-08. E-mails: gorbatiuk_sergiy@i.ua, lit@issukraine.com, viktor.gorbatiuk@gmail.com mailto:gorbatiuk_sergiy@i.ua mailto:lit@issukraine.com mailto:viktor.gorbatiuk@gmail.com