Алгебраїчне моделювання та його застосування

Статтю присвячено науковим розробкам Інституту кібернетики ім. В.М. Глушкова НАН України, пов’язаним із застосуванням технологій алгебраїчного та інсерційного моделювання на основі алгебри поведінок. Розглянуто технології формалізації, алгебраїчної верифікації та тестування програмних і апаратних...

Ausführliche Beschreibung

Gespeichert in:

Bibliographische Detailangaben
Datum:	2021
1. Verfasser:	Летичевський, О.О.
Format:	Artikel
Sprache:	Ukrainian
Veröffentlicht:	Видавничий дім "Академперіодика" НАН України 2021
Schriftenreihe:	Вісник НАН України
Schlagworte:	Статті та огляди
Online Zugang:	http://dspace.nbuv.gov.ua/handle/123456789/179713
Tags:	Tag hinzufügen Keine Tags, Fügen Sie den ersten Tag hinzu!
Назва журналу:	Digital Library of Periodicals of National Academy of Sciences of Ukraine
Zitieren:	Алгебраїчне моделювання та його застосування / О.О. Летичевський // Вісник Національної академії наук України. — 2021. — № 3. — С. 59-66. — Бібліогр.: 22 назв. — укр.

Institution

Digital Library of Periodicals of National Academy of Sciences of Ukraine

id	irk-123456789-179713
record_format	dspace
spelling	irk-123456789-1797132021-06-01T01:26:31Z Алгебраїчне моделювання та його застосування Летичевський, О.О. Статті та огляди Статтю присвячено науковим розробкам Інституту кібернетики ім. В.М. Глушкова НАН України, пов’язаним із застосуванням технологій алгебраїчного та інсерційного моделювання на основі алгебри поведінок. Розглянуто технології формалізації, алгебраїчної верифікації та тестування програмних і апаратних специфікацій у рамках модельного способу розроблення програмних систем. Приділено увагу використанню алгебраїчного моделювання в біологічних дослідженнях, створенні систем на основі блокчейн-платформ, аналізі правових та економічних моделей. Як один з основних напрямів практичного застосування зазначених технологій виокремлено галузь кібербезпеки, в якій використовується метод алгебраїчного зіставлення та формалізація шаблонів вразливостей і кібератак. The article is devoted to the scientific development of the Glushkov Institute of Cybernetics of the National Academy of Sciences of Ukraine on the application of algebraic and insertional modeling technologies created on the basis of behavioral algebra. Technologies of formalization, algebraic verification, and testing of software and hardware specifications within the model-driven development method are considered. The use of algebraic modeling in biological research, development of systems based on blockchain platforms, analysis of legal and economic models is covered. One of the main areas of application of these technologies is the field of cybersecurity, which uses the method of algebraic matching and formalization of patterns of vulnerabilities and cyberattacks. 2021 Article Алгебраїчне моделювання та його застосування / О.О. Летичевський // Вісник Національної академії наук України. — 2021. — № 3. — С. 59-66. — Бібліогр.: 22 назв. — укр. 0372-6436 DOI: doi.org/10.15407/visn2021.03.059 http://dspace.nbuv.gov.ua/handle/123456789/179713 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	2021
topic_facet	Статті та огляди
url	http://dspace.nbuv.gov.ua/handle/123456789/179713
citation_txt	Алгебраїчне моделювання та його застосування / О.О. Летичевський // Вісник Національної академії наук України. — 2021. — № 3. — С. 59-66. — Бібліогр.: 22 назв. — укр.
series	Вісник НАН України
work_keys_str_mv	AT letičevsʹkijoo algebraíčnemodelûvannâtajogozastosuvannâ
first_indexed	2025-07-15T18:39:33Z
last_indexed	2025-07-15T18:39:33Z
_version_	1837739313265115136
fulltext	ISSN 1027-3239. Вісн. НАН України, 2021, № 3 59 АЛГЕБРАЇЧНЕ МОДЕЛЮВАННЯ ТА ЙОГО ЗАСТОСУВАННЯ Статтю присвячено науковим розробкам Інституту кібернетики ім. В.М. Глушкова НАН України, пов’язаним із застосуванням технологій алгебраїчного та інсерційного моделювання на основі алгебри поведінок. Розглянуто технології формалізації, алгебраїчної верифікації та тесту- вання програмних і апаратних специфікацій у рамках модельного способу розроблення програмних систем. Приділено увагу використанню алгебра- їчного моделювання в біологічних дослідженнях, створенні систем на основі блокчейн-платформ, аналізі правових та економічних моделей. Як один з основних напрямів практичного застосування зазначених технологій ви- окремлено галузь кібербезпеки, в якій використовується метод алгебраїч- ного зіставлення та формалізація шаблонів вразливостей і кібератак. Ключові слова: алгебраїчне моделювання, вразливості коду, модельний метод розроблення, інсерційне моделювання, формальна верифікація, модельне тестування, гібридні інтелектуальні системи. У 70-х роках минулого століття у відділі теорії цифрових автоматів, яким керував засновник Інституту кібернетики академік Віктор Михайлович Глушков, було розроблено одну з перших у світі систем автоматичного доведення теорем [1], що поклало початок розвитку технології алгебраїчного про- грамування. Систему APS (Algebraic Programming System) [2] було створено як інструментарій для реалізації алгебраїч- них алгоритмів з метою автоматичного доведення тверджень, розв’язання рівнянь у різних теоріях, задач доказового програ- мування, паралельного програмування, перетворень формаль- них специфікацій та інших проблем. Перші програми символьного моделювання було написано мовою АПЛАН, що ґрунтується на застосуванні систем пере- писувальних правил. Надалі цей напрям активно розвивався, оскільки символьне моделювання виявилося ефективним для вирішення багатьох індустріальних завдань у різноманітних предметних галузях. Продовженням алгебраїчного програму- вання стала технологія інсерційного моделювання [3]. Вона узагальнювала алгебраїчний підхід для формалізації проце- сів, які можна описувати як взаємодію агентів та їх занурення (insertion) у середовище. ЛЕТИЧЕВСЬКИЙ Олександр Олександрович — доктор фізико-математичних наук, завідувач відділу теорії цифрових автоматів Інституту кібернетики ім. В.М. Глушкова НАН України doi: https://doi.org/10.15407/visn2021.03.059 60 ISSN 1027-3239. Visn. Nac. Acad. Nauk Ukr. 2021. (3) СТАТТІ ТА ОГЛЯДИ Уперше систему інсерційного моделюван- ня було впроваджено на практиці для вирі- шення завдань, пов’язаних з верифікацією та тестуванням телекомунікаційних систем та їхніх програмних і апаратних компонентів. З 2000 р. розпочалася активна співпраця Ін- ституту кібернетики ім В.М. Глушкова НАН України з компанією Motorola, і інсерційний підхід став основою системи VRS (Verification of Requirements Specifications) [4]. Ця система була призначена для автоматичної верифікації формальних вимог до проєктів програмного та апаратного забезпечення, для чого, відповідно, було розроблено технологію формалізації тек- стових та напівформальних вимог. Пізніше цю технологію було застосовано до верифікації дизайну систем та генерації тестових сценаріїв із заданим покриттям. Після перших успішних впроваджень у те- лекомунікаційних проєктах компанії Motorola коло предметних галузей використання систе- ми VRS значно розширилося: мережеві про- токоли, мікропроцесорне середовище, авто- мобільна промисловість тощо. Останнім часом алгебраїчне моделювання впроваджується у сфері кібербезпеки, біології, економіки, пра- ва. Досвід таких інституцій, як Агентство пе- редових оборонних дослідницьких проєктів США (DARPA), та провідних IT-компаній, наприклад Amazon, Google та Intel, свідчить, що формальні методи, зокрема алгебраїчний підхід, має бути покладено в основу всіх сучас- них інструментів, які використовуються при проєктуванні, дослідженні та аналізі складних систем. Важливість застосування алгебраїчно- го підходу зумовлена також створенням сучас- них ефективних програм, що виконують авто- матичне доведення тверджень та розв’язок за- дач у різних теоріях. Алгебра поведінок. У 1997 р. британський учений Девід Гільберт (David R. Gilbert) та український кібернетик академік НАН Укра- їни Олександр Адольфович Летичевський (1935–2019) розробили теоретичні основи інсерційного моделювання, зокрема алгебру поведінок [5]. Відмінністю інсерційного мо- делювання від попередніх теорій формальних процесів було використання понять «агент» та «середовище». Сценарії поведінок агентів мо- жуть породжуватися в багаторівневому сере- довищі, тобто сам агент може бути середови- щем для інших агентів. Формально алгебра по- ведінок визначається як двохосновна алгебра над множинами поведінок та дій агентів. Вона містить операцію префіксингу та операцію не- детермінованого вибору поведінок і включає три термінальні константи: успішне припи- нення Δ, тупик 0 та невідома поведінка . Крім того, алгебра поведінки розширена двома опе- раціями: паралельні (\|\|) та послідовні (;) ком- позиції поведінок. Терм, створений з операцій алгебри поведінки над поведінками та діями, формує вираз алгебри поведінок. Семантика дій визначається перед- та після- умовою, що характеризують допустимість дій агента в середовищі та відповідну зміну сере- до вища. Символьне моделювання поведінки агента визначається послідовністю його дій. У різних предметних галузях агент може мати свій тип або набір атрибутів з відповід- ними простими типами. Формули перед- та післяумови є формулами над множиною атри- бутів у відповідній теорії. При формалізації поведінки агентів у певній предметній галузі на різних рівнях абстракції використовують теорії булевої алгебри, цілочислової та ірраці- ональної арифметики, теорії перелічувальних символьних типів. Для створення середовищ моделей програм у мережевому та хмарному оточенні застосовують теорії, які містять опе- рації та предикати над байтами і бітами. Розроблення систем високої надійності. Найважливішою сферою використання алге- браїчного підходу є розроблення систем, кри- тичних до безпеки. В Інституті кібернетики ім. В.М. Глушкова НАН України алгебраїчне моделювання впроваджено в модельний спо- сіб розроблення програмного та апаратного забезпечення. Модельний метод передбачає, що на кожному етапі розроблення, зокрема на стадіях усталення вимог, дизайну, кодування і тестування, з використанням формальних методів створюються відповідні моделі, при- значені для верифікації та валідації системи. ISSN 1027-3239. Вісн. НАН України, 2021, № 3 61 СТАТТІ ТА ОГЛЯДИ Сучасні стандарти розроблення критичних до безпеки систем у медицині, авіакосмічній та автомобільній промисловості вже містять ви- моги до використання відповідних формаль- них методів. Ціна помилки, допущеної на ранніх стаді- ях розроблення критичних систем, може ви- явитися дуже високою. Недостатня надійність системи може вкрай негативно вплинути на загальний перебіг процесу реалізації проєкту, зокрема на його якість, собівартість та термі- ни виконання. Тому процедури формальної верифікації та тестування слід застосовувати як до системних вимог, так і до дизайну та про- грамного коду. Для цього на відповідних ета- пах розроблення системи створюють моделі формальних вимог, модель дизайну та модель коду. Ці моделі можуть бути отримані зі спе- цифікацій формальних мов, таких як UML [6], SysML [7], BPMN [8], та мов програмування автоматичною трансляцією у специфікації ал- гебри поведінок. Маючи алгебраїчну модель, можна впровадити процедуру верифікації, ви- користовуючи формальні методи, розроблені в рамках алгебри поведінок. Основними метода- ми є символьне моделювання, методи алгебра- їчного зіставлення та автоматичне доведення тверджень. Такі методи дають змогу верифіку- вати специфікації на недетермінізм, повноту, збереження властивостей безпеки та доведен- ня життєздатності. Зазначені моделі є також джерелом тестів, як для специфікації дизайну, так і для програмного коду. Загальну схему життєвого циклу модель- ної розробки водоспадного типу наведено на рис. 1. Алгебраїчний та інсерційний підходи ефек- тивні для розподілених мереж та систем, для яких у зв’язку з нескінченною або великою кількістю станів традиційні методи тестуван- ня та верифікації можуть не дати гарантовано- го покриття. Формальні методи завдяки тому, що вони дозволяють застосовувати абстракції різних рівнів, дають змогу вирішувати такі за- вдання для досить широкого класу моделей. Модельний спосіб розроблення програмних систем було застосовано також для створення апаратного забезпечення. У рамках співробіт- ництва Інституту кібернетики ім. В.М. Глуш- кова НАН України з Національним аерокос- мічним університетом ім. М.Є. Жуковського «Харківський авіаційний інститут» та ТОВ «Науково-виробниче підприємство «Ра- дікс» — виробником мікроелектроніки для потреб атомної енергетики України, було про- ведено апробацію модельного способу роз- роблення апаратних систем [9]. На кожному етапі V-модельного життєвого циклу системи для дизайну мікроелектроніки використову- ються специфікації формальних мов, таких як Рис. 1. Загальна схема життєво- го циклу модельної розробки во- доспадного типу 62 ISSN 1027-3239. Visn. Nac. Acad. Nauk Ukr. 2021. (3) СТАТТІ ТА ОГЛЯДИ VHDL [10], System Verilog [11], та специфіка- ції формальних вимог до апаратного забезпе- чення. Загальну схему такого циклу наведено на рис. 2. Завдання кібербезпеки. Специфіка сучас- них методів кібербезпеки полягає в постійній адаптації технології захисту до нових атак зловмисників. Нові методи проникнення та ураження програмних і апаратних систем з’яв- ля ються щодня, тому традиційні технології антивірусних та інших засобів безпеки можуть виявитися неефективними. Алгебраїчний під- хід дає змогу охоплювати класи шкідливих дій з використанням абстракцій різного рів- ня. Ефективність використання алгебраїчного підходу було доведено на міжнародному зма- ганні з кібербезпеки, проведеному корпораці- єю DARPA [12]. Перші три місця на ньому по- сіли компанії, які використовують символьне моделювання. В Інституті кібернетики ім. В.М. Глушкова НАН України розроблено технологію алгебра- їчної формалізації можливих вразливостей у бінарному коді програми. Поведінка програми при використанні зловмисником вразливості записується у вигляді виразів алгебри поведі- нок. Наприклад, вразливість «ураження про- грамного стеку» складається з трьох поведін- кових виразів: точка входу в програму, ство- рення нового стекового простору для запису змінних процедури та запис до стеку з метою пошкодження даних або перехоплення управ- ління зловмисником. У такий спосіб було фор- малізовано певну частину відомих вразливос- тей зі світових баз даних. Розроблені алгоритми символьного моделю- вання та алгебраїчного зіставлення дозволя- ють ефективно знаходити вразливість за її ал- гебраїчним шаблоном на рівні бінарного коду [13], зокрема на рівні машинних інструкцій мови Intel x86. Ефективність алгебраїчного ме- тоду полягає в подоланні проблеми помилко- вих виявлень (false positive) та покритті більш широкого класу вразливостей. Відомо, що ал- гебраїчні методи підвищують обчислювальну складність, але бурхливий розвиток дедук- тивних інструментів та програм-розв’язувачів [14] в останнє десятиліття дав можливість ви- користовувати символьні обчислення в усіх сферах комп’ютерних технологій. Алгебраїчний підхід до формалізації вразли- востей, зокрема використання абстракцій, дає змогу знаходити прояви невідомих вразливос- тей, що можуть стати мішенню для шкідливих дій зловмисників. Ще один із методів пошуку так званих «вразливостей нульового дня» — це метод алгебраїчного фазингу (fuzzing), за до- помогою якого за попереднім аналізом коду можна виявити критичні вхідні дані, що зла- мують програму. Рис. 2. Життєвий цикл розробки V-модельного типу ISSN 1027-3239. Вісн. НАН України, 2021, № 3 63 СТАТТІ ТА ОГЛЯДИ Виявлення вразливостей у бінарному коді є важливим етапом у забезпеченні захисту систем об’єктів критичної інфраструктури, насамперед при встановленні та експлуатації програмних систем. Придбані системи потен- ційно можуть містити вразливості, які умож- ливлюють неавторизоване проникнення або пошкодження даних. Принаймні такий етап перевірки на вразливості є необхідним при розробленні програмного забезпечення як на стадії кодування, так і при тестуванні програм. Інше використання алгебраїчного підхо- ду можливе при виявленні кібератак під час функціонування програмної системи. Алге- браїчний шаблон зламу або проникнення в систему можна описати відносно дій зловмис- ника. Аналізуючи трафік та дії в системі або мережі, алгоритм алгебраїчного зіставлення з шаблоном поведінки зловмисника просигналі- зує в разі її виявлення. Для виявлення зловмисників у мережі або хмарному середовищі алгебраїчний підхід ви- користовується також у комбінації з методами машинного навчання [15]. Модель класифіка- ції, яка попередньо виявляє підозру на пове- дінку зловмисника на рівні нейронної мережі, може активувати алгебраїчні алгоритми для точного виявлення атаки. Технологію формалізації вразливостей у термінах алгебри поведінок застосовують і для виявлення нештатних функціональностей, які можуть бути внесені в систему програмістом- розробником для подальшої експлуатації з ме- тою проникнення або пошкодження системи. Методи виявлення таких «закладок» (back- doors) ґрунтуються на методах алгебраїчного моделювання та застосовуються як до про- грамних систем, так і для пристроїв мікроелек- троніки та інших апаратних систем. Гібридні інтелектуальні системи. Наукова спадщина академіка О.А. Летичевського охо- плює низку важливих розробок та перспектив- них ідей, зокрема впровадження в інсерційне моделювання неперервних процесів [16]. Ця ідея та начерки теорії стосуються аналі- зу і верифікації процесів у гібридних інтелек- туальних системах, що поєднують взаємодію фізичних об’єктів та дискретних обчислюваль- них процесів. По суті для таких систем вико- ристовується комбінація алгебри поведінок та фізичних процесів, що описуються диферен- ційними рівняннями і фігурують у дискретній системі як процес переходу між станами. Від- мінність від сучасних гібридних систем, таких як автомат Хенцінгера [17], полягає в тому, що неперервні процеси розглядаються в контексті взаємодії агентів фізичних систем у багаторів- невих середовищах. Завдяки такій синергії гі- бридний підхід збагачує можливості вивчення природних, зокрема біологічних, об’єктів. Гібридний підхід було застосовано у спільних роботах Інституту кібернетики ім. В.М. Глуш- кова НАН України та Херсонського держав- ного університету для формалізації хімічних і біологічних взаємодій. Можливість будувати абстракції на різних рівнях представлення мо- делей дозволила розглядати взаємодії агентів та середовищ від молекулярного рівня до рів- нів вищих організацій матерії. На рівні молекулярної взаємодії розгляда- ються середовища, в яких атоми і молекули є агентами, що змінюють свої стани та структу- ри. Дії таких агентів, що формалізуються алге- браїчними рівняннями, моделюють переходи електронів на орбіталях, встановлення різно- видів молекулярного зв’язку, розклад молекул на складові, утворення нових агентів та інші можливі взаємодії. У формальній моделі при- сутня також неперервна компонента, яка опи- сує, наприклад, перебіг хімічної реакції. У системі інсерційного моделювання про- ведено низку експериментів зі взаємодії мо- лекул органічних речовин. Систему було інте- гровано з відомими форматами представлення молекул, що дає можливість використовувати інформацію про речовини із всесвітніх банків даних, зокрема з банку білків. Наразі планується продовжити експеримен- ти з гібридними системами в хімії та біології. Алгебраїчне моделювання молекулярної вза- ємодії можна використовувати і для розгляду агентів та середовищ на іншому рівні абстрак- ції. Зокрема, передбачається застосування цієї технології для вивчення взаємодії вірусу з 64 ISSN 1027-3239. Visn. Nac. Acad. Nauk Ukr. 2021. (3) СТАТТІ ТА ОГЛЯДИ клітинами. Такі дослідження в системі інсер- ційного моделювання дадуть змогу вивчати поведінку та властивості агентів клітинного середовища, наприклад з метою розроблення вакцин в умовах еволюції вірусів. Технологія блокчейн. Технологія блокчейн, яка основана на принципах децентралізації та алгоритмах консенсусу, сьогодні дедалі ширше впроваджується в різні сфери економічної та суспільної діяльності як технологія, що забез- печує захищеність від стороннього втручання, цілісність даних та справедливість вибору. Про- те складність систем на блокчейн-платформах зумовлює можливість появи помилок, які не так просто виявити. З іншого боку, виникнення цієї нової технології і поширення використання криптовалют спричинили появу нових технік зламу та втручань у роботу систем. При використанні алгебраїчного моделю- вання як агентів розглядають вузли мережі, в рамках якої функціонує протокол блокчейну. Агенти обмінюються транзакціями, формуючи блокчейн, але при цьому може з’явитися зло- вмисник, який використовуватиме вразливос- ті протоколу з метою викрадення криптовалю- ти. Такі ситуації трапляються при функціону- ванні «розумних контрактів» (smart contracts) [18] у рамках протоколів блокчейну. В цьому разі також можна формалізувати відомі по- ведінки зловмисника як алгебраїчні шаблони, що дає змогу перевіряти стійкість «розумного контракту» до атак та наявність у ньому враз- ливостей. У різних галузях сучасної індустрії останнім часом з’явилося багато систем на основі блок- чейн-платформ, зокрема фінансові, енергетич- ні та логістичні системи. В Інституті кіберне- тики ім. В.М. Глушкова НАН України розро- блено технологію формалізації, верифікації та тестування таких платформ з використанням алгебраїчного моделювання [19]. Також роз- глядається можливість використання гібрид- ного підходу, який поєднує алгебраїчний під- хід та методи машинного навчання для форму- вання моделі класифікації поведінки. Економіка та право. У спільних з Херсон- ським державним університетом роботах ал- гебраїчне моделювання та інсерційний підхід було застосовано для створення економічних та правових моделей. В економічних системах як взаємодіючі агенти розглядаються різні об’єкти, що вза- ємодіють один з одним у рамках економічної діяльності, а саме — державні органи управ- ління, підприємства, банки, групи населення. Завданням для використання алгебраїчного моделювання в економіці є вивчення власти- востей економічної системи, наприклад еко- номічної рівноваги. Властивості описують формулами в алгебрі поведінок і за допомогою символьного моделювання з’ясовують, чи до- сяжна ситуація, коли та чи інша властивість проявляється, або чи є серед множини сцена- ріїв такий, що приводить до порушення певної властивості системи. В економіці алгебраїчна модель з більшою точністю може передбачити розвиток подій, оскільки вона, на відміну від імітаційного моделювання, працює з множи- ною сценаріїв. У проєктах, що реалізуються на основі блок- чейн-платформ, використовують добре фор- малізовані алгоритми із застосуванням токе- нів — умовних грошових одиниць. Досліджен- ня властивостей таких систем та передбачення небажаних сценаріїв є важливим завданням, яке успішно вирішується за допомогою алге- браїчного підходу [20]. У моделюванні правових систем в рамках експерименту було формалізовано Податко- вий кодекс України у вигляді моделі взаємодії агентів — платників податків [21]. Одним із завдань, для вирішення якого може бути вико- ристано алгебраїчне моделювання, є перевірка правомірності дій платника податків відповід- но до Податкового кодексу та виявлення по- рушень. Це може бути застосовано як під час моніторингу функціонування агентів, так і при розгляді судових рішень та суперечливих си- туацій. Формальна модель законів дає також змогу перевірити їх на властивості повноти та вза- ємосуперечливості положень окремих статей. Одним із прикладів такого використання є до- ведення суперечливості в положеннях старої ISSN 1027-3239. Вісн. НАН України, 2021, № 3 65 СТАТТІ ТА ОГЛЯДИ версії Податкового кодексу на основі преце- денту «засуджений ПДВ» [22]. На сьогодні алгебраїчний підхід та методи символьних обчислень все ширше застосову- ються в наукових дослідженнях та в процесі створення сучасних програмних систем. Нові ефективні інструменти, такі як дедуктивні системи, програми-розв’язувачі, засоби авто- матичного доведення, є не лише предметом обговорення на наукових конференціях, вони вже використовуються в практичній діяль- ності багатьох передових індустріальних ком- паній. Тому подальший розвиток таких підхо- дів, особливо в поєднанні з іншими методами штучного інтелекту, прогнозується як один з найважливіших напрямів у сучасній індустрії. REFERENCES [СПИСОК ЛІТЕРАТУРИ] 1. Letichevsky A., Lyaletski A., Morokhovets M. Glushkov’s evidence algorithm. Cybernetics and Systems Analysis. 2013. 49(4): 489–500. DOI: https://doi.org/10.1007/s10559-013-9534-z [Летичевский А.А., Лялецкий А.В., Мороховец М.К. Алгоритм очевидности Глушкова. Кібернетика та сис- темний аналіз. 2013. Т. 49, № 4. C. 3–16.] 2. Kapitonova J., Letichevsky A. Algebraic Programming in the APS System. In: ISSAC ‘90: Proceedings of the interna- tional symposium on symbolic and algebraic computation (20-25 August, 1990, Tokyo, Japan). P. 68–75. DOI: https:// doi.org/10.1145/96877.96896 3. Letichevsky A., Letychevskyi O., Peschanenko V. Insertion Modeling and Its Applications. Computer Science Journal of Moldova. 2016. 24(3): 357–370. http://www.apsystems.org.ua/uploads/doc/aps/APSv3.eng.pdf 4. Letichevsky A., Kolchin A., Letychevskyi O., Potiyenko S., Volkov V., Weigert T. Formal Requirements Capturing using VRS system. In: Voronkov A., Kovács L., Bjorner N. (eds). WING 2010. Workshop on Invariant Generation 2010 (21 July, 2010, Edinburgh, UK). Vol. 1. P. 148–149. DOI: https://doi.org/10.29007/q6mc 5. Letichevsky A., Gilbert D. A Model for Interaction of Agents and Environments. In: Bert D., Choppy C., Mosses P.D. (eds). Recent Trends in Algebraic Development Techniques. WADT 1999. Lecture Notes in Computer Science. Vol. 1827. Berlin, Heidelberg: Springer, 2000. P. 311–328. DOI: https://doi.org/10.1007/978-3-540-44616-3_18 6. Booch G., Rumbaugh J., Jacobson I. Unified modeling language user guide. Addison-Wesley, 2005. 7. Burger E. Flexible views for view-based model-driven development. KIT Scientific Publishing, 2014. 8. Silver B. BPMN method and style. Cody–Cassidy Press, 2011. 9. Letychevskyi O., Odarushchenko O., Peschanenko V., Kharchenko V., Volkov V. Modeling Method for Development of Digital System Algorithms Based on Programmable Logic Devices. Cybernetics and Systems Analysis. 2020. 56: 710–717. DOI: https://doi.org/10.1007/s10559-020-00289-8 [Летичевський О., Одарущенко О., Песчаненко В., Харченко В., Волков В. Модельний спосіб розроблення алгоритмів цифрових систем на програмованих логічних інтегральних схемах. Кібернетика та системний аналіз. 2020.Т. 56, № 5. C. 29–37.] 10. Coelho D. The VHDL handbook. Springer Science & Business Media, 1989. 11. Sutherland S., Davidmann S., Flake P. SystemVerilog for Design. Springer Science & Business Media, 2006. 12. Fraze D. Cyber Grand Challenge (CGC) (Archived). DARPA. https://www.darpa.mil/program/cyber-grand-chal- lenge 13. Letychevskyi O. Two-Level Algebraic Method for Detection of Vulnerabilities in Binary Code. In: Proc. of 10th IEEE International Conference on Intelligent Data Acquisition and Advanced Computing Systems (18-21 September, 2019, Metz, France). DOI: https://doi.org/10.1109/IDAACS.2019.8924255 14. Robere R., Kolokolova A., Ganesh V. The Proof Complexity of SMT Solvers. In: Chockler H., Weissenbacher G. (eds). Computer Aided Verification. CAV 2018. Lecture Notes in Computer Science. Vol. 10982. Springer, Cham, 2018. DOI: https://doi.org/10.1007/978-3-319-96142-2_18 15. Letychevskyi O., Polhul T. Detection of Fraudulent Behavior Using the Combined Algebraic and Machine Learn- ing Approach. In: Proc. of IEEE International Conference on Big Data (9-12 December, 2019, Los Angeles, USA). DOI: https://doi.org/10.1109/BigData47090.2019.9006546 16. Letichevsky A. Algebraic Interaction Theory and Cyber-Physical Systems. Journal of Automation and Information Sciences. 2017. 49(9): 1–19. DOI: https://doi.org/10.1615/JAutomatInfScien.v49.i9.10 66 ISSN 1027-3239. Visn. Nac. Acad. Nauk Ukr. 2021. (3) СТАТТІ ТА ОГЛЯДИ [Летичевский А.А. Алгебраическая теория взаимодействия и кибер-физические системы. Проблемы управле- ния и информатики. 2017. № 5. С. 37–55.] 17. Henzinger T.A. The theory of hybrid automata. In: Inan M.K., Kurshan R.P. (eds). Verification of Digital and Hy- brid Systems. NATO ASI Series (Series F: Computer and Systems Sciences). Vol. 170. Springer, Berlin, Heidelberg. DOI: https://doi.org/10.1007/978-3-642-59615-5_13 18. Alharby M., Moorsel A. Blockchain Based Smart Contracts. A Systematic Mapping Study. In: Proc. of International Conference on Cloud Computing, Big Data and Blockchain (15-17 November, 2018, Fuzhou, China). DOI: https://doi. org/10.5121/csit.2017.71011 19. Letychevskyi O., Peschanenko V., Radchenko V., Orlovskyi M., Sobol A. Algebraic approach to verification and test- ing of distributed applications. In: Proc. of Blockchain and Internet of Things Conference (7-9 July, 2019, Okinawa, Japan). DOI: https://doi.org/10.1145/3343147.3343159 20. Letychevskyi O., Peschanenko V., Radchenko V., Poltoratzkyi M., Mogylko S., Kovalenko P. Formal Verification of Token Economy Models. In: Proc. of International Conference on Blockchain and Cryptocurrency (14-17 May, 2019, Seoul, South Korea). DOI: https://doi.org/10.1109/BLOC.2019.8751318 21. Letichevsky A., Letychevskyi O., Peschanenko V., Poltoratzky M. An Algebraic Approach for Analyzing of Legal Re- quirements. In: Proc. of International Requirements Engineering Conference Workshops (REW). (4-8 Septеmber, 2017, Lisbon). DOI: https://doi.org/10.1109/REW.2017.51 22. «Zasudzhenyi» PDV abo Pretsedent na koryst platnyka podatku. Konsultant bukhhaltera. No. 16 (400). 16.04.2007. http://cons.parus.ua/_d.asp?r=03WMGd7e3c4816c93692e4d5ba8e0b8234dec [«Засуджений» ПДВ або Прецедент на користь платника податку. Консультант бухгалтера. № 16 (400). 16.04.2007.] Oleksandr О. Letychevskyi ORCID: https://orcid.org/0000-0003-0856-9771 Glushkov Institute of Cybernetics of the National Academy of Sciences of Ukraine, Kyiv, Ukraine ALGEBRAIC MODELING AND ITS APPLICATION The article is devoted to the scientific development of the Glushkov Institute of Cybernetics of the National Academy of Sciences of Ukraine on the application of algebraic and insertional modeling technologies created on the basis of behav- ioral algebra. Technologies of formalization, algebraic verification, and testing of software and hardware specifications within the model-driven development method are considered. The use of algebraic modeling in biological research, de- velopment of systems based on blockchain platforms, analysis of legal and economic models is covered. One of the main areas of application of these technologies is the field of cybersecurity, which uses the method of algebraic matching and formalization of patterns of vulnerabilities and cyberattacks. Keywords: algebraic modeling, code vulnerabilities, model-driven development, insertion modeling, formal verification, model-based testing, hybrid intelligent systems.

Алгебраїчне моделювання та його застосування

Institution

Ähnliche Einträge